Dependent product and sum of QPFs are QPFs #
Dependent sum 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)
Dependent product of an n-ary functor. The sum can range over
data types like ℕ or over Type.{u-1}
instance
MvQPF.Sigma.inhabited
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
{α : TypeVec.{u} n}
[Inhabited A]
[Inhabited (F default α)]
:
Inhabited (MvQPF.Sigma F α)
Equations
- MvQPF.Sigma.inhabited F = { default := ⟨default, default⟩ }
instance
MvQPF.Pi.inhabited
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
{α : TypeVec.{u} n}
[(a : A) → Inhabited (F a α)]
:
Equations
- MvQPF.Pi.inhabited F = { default := fun (_a : A) => default }
instance
MvQPF.Sigma.instMvFunctor
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvFunctor (F α)]
:
MvFunctor (MvQPF.Sigma F)
Equations
- MvQPF.Sigma.instMvFunctor F = { map := fun {α β : TypeVec.{?u.42} n} (f : α.Arrow β) (x : MvQPF.Sigma F α) => match x with | ⟨a, x⟩ => ⟨a, MvFunctor.map f x⟩ }
polynomial functor representation of a dependent sum
Equations
- MvQPF.Sigma.P F = { A := (a : A) × (MvQPF.P (F a)).A, B := fun (x : (a : A) × (MvQPF.P (F a)).A) => (MvQPF.P (F x.fst)).B x.snd }
def
MvQPF.Sigma.abs
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvQPF (F α)]
⦃α : TypeVec.{u} n⦄
:
↑(MvQPF.Sigma.P F) α → MvQPF.Sigma F α
abstraction function for dependent sums
Equations
- MvQPF.Sigma.abs F ⟨a, f⟩ = ⟨a.fst, MvQPF.abs ⟨a.snd, f⟩⟩
def
MvQPF.Sigma.repr
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvQPF (F α)]
⦃α : TypeVec.{u} n⦄
:
MvQPF.Sigma F α → ↑(MvQPF.Sigma.P F) α
representation function for dependent sums
Equations
- MvQPF.Sigma.repr F ⟨a, x_1⟩ = ⟨⟨a, (MvQPF.repr x_1).fst⟩, (MvQPF.repr x_1).snd⟩
instance
MvQPF.Sigma.inst
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvQPF (F α)]
:
MvQPF (MvQPF.Sigma F)
Equations
- MvQPF.Sigma.inst F = MvQPF.mk (MvQPF.Sigma.P F) (fun {α : TypeVec.{?u.37} n} => MvQPF.Sigma.abs F) (fun {α : TypeVec.{?u.37} n} => MvQPF.Sigma.repr F) ⋯ ⋯
instance
MvQPF.Pi.instMvFunctor
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvFunctor (F α)]
:
Equations
- MvQPF.Pi.instMvFunctor F = { map := fun {α β : TypeVec.{?u.39} n} (f : α.Arrow β) (x : MvQPF.Pi F α) (a : A) => MvFunctor.map f (x a) }
polynomial functor representation of a dependent product
def
MvQPF.Pi.abs
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvQPF (F α)]
⦃α : TypeVec.{u} n⦄
:
↑(MvQPF.Pi.P F) α → MvQPF.Pi F α
abstraction function for dependent products
Equations
- MvQPF.Pi.abs F ⟨a, f⟩ = fun (x : A) => MvQPF.abs ⟨a x, fun (i : Fin2 n) (y : (MvQPF.P (F x)).B (a x) i) => f i ⟨x, y⟩⟩
def
MvQPF.Pi.repr
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvQPF (F α)]
⦃α : TypeVec.{u} n⦄
:
MvQPF.Pi F α → ↑(MvQPF.Pi.P F) α
representation function for dependent products
Equations
- MvQPF.Pi.repr F x = ⟨fun (a : A) => (MvQPF.repr (x a)).fst, fun (_i : Fin2 n) (a : (MvQPF.Pi.P F).B (fun (a : A) => (MvQPF.repr (x a)).fst) _i) => (MvQPF.repr (x a.fst)).snd _i a.snd⟩
instance
MvQPF.Pi.inst
{n : ℕ}
{A : Type u}
(F : A → TypeVec.{u} n → Type u)
[(α : A) → MvQPF (F α)]
:
Equations
- MvQPF.Pi.inst F = MvQPF.mk (MvQPF.Pi.P F) (MvQPF.Pi.abs F) (MvQPF.Pi.repr F) ⋯ ⋯