-
Notifications
You must be signed in to change notification settings - Fork 251
/
Sigma.lean
112 lines (83 loc) · 3.5 KB
/
Sigma.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
-/
import Mathlib.Data.PFunctor.Multivariate.Basic
import Mathlib.Data.QPF.Multivariate.Basic
#align_import data.qpf.multivariate.constructions.sigma from "leanprover-community/mathlib"@"dc6c365e751e34d100e80fe6e314c3c3e0fd2988"
/-!
# Dependent product and sum of QPFs are QPFs
-/
universe u
namespace MvQPF
open MvFunctor
variable {n : ℕ} {A : Type u}
variable (F : A → TypeVec.{u} n → Type u)
/-- Dependent sum of an `n`-ary functor. The sum can range over
data types like `ℕ` or over `Type.{u-1}` -/
def Sigma (v : TypeVec.{u} n) : Type u :=
Σ α : A, F α v
#align mvqpf.sigma MvQPF.Sigma
/-- Dependent product of an `n`-ary functor. The sum can range over
data types like `ℕ` or over `Type.{u-1}` -/
def Pi (v : TypeVec.{u} n) : Type u :=
∀ α : A, F α v
#align mvqpf.pi MvQPF.Pi
instance Sigma.inhabited {α} [Inhabited A] [Inhabited (F default α)] : Inhabited (Sigma F α) :=
⟨⟨default, default⟩⟩
#align mvqpf.sigma.inhabited MvQPF.Sigma.inhabited
instance Pi.inhabited {α} [∀ a, Inhabited (F a α)] : Inhabited (Pi F α) :=
⟨fun _a => default⟩
#align mvqpf.pi.inhabited MvQPF.Pi.inhabited
namespace Sigma
instance [∀ α, MvFunctor <| F α] : MvFunctor (Sigma F) where
map := fun f ⟨a, x⟩ => ⟨a, f <$$> x⟩
variable [∀ α, MvQPF <| F α]
/-- polynomial functor representation of a dependent sum -/
protected def P : MvPFunctor n :=
⟨Σ a, (P (F a)).A, fun x => (P (F x.1)).B x.2⟩
set_option linter.uppercaseLean3 false in
#align mvqpf.sigma.P MvQPF.Sigma.P
/-- abstraction function for dependent sums -/
protected def abs ⦃α⦄ : Sigma.P F α → Sigma F α
| ⟨a, f⟩ => ⟨a.1, MvQPF.abs ⟨a.2, f⟩⟩
#align mvqpf.sigma.abs MvQPF.Sigma.abs
/-- representation function for dependent sums -/
protected def repr ⦃α⦄ : Sigma F α → Sigma.P F α
| ⟨a, f⟩ =>
let x := MvQPF.repr f
⟨⟨a, x.1⟩, x.2⟩
#align mvqpf.sigma.repr MvQPF.Sigma.repr
instance : MvQPF (Sigma F) where
P := Sigma.P F
abs {α} := @Sigma.abs _ _ F _ α
repr {α} := @Sigma.repr _ _ F _ α
abs_repr := by rintro α ⟨x, f⟩; simp only [Sigma.abs, Sigma.repr, Sigma.eta, abs_repr]
abs_map := by rintro α β f ⟨x, g⟩; simp only [Sigma.abs, MvPFunctor.map_eq]
simp only [(· <$$> ·), ← abs_map, ← MvPFunctor.map_eq]
end Sigma
namespace Pi
instance [∀ α, MvFunctor <| F α] : MvFunctor (Pi F) where map f x a := f <$$> x a
variable [∀ α, MvQPF <| F α]
/-- polynomial functor representation of a dependent product -/
protected def P : MvPFunctor n :=
⟨∀ a, (P (F a)).A, fun x i => Σ a, (P (F a)).B (x a) i⟩
set_option linter.uppercaseLean3 false in
#align mvqpf.pi.P MvQPF.Pi.P
/-- abstraction function for dependent products -/
protected def abs ⦃α⦄ : Pi.P F α → Pi F α
| ⟨a, f⟩ => fun x => MvQPF.abs ⟨a x, fun i y => f i ⟨_, y⟩⟩
#align mvqpf.pi.abs MvQPF.Pi.abs
/-- representation function for dependent products -/
protected def repr ⦃α⦄ : Pi F α → Pi.P F α
| f => ⟨fun a => (MvQPF.repr (f a)).1, fun _i a => (MvQPF.repr (f _)).2 _ a.2⟩
#align mvqpf.pi.repr MvQPF.Pi.repr
instance : MvQPF (Pi F) where
P := Pi.P F
abs := @Pi.abs _ _ F _
repr := @Pi.repr _ _ F _
abs_repr := by rintro α f; simp only [Pi.abs, Pi.repr, Sigma.eta, abs_repr]
abs_map := by rintro α β f ⟨x, g⟩; simp only [Pi.abs, (· <$$> ·), ← abs_map]; rfl
end Pi
end MvQPF