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 : Type u} [] [q : ] {G : Type u} [] {FG_abs : {α : } → F αG α} {FG_repr : {α : } → G αF α} (FG_abs_repr : ∀ {α : } (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : } (f : α.Arrow β) (x : F α), FG_abs () = MvFunctor.map f (FG_abs x)) :

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.
Instances For
def MvQPF.Quot1 {n : } {F : Type u} (R : α : ⦄ → F αF αProp) (α : ) :

Functorial quotient type

Equations
Instances For
instance MvQPF.Quot1.inhabited {n : } {F : Type u} (R : α : ⦄ → F αF αProp) {α : } [Inhabited (F α)] :
Equations
def MvQPF.Quot1.map {n : } {F : Type u} (R : α : ⦄ → F αF αProp) [] (Hfunc : ∀ ⦃α β : ⦄ (a b : F α) (f : α.Arrow β), R a bR () ()) ⦃α : ⦃β : (f : α.Arrow β) :

map of the Quot1 functor

Equations
Instances For
def MvQPF.Quot1.mvFunctor {n : } {F : Type u} (R : α : ⦄ → F αF αProp) [] (Hfunc : ∀ ⦃α β : ⦄ (a b : F α) (f : α.Arrow β), R a bR () ()) :

mvFunctor instance for Quot1 with well-behaved R

Equations
Instances For
noncomputable def MvQPF.relQuot {n : } {F : Type u} (R : α : ⦄ → F αF αProp) [] [q : ] (Hfunc : ∀ ⦃α β : ⦄ (a b : F α) (f : α.Arrow β), R a bR () ()) :

Quot1 is a QPF

Equations
Instances For