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 α}
(FG_abs_repr : ∀ {α : typevec n} (x : G α), FG_abs (FG_repr x) = x)
(FG_abs_map : ∀ {α β : typevec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = 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
def
mvqpf.quot1
{n : ℕ}
{F : typevec n → Type u}
(R : Π ⦃α : typevec n⦄, F α → F α → Prop)
(α : typevec n) :
Type u
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 α)
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 : α ⟹ β), R a b → R (f <$$> a) (f <$$> b))
⦃α β : typevec n⦄
(f : α ⟹ β)
(a : 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 (f <$$> x)) _
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 : α ⟹ β), R a b → R (f <$$> a) (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 : α ⟹ β), R a b → R (f <$$> a) (f <$$> b)) :
mvqpf (mvqpf.quot1 R)
quot1 is a qpf
Equations
- mvqpf.rel_quot R Hfunc = mvqpf.quotient_qpf _ _