Merge pull request #1783 from jdchristensen/join-assoc-natural

Naturality of join_assoc and trijoin_twist

contrib/SetoidRewrite.v

@@ -200,7 +200,7 @@ Proposition nat_equiv_faithful {A B : Type}
 Proof.
   intros faithful_F x y f g eq_Gf_Gg.
   apply (@fmap _ _ _ _ _ (is0functor_precomp _
-       _ _ (cat_equiv_natequiv F G tau x))) in eq_Gf_Gg.
+       _ _ (cat_equiv_natequiv tau x))) in eq_Gf_Gg.
   cbn in eq_Gf_Gg.
   unfold cat_precomp in eq_Gf_Gg.
   rewrite <- is1natural_natequiv in eq_Gf_Gg.

theories/Basics/PathGroupoids.v

@@ -1021,6 +1021,18 @@ Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q)
 
 (** Some higher coherences *)
 
+Lemma ap_pp_concat_p1 {A B} (f : A -> B) {a b : A} (p : a = b)
+  : ap_pp f p 1 @ concat_p1 (ap f p) = ap (ap f) (concat_p1 p).
+Proof.
+  destruct p; reflexivity.
+Defined.
+
+Lemma ap_pp_concat_1p {A B} (f : A -> B) {a b : A} (p : a = b)
+  : ap_pp f 1 p @ concat_1p (ap f p) = ap (ap f) (concat_1p p).
+Proof.
+  destruct p; reflexivity.
+Defined.
+
 Lemma ap_pp_concat_pV {A B} (f : A -> B) {x y : A} (p : x = y)
 : ap_pp f p p^ @ ((1 @@ ap_V f p) @ concat_pV (ap f p))
   = ap (ap f) (concat_pV p).

theories/Homotopy/Bouquet.v

@@ -37,7 +37,7 @@ Section AssumeUnivalence.
     1: refine (natequiv_prewhisker (natequiv_pointify_r S) ptype_group).
     (** Post-compose with [pequiv_loops_bg_g] *)
     nrefine (natequiv_compose _ _).
-1: rapply (natequiv_postwhisker _ (natequiv_inverse _ _ natequiv_g_loops_bg)).
+1: rapply (natequiv_postwhisker _ (natequiv_inverse natequiv_g_loops_bg)).
     (** Loop-susp adjoint *)
     nrefine (natequiv_compose _ _).
     1: refine (natequiv_prewhisker
@@ -61,7 +61,7 @@ Section AssumeUnivalence.
         (opyon S o group_type)
         (fun G => equiv_pi1bouquet_rec S G).
   Proof.
-    rapply (is1natural_natequiv _ _ (natequiv_pi1bouquet_rec _)).
+    rapply (is1natural_natequiv (natequiv_pi1bouquet_rec _)).
   Defined.
 
   (** We can define the inclusion map by using the previous equivalence on the identity group homomorphism. *)

theories/Homotopy/ClassifyingSpace.v

@@ -589,7 +589,7 @@ Lemma is1natural_equiv_bg_pi1_adjoint_r `{Univalence}
   : Is1Natural (opyon (Pi1 X)) (opyon X o B)
       (equiv_bg_pi1_adjoint X).
 Proof.
-  rapply (is1natural_natequiv _ _ (natequiv_bg_pi1_adjoint X)).
+  rapply (is1natural_natequiv (natequiv_bg_pi1_adjoint X)).
   (** Why so slow? Fixed by making this opaque. *)
   Opaque equiv_bg_pi1_adjoint.
 Defined.

theories/Homotopy/Join/Core.v

@@ -352,7 +352,7 @@ Defined.
 
 (** It will be handy to name the inverse natural equivalence. *)
 Definition join_rec_natequiv (A B : Type)
-  := natequiv_inverse _ _ (join_rec_inv_natequiv A B).
+  := natequiv_inverse (join_rec_inv_natequiv A B).
 
 (** [join_rec_natequiv A B P] is an equivalence of 0-groupoids whose underlying function is definitionally [join_rec]. *)
 Local Definition join_rec_natequiv_check (A B P : Type)
@@ -482,20 +482,19 @@ Defined.
 (** * Functoriality of Join. *)
 Section FunctorJoin.
 
+  (** In some cases, we'll need to refer to the recursion data that defines [functor_join], so we make it a separate definition. *)
+  Definition functor_join_recdata {A B C D} (f : A -> C) (g : B -> D)
+    : JoinRecData A B (Join C D)
+    := {| jl := joinl o f; jr := joinr o g; jg := fun a b => jglue (f a) (g b); |}.
+
   Definition functor_join {A B C D} (f : A -> C) (g : B -> D)
-    : Join A B -> Join C D.
-  Proof.
-    snrapply Join_rec.
-    1: exact (joinl o f).
-    1: exact (joinr o g).
-    intros a b.
-    apply jglue.
-  Defined.
+    : Join A B -> Join C D
+    := join_rec (functor_join_recdata f g).
 
   Definition functor_join_beta_jglue {A B C D : Type} (f : A -> C) (g : B -> D)
     (a : A) (b : B)
     : ap (functor_join f g) (jglue a b) = jglue (f a) (g b)
-    := Join_rec_beta_jglue _ _ _ a b.
+    := join_rec_beta_jg _ a b.
 
   Definition functor_join_compose {A B C D E F}
     (f : A -> C) (g : B -> D) (h : C -> E) (i : D -> F)

theories/Homotopy/Join/JoinAssoc.v

@@ -162,3 +162,70 @@ Proof.
   simpl. refine (_ oE (join_assoc _ _ _)^-1%equiv).
   exact (equiv_functor_join equiv_idmap IHn).
 Defined.
+
+(** ** Naturality of [trijoin_twist] *)
+
+(** Our goal is to prove that [trijoin_twist A' B' C' o functor_join f (functor_join g h)] is homotopic to [functor_join g (functor_join f h) o trijoin_twist A B C]. *)
+
+(** We first give a slightly more general result, which works for anything of the form [trijoin_rec f]. *)
+Definition trijoin_rec_trijoin_twist {A B C P} (f : TriJoinRecData B A C P)
+  : trijoin_rec (trijoinrecdata_twist _ _ _ _ f) == trijoin_rec f o trijoin_twist A B C.
+Proof.
+  (* We first replace [trijoin_twist] with [equiv_trijoin_twist']. *)
+  transitivity (trijoin_rec f o equiv_trijoin_twist' A B C).
+  2: exact (fun x => ap (trijoin_rec f) (trijoin_twist_homotopic A B C x)^).
+  (* The RHS is now the twist natural transformation applied to [Id], followed by postcomposition; naturality states that that is the same as the natural trans applied to [trijoin_rec f]. *)
+  refine (_ $@ isnat_natequiv (trijoinrecdata_fun_twist B A C) (trijoin_rec f) _).
+  (* The RHS simplifies to [trijoinrecdata_fun_twist] applied to [trijoin_rec f].  The former is a composite of [trijoin_rec], [trijoinrecdata_twist] and [trijoin_rec_inv], so we can write the RHS as: *)
+  change (?L $== ?R) with (L $== trijoin_rec (trijoinrecdata_twist B A C P (trijoin_rec_inv (trijoin_rec f)))).
+  refine (fmap trijoin_rec _).
+  refine (fmap (trijoinrecdata_twist B A C P) _).
+  symmetry; apply trijoin_rec_beta.
+Defined.
+
+(** Naturality of [trijoin_twist].  This version uses [functor_trijoin] and simply combines previous results. *)
+Definition trijoin_twist_nat' {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
+  : trijoin_twist A' B' C' o functor_trijoin f g h
+    == functor_trijoin g f h o trijoin_twist A B C.
+Proof.
+  intro x.
+  rhs_V nrapply trijoin_rec_trijoin_twist.
+  nrapply trijoin_rec_functor_trijoin.
+Defined.
+
+(** And now a version using [functor_join]. *)
+Definition trijoin_twist_nat {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
+  : trijoin_twist A' B' C' o functor_join f (functor_join g h)
+    == functor_join g (functor_join f h) o trijoin_twist A B C.
+Proof.
+  intro x.
+  lhs nrefine (ap _ (functor_trijoin_as_functor_join f g h x)).
+  rhs nrapply functor_trijoin_as_functor_join.
+  apply trijoin_twist_nat'.
+Defined.
+
+(** ** Naturality of [join_assoc] *)
+
+(** Since [join_assoc] is a composite of [trijoin_twist] and [join_sym], we just use their naturality. *)
+Definition join_assoc_nat {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
+  : join_assoc A' B' C' o functor_join f (functor_join g h)
+    == functor_join (functor_join f g) h o join_assoc A B C.
+Proof.
+  (* We'll work from right to left, as it is easier to work near the head of a term. *)
+  intro x.
+  unfold join_assoc; simpl.
+  (* First we pass the [functor_joins]s through the outer [join_sym]. *)
+  rhs_V nrapply join_sym_nat.
+  (* Strip off the outer [join_sym]. *)
+  apply (ap _).
+  (* Next we pass the [functor_join]s through [trijoin_twist]. *)
+  rhs_V nrapply trijoin_twist_nat.
+  (* Strip off the [trijoin_twist]. *)
+  apply (ap _).
+  (* Finally, we pass the [functor_join]s through the inner [join_sym]. *)
+  lhs_V nrapply functor_join_compose.
+  rhs_V nrapply functor_join_compose.
+  apply functor2_join.
+  - reflexivity.
+  - apply join_sym_nat.
+Defined.

theories/Homotopy/Join/TriJoin.v

@@ -1,4 +1,4 @@
-Require Import Basics Types WildCat Join.Core.
+Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.
 
 (** * Induction and recursion principles for the triple join
 
@@ -651,7 +651,7 @@ Defined.
 
 (** It will be handy to name the inverse natural equivalence. *)
 Definition trijoin_rec_natequiv (A B C : Type)
-  := natequiv_inverse _ _ (trijoin_rec_inv_natequiv A B C).
+  := natequiv_inverse (trijoin_rec_inv_natequiv A B C).
 
 (** [trijoin_rec_natequiv A B C P] is an equivalence of 0-groupoids whose underlying function is definitionally [trijoin_rec]. *)
 Local Definition trijoin_rec_natequiv_check (A B C P : Type)
@@ -672,3 +672,177 @@ Definition trijoin_rec_nat (A B C : Type) {P Q : Type} (g : P -> Q)
 Proof.
   exact (isnat (trijoin_rec_natequiv A B C) g f).
 Defined.
+
+(** * Functoriality of the triple join *)
+
+(** ** Precomposition of [TriJoinRecData] *)
+
+(** First observe that we can precompose [k : TriJoinRecData] with a triple of maps. *)
+Definition trijoinrecdata_tricomp {A B C A' B' C' P} (k : TriJoinRecData A B C P)
+  (f : A' -> A) (g : B' -> B) (h : C' -> C)
+  : TriJoinRecData A' B' C' P
+  := {| j1 := j1 k o f; j2 := j2 k o g; j3 := j3 k o h;
+       j12 := fun a b => j12 k (f a) (g b);
+       j13 := fun a c => j13 k (f a) (h c);
+       j23 := fun b c => j23 k (g b) (h c);
+       j123 := fun a b c => j123 k (f a) (g b) (h c); |}.
+
+(** Precomposition with a triple respects paths. *)
+Definition trijoinrecdata_tricomp_0fun {A B C A' B' C' P}
+  {k l : TriJoinRecData A B C P} (p : k $== l)
+  (f : A' -> A) (g : B' -> B) (h : C' -> C)
+  : trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp l f g h.
+Proof.
+  (* This line is not needed, but clarifies the proof. *)
+  unfold trijoinrecdata_tricomp; destruct p.
+  snrapply Build_TriJoinRecPath; intros; cbn; apply_hyp.
+  (* E.g., the first goal is [j1 k (f a) = j1 l (f a)], and this is solved by [h1 p (f a)]. We just precompose all fields of [p] with [f], [g] and [h]. *)
+Defined.
+
+(** Homotopies between the triple are also respected. *)
+Definition trijoinrecdata_tricomp2 {A B C A' B' C' P} (k : TriJoinRecData A B C P)
+  {f f' : A' -> A} {g g' : B' -> B} {h h' : C' -> C}
+  (p : f == f') (q : g == g') (r : h == h')
+  : trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp k f' g' h'.
+Proof.
+  snrapply Build_TriJoinRecPath; intros; cbn.
+  - apply ap, p.
+  - apply ap, q.
+  - apply ap, r.
+  - induction (p a), (q b); by apply equiv_p1_1q.
+  - induction (p a), (r c); by apply equiv_p1_1q.
+  - induction (q b), (r c); by apply equiv_p1_1q.
+  - induction (p a), (q b), (r c); apply prism_id.
+Defined.
+
+(** ** Functoriality of [TriJoin] via [functor_trijoin] *)
+
+(** To define [functor_trijoin], we simply precompose the canonical [TriJoinRecData] with [f], [g] and [h]. For example, this has [j1 := join1 o f] and [j12 := fun a b => join12 (f a) (g b)]. *)
+Definition functor_trijoin {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
+  : TriJoin A B C -> TriJoin A' B' C'
+  := trijoin_rec (trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f g h).
+
+(** We use [functor_trijoin] to express a partial functoriality of [trijoin_rec] in [A], [B] and [C]. *)
+Definition trijoin_rec_functor_trijoin {A B C A' B' C' P} (k : TriJoinRecData A' B' C' P)
+  (f : A -> A') (g : B -> B') (h : C -> C')
+  : trijoin_rec k o functor_trijoin f g h == trijoin_rec (trijoinrecdata_tricomp k f g h).
+Proof.
+  (* On the LHS, we use naturality of the [trijoin_rec] inside [functor_trijoin]: *)
+  refine ((trijoin_rec_nat _ _ _ _ _)^$ $@ _).
+  refine (fmap trijoin_rec _).
+  (* Just to clarify to the reader what is going on: *)
+  change (?L $-> ?R) with (trijoinrecdata_tricomp (trijoin_rec_inv (trijoin_rec k)) f g h $-> R).
+  exact (trijoinrecdata_tricomp_0fun (trijoin_rec_beta k) f g h).
+Defined.
+
+(** Now we have all of the tools to efficiently prove functoriality. *)
+
+Definition functor_trijoin_compose {A B C A' B' C' A'' B'' C''}
+  (f : A -> A') (g : B -> B') (h : C -> C')
+  (f' : A' -> A'') (g' : B' -> B'') (h' : C' -> C'')
+  : functor_trijoin (f' o f) (g' o g) (h' o h) == functor_trijoin f' g' h' o functor_trijoin f g h.
+Proof.
+  symmetry.
+  nrapply trijoin_rec_functor_trijoin.
+Defined.
+
+Definition functor_trijoin_idmap {A B C}
+  : functor_trijoin idmap idmap idmap == (idmap : TriJoin A B C -> TriJoin A B C).
+Proof.
+  refine (moveR_equiv_V_0gpd (trijoin_rec_inv_natequiv A B C _) _ _ _).
+  change (trijoinrecdata_trijoin A B C $== trijoinrecdata_fun idmap (trijoinrecdata_trijoin A B C)).
+  symmetry.
+  exact (fmap_id (trijoinrecdata_0gpd A B C) _ (trijoinrecdata_trijoin A B C)).
+Defined.
+
+Definition functor2_trijoin {A B C A' B' C'}
+  {f f' : A -> A'} {g g' : B -> B'} {h h' : C -> C'}
+  (p : f == f') (q : g == g') (r : h == h')
+  : functor_trijoin f g h == functor_trijoin f' g' h'.
+Proof.
+  unfold functor_trijoin.
+  rapply (fmap trijoin_rec).
+  apply (trijoinrecdata_tricomp2 _ p q r).
+Defined.
+
+Global Instance isequiv_functor_trijoin {A B C A' B' C'}
+  (f : A -> A') `{!IsEquiv f}
+  (g : B -> B') `{!IsEquiv g}
+  (h : C -> C') `{!IsEquiv h}
+  : IsEquiv (functor_trijoin f g h).
+Proof.
+  (* This proof is almost identical to the proof of [isequiv_functor_join]. *)
+  snrapply isequiv_adjointify.
+  - apply (functor_trijoin f^-1 g^-1 h^-1).
+  - etransitivity.
+    1: symmetry; apply functor_trijoin_compose.
+    etransitivity.
+    1: exact (functor2_trijoin (eisretr f) (eisretr g) (eisretr h)).
+    apply functor_trijoin_idmap.
+  - etransitivity.
+    1: symmetry; apply functor_trijoin_compose.
+    etransitivity.
+    1: exact (functor2_trijoin (eissect f) (eissect g) (eissect h)).
+    apply functor_trijoin_idmap.
+Defined.
+
+Definition equiv_functor_trijoin {A B C A' B' C'}
+  (f : A <~> A') (g : B <~> B') (h : C <~> C')
+  : TriJoin A B C <~> TriJoin A' B' C'
+  := Build_Equiv _ _ (functor_trijoin f g h) _.
+
+(** ** The relationship between [functor_trijoin] and [functor_join]. *)
+
+(** While [functor_trijoin] is convenient to work with, we want to know that [functor_trijoin f g h] is homotopic to [functor_join f (functor_join g h)].  This is worked out using the next three results. *)
+
+(** A lemma that handles the path algebra in the next result. [BC] here is [Join B C] there, [bc] here is [jglue b c] there, [bc'] here is [jg g b c] there, and [beta_jg] here is [Join_rec_beta_jglue _ _ _ b c] there. *)
+Local Lemma ap_triangle_functor_join {A BC A' P} (f : A -> A') (g : BC -> P)
+  (a : A) {b c : BC} (bc : b = c) (bc' : g b = g c) (beta_jg : ap g bc = bc')
+  : ap_triangle (functor_join f g) (triangle_v' a bc) @ functor_join_beta_jglue f g a c
+    = (functor_join_beta_jglue f g a b
+        @@ ((ap_compose joinr (functor_join f g) bc)^
+             @ (ap_compose g joinr bc @ ap (ap joinr) beta_jg)))
+       @ triangle_v' (f a) bc'.
+Proof.
+  induction bc, beta_jg; simpl.
+  transitivity (concat_p1 _ @ functor_join_beta_jglue f g a b).
+  - refine (_ @@ 1).
+    unfold ap_triangle.
+    apply moveR_Vp; symmetry.
+    exact (ap_pp_concat_p1 (functor_join f g) (jglue a b)).
+  - apply moveR_Mp; symmetry.
+    exact (concat_p_pp _ _ _ @ whiskerR_p1 _).
+Defined.
+
+(** We'll generalize the situation a bit to keep things less verbose.  [join_rec g] here will be [functor_join g h] in the next result.  Maybe this extra generality will also be useful sometime? *)
+Definition functor_join_join_rec {A B C A' P} (f : A -> A') (g : JoinRecData B C P)
+  : functor_join f (join_rec g)
+    == trijoin_rec {| j1 := joinl o f; j2 := joinr o jl g; j3 := joinr o jr g;
+                      j12 := fun a b => jglue (f a) (jl g b);
+                      j13 := fun a c => jglue (f a) (jr g c);
+                      j23 := fun b c => ap joinr (jg g b c);
+                      j123 := fun a b c => triangle_v' (f a) (jg g b c); |}.
+Proof.
+  (* Recall that [trijoin_rec] is defined to be the inverse of [trijoin_rec_inv_natequiv ...]. *)
+  refine (moveL_equiv_V_0gpd (trijoin_rec_inv_natequiv A B C _) _ _ _).
+  (* The next two lines aren't needed, but clarify the goal. *)
+  unfold trijoin_rec_inv_natequiv, equiv_fun_0gpd; simpl.
+  unfold trijoinrecdata_fun, trijoinrecdata_trijoin; simpl.
+  bundle_trijoinrecpath; intros; cbn.
+  - exact (functor_join_beta_jglue f _ a (joinl b)).
+  - exact (functor_join_beta_jglue f _ a (joinr c)).
+  - unfold join23.
+    refine ((ap_compose joinr _ _)^ @ _).
+    simpl.
+    refine (ap_compose _ joinr (jglue b c) @ _).
+    refine (ap (ap joinr) _).
+    apply join_rec_beta_jg.
+  - unfold prism'.
+    change (join123 a b c) with (triangle_v' a (jglue b c)).
+    exact (ap_triangle_functor_join f (join_rec g) a (jglue b c) (jg g b c) (Join_rec_beta_jglue _ _ _ b c)).
+Defined.
+
+Definition functor_trijoin_as_functor_join {A B C A' B' C'}
+  (f : A -> A') (g : B -> B') (h : C -> C')
+  : functor_join f (functor_join g h) == functor_trijoin f g h
+  := functor_join_join_rec f (functor_join_recdata g h).