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.quotient_qpf
{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 α} :
(∀ {α : typevec n} (x : G α), FG_abs (FG_repr x) = x) → (∀ {α β : typevec 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
Functorial quotient type
Equations
- mvqpf.quot1 R α = quot R
@[instance]
def
mvqpf.quot1.inhabited
{n : ℕ}
{F : typevec n → Type u}
(R : Π ⦃α : typevec n⦄, F α → F α → Prop)
{α : typevec n}
[inhabited (F α)] :
inhabited (mvqpf.quot1 R α)
Equations
- mvqpf.quot1.inhabited R = {default := quot.mk R (inhabited.default ((λ (α : typevec n), F α) α))}
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 : α.arrow β), R a b → R (mvfunctor.map f a) (mvfunctor.map f b))
⦃α β : typevec n⦄ :
α.arrow β → mvqpf.quot1 R α → mvqpf.quot1 R β
map of the quot1 functor
Equations
- mvqpf.quot1.map R Hfunc f = quot.lift (λ (x : F α), quot.mk R (mvfunctor.map f x)) _
def
mvqpf.quot1.mvfunctor
{n : ℕ}
{F : typevec n → Type u}
(R : Π ⦃α : typevec n⦄, F α → F α → Prop)
[mvfunctor F] :
(∀ ⦃α β : typevec n⦄ (a b : F α) (f : α.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
Equations
- mvqpf.quot1.mvfunctor R Hfunc = {map := mvqpf.quot1.map R Hfunc}
def
mvqpf.rel_quot
{n : ℕ}
{F : typevec n → Type u}
(R : Π ⦃α : typevec n⦄, F α → F α → Prop)
[mvfunctor F]
[q : mvqpf F]
(Hfunc : ∀ ⦃α β : typevec n⦄ (a b : F α) (f : α.arrow β), R a b → R (mvfunctor.map f a) (mvfunctor.map f b)) :
mvqpf (mvqpf.quot1 R)
quot1 is a qpf
Equations
- mvqpf.rel_quot R Hfunc = mvqpf.quotient_qpf _ _