Dependent product and sum of QPFs are QPFs
Dependent sum of of an n-ary functor. The sum can range over
data types like ℕ or over Type.{u-1}
Equations
- mvqpf.sigma F v = Σ (α : A), F α v
@[instance]
def
mvqpf.sigma.inhabited
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
{α : typevec n}
[inhabited A]
[inhabited (F (inhabited.default A) α)] :
inhabited (mvqpf.sigma F α)
Equations
- mvqpf.sigma.inhabited F = {default := ⟨inhabited.default A _inst_1, inhabited.default (F (inhabited.default A) α) _inst_2⟩}
@[instance]
def
mvqpf.pi.inhabited
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
{α : typevec n}
[Π (a : A), inhabited (F a α)] :
Equations
- mvqpf.pi.inhabited F = {default := λ (a : A), inhabited.default (F a α)}
@[instance]
def
mvqpf.sigma.mvfunctor
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)] :
mvfunctor (mvqpf.sigma F)
Equations
- mvqpf.sigma.mvfunctor F = {map := λ (α β : typevec n) (f : α.arrow β) (_x : mvqpf.sigma F α), mvqpf.sigma.mvfunctor._match_1 F α β f _x}
- mvqpf.sigma.mvfunctor._match_1 F α β f ⟨a, x⟩ = ⟨a, mvfunctor.map f x⟩
def
mvqpf.sigma.P
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)] :
polynomial functor representation of a dependent sum
def
mvqpf.sigma.abs
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)]
⦃α : typevec n⦄ :
(mvqpf.sigma.P F).obj α → mvqpf.sigma F α
abstraction function for dependent sums
def
mvqpf.sigma.repr
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)]
⦃α : typevec n⦄ :
mvqpf.sigma F α → (mvqpf.sigma.P F).obj α
representation function for dependent sums
Equations
- mvqpf.sigma.repr F ⟨a, f⟩ = let x : (mvqpf.P (F a)).obj α := mvqpf.repr f in ⟨⟨a, x.fst⟩, x.snd⟩
@[instance]
def
mvqpf.sigma.mvqpf
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)] :
mvqpf (mvqpf.sigma F)
Equations
- mvqpf.sigma.mvqpf F = {P := mvqpf.sigma.P F (λ (α : A), _inst_2 α), abs := mvqpf.sigma.abs F (λ (α : A), _inst_2 α), repr := mvqpf.sigma.repr F (λ (α : A), _inst_2 α), abs_repr := _, abs_map := _}
@[instance]
def
mvqpf.pi.mvfunctor
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)] :
Equations
- mvqpf.pi.mvfunctor F = {map := λ (α β : typevec n) (f : α.arrow β) (x : mvqpf.pi F α) (a : A), mvfunctor.map f (x a)}
def
mvqpf.pi.P
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)] :
polynomial functor representation of a dependent product
def
mvqpf.pi.abs
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)]
⦃α : typevec n⦄ :
(mvqpf.pi.P F).obj α → mvqpf.pi F α
abstraction function for dependent products
def
mvqpf.pi.repr
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)]
⦃α : typevec n⦄ :
mvqpf.pi F α → (mvqpf.pi.P F).obj α
representation function for dependent products
Equations
- mvqpf.pi.repr F f = ⟨λ (a : A), (mvqpf.repr (f a)).fst, λ (i : fin2 n) (a : (mvqpf.pi.P F).B (λ (a : A), (mvqpf.repr (f a)).fst) i), (mvqpf.repr (f a.fst)).snd i a.snd⟩
@[instance]
def
mvqpf.pi.mvqpf
{n : ℕ}
{A : Type u}
(F : A → typevec n → Type u)
[Π (α : A), mvfunctor (F α)]
[Π (α : A), mvqpf (F α)] :
Equations
- mvqpf.pi.mvqpf F = {P := mvqpf.pi.P F (λ (α : A), _inst_2 α), abs := mvqpf.pi.abs F (λ (α : A), _inst_2 α), repr := mvqpf.pi.repr F (λ (α : A), _inst_2 α), abs_repr := _, abs_map := _}