Library UniMath.Induction.PolynomialAlgebras2Cells
2-cells of algebras over a polynomial functor.
Require Import UniMath.Foundations.All.
Require Import UniMath.Induction.PolynomialFunctors.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.Induction.FunctorAlgebras_legacy.
Local Open Scope cat.
Local Notation "a ;; b" := (funcomp a b).
Section Misc.
Horizontal composition of a path with a function
Definition comppathwithfun {X Y Z : UU} {f_1 f_2 : X → Y} (e: f_1 = f_2) (g: Y → Z)
: f_1 ;; g = f_2 ;; g.
Proof.
induction e.
apply idpath.
Defined.
Horizontal composition of a function with a path
Definition compfunwithpath {X Y Z : UU} (f : X → Y) {g_1 g_2 : Y → Z} (e : g_1 = g_2) :
f ;; g_1 = f ;; g_2.
Proof.
induction e.
apply idpath.
Defined.
Paths and homotopies
We relate operations on paths and on homotopies using function extensionality.
Result of applying toforallpaths to a vertical composition of paths.
First done pointwise then globally.
Definition comppathcomphom {X Y : UU} {f g h : X → Y} (p : f = g) (q : g = h)
: ∏ x : X, (homotcomp (toforallpaths _ f g p) (toforallpaths _ g h q)) x
= toforallpaths _ f h (pathscomp0 p q) x.
Proof.
intros.
induction p.
apply idpath.
Defined.
Definition comppathcomphom2 {X Y : UU} {f g h : X → Y} (p : f = g) (q : g = h)
: homotcomp (toforallpaths _ f g p) (toforallpaths _ g h q)
= λ x : X, toforallpaths _ f h (p @ q) x.
Proof.
intros.
apply funextsec.
intro x.
apply comppathcomphom.
Defined.
Result of applying funextfun on vertical composition of homotopies.
Definition compcomphomcomppath {X Y : UU} {f g h : X → Y} (phi : f ~ g) (psi : g ~ h)
: funextfun _ _ (homotcomp phi psi) = (funextfun _ _ phi) @ (funextfun _ _ psi).
Proof.
set (p := funextfun _ _ phi).
set (q := funextfun _ _ psi).
set (p_flat := toforallpaths _ _ _ p).
set (q_flat := toforallpaths _ _ _ q).
assert (e_1 : p_flat = phi) by (apply (homotweqinvweq (weqtoforallpaths _ f g) phi)).
assert (e_2 : q_flat = psi) by (apply (homotweqinvweq (weqtoforallpaths _ g h) psi)).
apply (transportf (λ u, funextfun f h (homotcomp u psi) = p @ q) e_1).
apply (transportf (λ v, funextfun f h (homotcomp p_flat v) = p @ q) e_2).
assert (e_3 : homotcomp p_flat q_flat = λ x : X, toforallpaths _ f h (p @ q) x)
by apply (comppathcomphom2 p q).
apply (transportb (λ u : f ~ h, funextfun f h u = p @ q) e_3).
apply (pathsinv0 (homotinvweqweq0 (weqtoforallpaths _ f h) (p @ q))).
Defined.
Result of applying toforallpaths to horizontal composition of path with a function.
Definition comparefuncompwithpathwithfuncompwithhomot {X Y Z : UU} {f_1 f_2 : X → Y} (g : Y → Z) (e : f_1 = f_2)
: toforallpaths _ _ _ (comppathwithfun e g) = homotfun (toforallpaths _ _ _ e) g.
Proof.
intros.
induction e.
apply idpath.
Defined.
Result of applying funextfun to horizontal composition of homotopy with a function.
Definition comparefuncompwithpathwithfuncompwithhomot2 {X Y Z : UU} {f_1 f_2 : X → Y} (g : Y → Z) (alpha : f_1 ~ f_2)
: funextfun _ _ (homotfun alpha g) = comppathwithfun (funextfun _ _ alpha) g.
Proof.
set (e := funextfun _ _ alpha).
assert (p_1 : toforallpaths _ _ _ e = alpha)
by apply (homotweqinvweq (weqtoforallpaths _ f_1 f_2) alpha).
assert (p_2 : paths (comppathwithfun e g) (funextfun _ _ (toforallpaths _ _ _ (comppathwithfun e g))))
by apply (homotinvweqweq0 (weqtoforallpaths _ (f_1 ;; g)(f_2 ;; g)) (comppathwithfun e g)).
apply (transportb (λ v, funextfun (f_1 ;; g) (f_2 ;; g) (homotfun alpha g)
= v) p_2).
apply maponpaths.
apply (transportf (λ v, homotfun v g
= toforallpaths _ (f_1 ;; g) (f_2 ;; g) (comppathwithfun e g)) p_1).
apply (pathsinv0 (comparefuncompwithpathwithfuncompwithhomot g e)).
Defined.
Result of applying toforallpaths to horizontal composition of a function with a path
Definition comparepathcompwithfunwithhomotcompwithfun {X Y Z : UU} (f : X → Y) {g_1 g_2 : Y → Z} (e : g_1 = g_2)
: toforallpaths _ _ _ (compfunwithpath f e) = funhomot f (toforallpaths _ _ _ e).
Proof.
intros.
induction e.
apply idpath.
Defined.
Result of applying funextfun to horizontal composition of a function with a homotopy
Definition comparehomotopycompwithfunwithpathcompwithfun {X Y Z : UU} (f : X → Y) {g_1 g_2 : Y → Z} (alpha : g_1 ~ g_2)
: funextfun _ _ (funhomot f alpha) = compfunwithpath f (funextfun _ _ alpha).
Proof.
set (e := funextfun _ _ alpha).
set (e_flat := toforallpaths _ _ _ e).
assert (p : e_flat = alpha)
by apply (homotweqinvweq (weqtoforallpaths _ g_1 g_2) alpha).
apply (transportf (λ u, funextfun _ _ (funhomot f u) = compfunwithpath f e) p).
apply (transportb (λ u, funextfun (f ;; g_1) (f ;; g_2) u = compfunwithpath f e)
(! (comparepathcompwithfunwithhomotcompwithfun f e))).
apply (! (homotinvweqweq0 (weqtoforallpaths _ (f ;; g_1) (f ;; g_2)) (compfunwithpath f e))).
Defined.
Sigma-types and identity types
Definition sigmaidtoidsigma {A : UU} {B : A → UU} (c_1 c_2: total2 B)
: total2 (λ v : pr1 c_1 = pr1 c_2, transportf B v (pr2 c_1) = pr2 c_2) → c_1 = c_2.
Proof.
induction c_1 as [a_1 b_1].
induction c_2 as [a_2 b_2].
intro e.
induction e as [u v].
apply (total2_paths2_f u v).
Defined.
Definition idsigmatosigmaid {A : UU} {B : A → UU} (c_1 c_2 : total2 B)
: c_1 = c_2 → total2 (λ v : pr1 c_1 = pr1 c_2, transportf B v (pr2 c_1) = pr2 c_2).
Proof.
intro u.
induction u.
exists (idpath _).
apply idpath.
Defined.
Definition idsigmaidsigma {A : UU} {B : A → UU} (c_1 c_2: total2 B) (e : c_1 = c_2)
: sigmaidtoidsigma c_1 c_2 (idsigmatosigmaid c_1 c_2 e) = e.
Proof.
induction e.
apply idpath.
Defined.
Definition sigmaidsigmaid {A : UU} {B : A → UU} (c_1 c_2: total2 B)
(e : total2 (λ v : pr1 c_1 = pr1 c_2, transportf B v (pr2 c_1) = pr2 c_2))
: idsigmatosigmaid _ _ (sigmaidtoidsigma c_1 c_2 e) = e.
Proof.
induction c_1 as [a_1 b_1].
induction c_2 as [a_2 b_2].
induction e as [u v].
simpl in u, v.
induction u, v.
apply idpath.
Defined.
Definition isweqsigmaidtoidsigma {A : UU} {B : A → UU} (c_1 c_2 : total2 B)
: isweq (sigmaidtoidsigma c_1 c_2).
Proof.
apply (isweq_iso (sigmaidtoidsigma c_1 c_2) (idsigmatosigmaid c_1 c_2)).
apply (sigmaidsigmaid c_1 c_2).
apply (idsigmaidsigma c_1 c_2).
Defined.
Definition weqsigmaidtoidsigma {A : UU} {B : A → UU} (c_1 c_2 : total2 B)
: total2 (λ v : pr1 c_1 = pr1 c_2, transportf B v (pr2 c_1) = pr2 c_2) ≃ (c_1 = c_2).
Proof.
unfold weq.
exists (sigmaidtoidsigma c_1 c_2).
apply isweqsigmaidtoidsigma.
Defined.
End Misc.
Section PolynomialFunctor.
Context {A: UU} (B: A → UU).
Notation P := (polynomial_functor A B).
Action of P on paths
Let P_2 {X Y : UU} {f g : X → Y} (p: f = g): # P f = # P g.
Proof.
apply maponpaths.
assumption.
Defined.
We define an action of P on homotopies. For this we need an auxiliary map.
Definition tau {X Y : UU} {f g : X → Y} (x : A) (u : B x → X) (v : ∏ (y : B x), f (u y) = g (u y))
: x,, u ;; f = tpair (λ a : A, B a → Y) x (u ;; g).
Proof.
apply maponpaths.
apply funextfun.
intro.
apply v.
Defined.
We record the effect of the computation rules on tau.
Definition tau_comp {X Y : UU} {f : X → Y} (x : A) (u : B x → X)
: tau x u (λ y : B x, idpath (f (u y))) = idpath (x ,, u ;; f).
Proof.
unfold tau.
assert (e : idpath (u ;; f) = funextfun _ _ (λ y : B x, idpath (f (u y)))).
{
apply homotinvweqweq0.
}
set (C := λ (p : u ;; f = u ;; f)
, pair_path_in2 (λ a : A, B a → Y) p = idpath _).
apply (transportf C e).
apply idpath.
Defined.
Action of P on homotopies
Definition P_2_h {X Y : UU} {f g : X → Y} (h: f ~ g): # P f ~ # P g.
Proof.
intro c.
induction c as [x u].
apply (tau x u (λ y : B x, h (u y))).
Defined.
The result of applying toforallpaths to P(e), where e is a path
Definition compareP2withP2h {X Y : UU} {f g : X → Y} (e : f = g) :
toforallpaths _ _ _ (P_2 e) = P_2_h (toforallpaths _ _ _ e).
Proof.
induction e.
cbn - [P].
apply funextsec.
intro c.
induction c as [x u].
unfold P_2_h.
apply (transportb (λ e, idpath (# P f (x ,, u)) = e) (tau_comp x u)).
apply idpath.
Defined.
The result of applying P_h(alpha), where alpha is a homotopy
Definition compareP2withP2h2 {X Y : UU} {f g : X → Y} (alpha : f ~ g) :
P_2 (funextfun _ _ alpha) = funextfun _ _ (P_2_h alpha).
Proof.
set (e := funextfun _ _ alpha).
set (e_flat := toforallpaths _ _ _ e).
assert (p_1 : e_flat = alpha).
{
apply (homotweqinvweq (weqtoforallpaths _ f g) alpha).
}
assert (p_2 : funextfun _ _ (P_2_h alpha) = funextfun _ _ (P_2_h e_flat)).
{
do 2 apply maponpaths.
apply (pathsinv0 p_1).
}
apply (transportb (λ u, P_2 e = u) p_2).
assert (p_3 : funextfun _ _ (P_2_h e_flat) = (funextfun _ _ (toforallpaths _ _ _ (P_2 e)))).
{
apply maponpaths.
apply (pathsinv0 (compareP2withP2h e)).
}
apply (transportb (λ u, P_2 e = u) p_3).
apply homotinvweqweq0.
Defined.
The type of algebra 2-cells between two algebra maps. An algebra 2-cell is a pair
consisting of a path between the underlying functions and a path witnessing a coherence
condition
Definition isalg2cell {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY) (e: pr1 ff = pr1 gg)
: UU := pr2 ff @ (comppathwithfun (maponpaths (# P) e) (pr2 YY))
= compfunwithpath (alg_map P XX) e @ (pr2 gg).
Definition algebra_2cell {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY)
: UU := ∑ (e: pr1 ff = pr1 gg), isalg2cell _ _ e.
Analysis of algebra 2-cells
We compare
Using this one shows that two algebra maps are equal iff
there is an algebra 2-cell between them.
Alternative definition of algebra 2-cell. An alternative
algebra 2-cell from (f,s_f) to (g,s_g) is a pair (e,s_e)
where e : f = g and s_e : e!(s_f) = s_g.
- Paths between algebra maps
- Pairs of paths involving transport
- Algebra 2-cells
Definition isalg2cellalt {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY) (e : pr1 ff = pr1 gg)
: UU := transportf (is_algebra_mor P XX YY) e (pr2 ff) = pr2 gg.
Definition algebra_2cellalt {XX YY : algebra_ob P}(ff gg : algebra_mor P XX YY)
: UU := ∑ (e: pr1 ff = pr1 gg), isalg2cellalt ff gg e.
For each e : f = g, the map isalg2cell(e) -→ e!(s_f) = s_g
Definition fiberwise2cellto2cellalt {XX YY: algebra_ob P} (ff gg : algebra_mor P XX YY) (e: pr1 ff = pr1 gg)
: isalg2cell ff gg e → isalg2cellalt ff gg e.
Proof.
induction ff as [f s_f].
induction gg as [g s_g].
simpl in e.
unfold isalg2cellalt.
induction e.
intro p.
change (s_f = s_g).
apply (transportf (λ u, u = s_g) (pathscomp0rid s_f)).
apply p.
Defined.
For each e, the map constructed above is a weak equivalence.
Definition isweqfiberwise2cellto2cellalt {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY) (e : pr1 ff = pr1 gg)
: isweq (fiberwise2cellto2cellalt ff gg e).
Proof.
induction ff as [f s_f].
induction gg as [g s_g].
simpl in e.
unfold fiberwise2cellto2cellalt.
induction e.
simpl.
apply (isweqtransportf (λ u, u = s_g) (pathscomp0rid s_f)).
Defined.
Definition weqfiberwise2cellto2cellalt {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY) (e : pr1 ff = pr1 gg)
: isalg2cell ff gg e ≃ isalg2cellalt ff gg e.
Proof.
exists (fiberwise2cellto2cellalt ff gg e).
apply isweqfiberwise2cellto2cellalt.
Defined.
The map from standard to alternative 2-cells, taking total spaces.
Definition from2cellto2cellalt {XX YY: algebra_ob P} (ff gg : algebra_mor P XX YY)
: algebra_2cell ff gg → algebra_2cellalt ff gg.
Proof.
intro ee.
apply (totalfun _ _ (fiberwise2cellto2cellalt ff gg) ee).
Defined.
This map is a weak equivalence because it is fiberwise a weak equivalence
Definition isweqfrom2cellto2cellalt {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY)
: isweq (from2cellto2cellalt ff gg).
Proof.
apply (isweqfibtototal _ _ (weqfiberwise2cellto2cellalt ff gg)).
Defined.
Definition weqfrom2cellto2cellalt {XX YY: algebra_ob P} (ff gg : algebra_mor P XX YY)
: algebra_2cell ff gg ≃ algebra_2cellalt ff gg.
Proof.
exists (from2cellto2cellalt ff gg).
apply isweqfrom2cellto2cellalt.
Defined.
As a special case of the general results obtained before for Id/Sigma we get
that there is a weak equivalence between alternative algebra 2-cells and paths
between algebra maps.
Definition weqfrom2cellalttoidalgmap {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY)
: algebra_2cellalt ff gg ≃ ff = gg.
Proof.
apply weqsigmaidtoidsigma.
Defined.
Definition weqfromalg2celltoidalgmap {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY)
: algebra_2cell ff gg ≃ ff = gg.
Proof.
exact (weqcomp (weqfrom2cellto2cellalt ff gg) (weqfrom2cellalttoidalgmap ff gg)).
Defined.
Definition weqfromaidalgmaptoalg2cell {XX YY : algebra_ob P} (ff gg : algebra_mor P XX YY)
: weq (ff = gg) (algebra_2cell ff gg).
Proof.
exact (invweq (weqfromalg2celltoidalgmap ff gg)).
Defined.
The type of algebra map homotopies
Definition isalgmaphomotopy {X : UU} {s_X : P X → X} {Y : UU} {s_Y : P Y → Y}
(f : X → Y) (sigma_f : s_X ;; f ~ # P f ;; s_Y)
(g : X → Y) (sigma_g : s_X ;; g ~ # P g ;; s_Y)
(alpha : f ~ g) : UU
:= homotcomp (funhomot s_X alpha) (sigma_g) ~ homotcomp (sigma_f) (homotfun (P_2_h alpha) s_Y).
Definition immisalghomotopy {X : UU} {s_X : P X → X} {Y : UU} {s_Y : P Y → Y}
(f : X → Y) (sigma_f : s_X ;; f ~ # P f ;; s_Y)
(g : X → Y) (sigma_g : s_X ;; g ~ # P g ;; s_Y)
(alpha : f ~ g)
: isalgmaphomotopy f sigma_f g sigma_g alpha
→ homotcomp (funhomot s_X alpha) (sigma_g) = (homotcomp (sigma_f) (homotfun (P_2_h alpha) s_Y)).
Proof.
intro is.
apply funextsec.
intro c.
apply (is c).
Defined.
Definition alghomotopytoalg2cell {X : UU} {s_X : P X → X} {Y : UU} {s_Y : P Y → Y}
(f : X → Y) (sigma_f : s_X ;; f ~ # P f ;; s_Y)
(g : X → Y) (sigma_g : s_X ;; g ~ # P g ;; s_Y)
(alpha : f ~ g)
: isalgmaphomotopy f sigma_f g sigma_g alpha →
isalg2cell (tpair (is_algebra_mor P (X ,, s_X) (tpair _ Y s_Y)) f (funextfun _ _ sigma_f))
(g ,, (funextfun _ _ sigma_g)) (funextfun f g alpha).
Proof.
intro is.
set (s_alpha := immisalghomotopy f sigma_f g sigma_g alpha is).
set (XX := X ,, s_X : algebra_ob P).
set (YY := Y ,, s_Y : algebra_ob P).
set (sigma_f_sharp := (funextfun (s_X ;; f) (# P f ;; s_Y) sigma_f)).
set (sigma_g_sharp := (funextfun (s_X ;; g) (# P g ;; s_Y) sigma_g)).
set (alpha_sharp := (funextfun f g alpha)).
unfold isalg2cell.
simpl.
assert (e_1 : P_2 alpha_sharp = funextfun _ _ (P_2_h alpha)).
{
apply compareP2withP2h2.
}
apply (transportb (λ u, sigma_f_sharp @ (comppathwithfun u s_Y)
= compfunwithpath s_X alpha_sharp @ sigma_g_sharp) e_1).
assert (e_2 : funextfun _ _ (funhomot s_X alpha) = compfunwithpath s_X alpha_sharp).
{
apply comparehomotopycompwithfunwithpathcompwithfun.
}
apply (transportf (λ u, sigma_f_sharp @ (comppathwithfun (funextfun (# P f) (# P g) (P_2_h alpha)) s_Y)
= u @ sigma_g_sharp) e_2).
unfold sigma_g_sharp.
assert (e_3 : funextfun _ _ (homotcomp (funhomot s_X alpha) sigma_g)
= (funextfun _ _ (funhomot s_X alpha)) @ (funextfun _ _ sigma_g)).
{
apply (compcomphomcomppath (funhomot s_X alpha) sigma_g).
}
apply (transportf (λ u, sigma_f_sharp @ (comppathwithfun (funextfun (# P f) (# P g) (P_2_h alpha)) s_Y) = u) e_3).
assert (e_4 : funextfun _ _ (homotfun (P_2_h alpha) s_Y) = comppathwithfun (funextfun _ _ (P_2_h alpha)) s_Y).
{
apply (comparefuncompwithpathwithfuncompwithhomot2 s_Y (P_2_h alpha)).
}
apply (transportf (λ u, sigma_f_sharp @ u
= (funextfun (s_X ;; f) (# P g ;; s_Y) (homotcomp (funhomot s_X alpha) sigma_g))) e_4).
assert (e_5 : sigma_f_sharp @ funextfun _ _ (homotfun (P_2_h alpha) s_Y)
= funextfun _ _ (homotcomp sigma_f (homotfun (P_2_h alpha) s_Y))).
{
apply (pathsinv0 (compcomphomcomppath sigma_f (homotfun (P_2_h alpha) s_Y))).
}
apply (transportb (λ u, u = (funextfun (s_X ;; f) (# P g ;; s_Y)
(homotcomp (funhomot s_X alpha) sigma_g))) e_5).
apply maponpaths.
apply (pathsinv0 s_alpha).
Defined.
End PolynomialFunctor.