The quotient of QPF is itself a QPF

The quotients are here defined using a surjective function and its right inverse. They are very similar to the abs and repr functions found in the definition of MvQPF

def MvQPF.quotientQPF {n : ℕ} {F : TypeVec.{u} n → Type u} [q : MvQPF F] {G : TypeVec.{u} n → Type u} [MvFunctor G] {FG_abs : {α : TypeVec.{u} n} → F α → G α} {FG_repr : {α : TypeVec.{u} n} → G α → F α} (FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α.Arrow β) (x : F α), FG_abs (MvFunctor.map f x) = MvFunctor.map f (FG_abs x)) : MvQPF G

If F is a QPF then G is a QPF as well. Can be used to construct MvQPF instances by transporting them across surjective functions

Equations

• One or more equations did not get rendered due to their size.

def MvQPF.Quot1 {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) (α : TypeVec.{u} n) : Type u

Functorial quotient type

Equations

• MvQPF.Quot1 R α = Quot R

instance MvQPF.Quot1.inhabited {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) {α : TypeVec.{u} n} [Inhabited (F α)] : Inhabited (Quot1 R α)

Equations

• MvQPF.Quot1.inhabited R = { default := Quot.mk R default }

def MvQPF.Quot1.map {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) [MvFunctor F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) ⦃α β : TypeVec.{u} n⦄ (f : α.Arrow β) : Quot1 R α → Quot1 R β

map of the Quot1 functor

Equations

• MvQPF.Quot1.map R Hfunc f = Quot.lift (fun (x : F α) => Quot.mk R (MvFunctor.map f x)) ⋯

def MvQPF.Quot1.mvFunctor {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) [MvFunctor F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) : MvFunctor (Quot1 R)

mvFunctor instance for Quot1 with well-behaved R

Equations

• MvQPF.Quot1.mvFunctor R Hfunc = { map := MvQPF.Quot1.map R Hfunc }

noncomputable def MvQPF.relQuot {n : ℕ} {F : TypeVec.{u} n → Type u} (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) [q : MvQPF F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) : MvQPF (Quot1 R)

Quot1 is a QPF

Equations

• MvQPF.relQuot R Hfunc = MvQPF.quotientQPF ⋯ ⋯