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 n → Type u}
[MvFunctor F]
[q : MvQPF F]
{G : TypeVec n → Type u}
[MvFunctor G]
{FG_abs : {α : TypeVec n} → F α → G α}
{FG_repr : {α : TypeVec n} → G α → F α}
(FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs α (FG_repr α x) = x)
(FG_abs_map : ∀ {α β : TypeVec n} (f : TypeVec.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
Instances For
def
MvQPF.Quot1.map
{n : ℕ}
{F : TypeVec n → Type u}
(R : ⦃α : TypeVec n⦄ → F α → F α → Prop)
[MvFunctor F]
(Hfunc : ⦃α β : TypeVec n⦄ → (a b : F α) → (f : TypeVec.Arrow α β) → R α a b → R β (MvFunctor.map f a) (MvFunctor.map f b))
⦃α : TypeVec n⦄
⦃β : TypeVec n⦄
(f : TypeVec.Arrow α β)
:
MvQPF.Quot1 R α → MvQPF.Quot1 R β
Instances For
def
MvQPF.Quot1.mvFunctor
{n : ℕ}
{F : TypeVec n → Type u}
(R : ⦃α : TypeVec n⦄ → F α → F α → Prop)
[MvFunctor F]
(Hfunc : ⦃α β : TypeVec n⦄ → (a b : F α) → (f : TypeVec.Arrow α β) → R α a b → R β (MvFunctor.map f a) (MvFunctor.map f b))
:
MvFunctor (MvQPF.Quot1 R)
mvFunctor
instance for Quot1
with well-behaved R
Instances For
noncomputable def
MvQPF.relQuot
{n : ℕ}
{F : TypeVec n → Type u}
(R : ⦃α : TypeVec n⦄ → F α → F α → Prop)
[MvFunctor F]
[q : MvQPF F]
(Hfunc : ⦃α β : TypeVec n⦄ → (a b : F α) → (f : TypeVec.Arrow α β) → R α a b → R β (MvFunctor.map f a) (MvFunctor.map f b))
:
MvQPF (MvQPF.Quot1 R)
Quot1
is a QPF