Merge pull request #1786 from jdchristensen/join-id-sym

trijoin_id_sym is natural; export more from HSpace/Core

theories/Homotopy/HSpace/Core.v

@@ -1,5 +1,7 @@
 Require Export Classes.interfaces.canonical_names (SgOp, sg_op,
-    MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity).
+    MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity,
+    Negate, negate, Associative, simple_associativity, associativity,
+    LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity).
 Require Classes.interfaces.canonical_names.
 Export canonical_names.BinOpNotations.
 Require Import Basics Types Pointed WildCat.

theories/Homotopy/Join/Core.v

@@ -410,31 +410,40 @@ Section Triangle.
   Context {A B : Type}.
 
   Definition triangle_h {a a' : A} (b : B) (p : a = a')
-    : jglue a b @ (jglue a' b)^ = ap joinl p.
+    : ap joinl p @ (jglue a' b) = jglue a b.
   Proof.
     destruct p.
-    apply concat_pV.
+    apply concat_1p.
   Defined.
 
   Definition triangle_h' {a a' : A} (b : B) (p : a = a')
-    : ap joinl p @ (jglue a' b) = jglue a b.
+    : jglue a b @ (jglue a' b)^ = ap joinl p.
   Proof.
     destruct p.
-    apply concat_1p.
+    apply concat_pV.
   Defined.
 
   Definition triangle_v (a : A) {b b' : B} (p : b = b')
-    : (jglue a b)^ @ jglue a b' = ap joinr p.
+    : jglue a b @ ap joinr p = jglue a b'.
   Proof.
     destruct p.
-    apply concat_Vp.
+    apply concat_p1.
   Defined.
 
   Definition triangle_v' (a : A) {b b' : B} (p : b = b')
-    : jglue a b @ ap joinr p = jglue a b'.
+    : (jglue a b)^ @ jglue a b' = ap joinr p.
   Proof.
     destruct p.
-    apply concat_p1.
+    apply concat_Vp.
+  Defined.
+
+  (** For just one of the above, we give a rule for how it behaves on inverse paths. *)
+  Definition triangle_v_V (a : A) {b b' : B} (p : b = b')
+    : triangle_v a p^ = (1 @@ ap_V joinr p) @ moveR_pV _ _ _ (triangle_v a p)^.
+  Proof.
+    induction p; cbn.
+    rhs nrapply concat_1p.
+    symmetry; apply concat_pV_p.
   Defined.
 
 End Triangle.
@@ -732,7 +741,7 @@ Section JoinTrunc.
     - intros b; apply jglue.
     - intros a b; cbn.
       lhs nrapply transport_paths_r.
-      apply triangle_h'.
+      apply triangle_h.
   Defined.
 
   (** The join of hprops is an hprop *)

theories/Homotopy/Join/JoinAssoc.v

@@ -146,9 +146,15 @@ Definition equiv_trijoin_twist (A B C : Type)
 
 (** ** The associativity of [Join] *)
 
+(** [trijoin_twist] corresponds to the permutation (1,2).  The equivalence corresponding to the permutation (2,3) also plays a key role, so we name it here. *)
+Definition trijoin_id_sym A B C : TriJoin A B C <~> TriJoin A C B
+  := equiv_functor_join equiv_idmap (equiv_join_sym B C).
+
+Arguments trijoin_id_sym : simpl never.
+
 Definition join_assoc A B C : Join A (Join B C) <~> Join (Join A B) C.
 Proof.
-  refine (_ oE equiv_functor_join equiv_idmap (equiv_join_sym B C)).
+  refine (_ oE trijoin_id_sym _ _ _).
   refine (_ oE equiv_trijoin_twist _ _ _).
   apply equiv_join_sym.
 Defined.
@@ -206,16 +212,42 @@ Proof.
   apply trijoin_twist_nat'.
 Defined.
 
+(** ** Naturality of [trijoin_id_sym] *)
+
+(** Naturality of [trijoin_id_sym], using [functor_join].  In this case, it's easier to do this version first. *)
+Definition trijoin_id_sym_nat {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
+  : trijoin_id_sym A' B' C' o functor_join f (functor_join g h)
+    == functor_join f (functor_join h g) o trijoin_id_sym A B C.
+Proof.
+  intro x; simpl.
+  lhs_V nrapply functor_join_compose.
+  rhs_V nrapply functor_join_compose.
+  apply functor2_join.
+  - reflexivity.
+  - apply join_sym_nat.
+Defined.
+
+(** Naturality of [trijoin_id_sym], using [functor_trijoin]. *)
+Definition trijoin_id_sym_nat' {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
+  : trijoin_id_sym A' B' C' o functor_trijoin f g h
+    == functor_trijoin f h g o trijoin_id_sym A B C.
+Proof.
+  intro x.
+  lhs_V nrefine (ap _ (functor_trijoin_as_functor_join f g h x)).
+  rhs_V nrapply functor_trijoin_as_functor_join.
+  apply trijoin_id_sym_nat.
+Defined.
+
 (** ** Naturality of [join_assoc] *)
 
-(** Since [join_assoc] is a composite of [trijoin_twist] and [join_sym], we just use their naturality. *)
+(** Since [join_assoc] is a composite of [join_sym], [trijoin_twist] and [trijoin_id_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.
+  unfold join_assoc; cbn.
   (* First we pass the [functor_joins]s through the outer [join_sym]. *)
   rhs_V nrapply join_sym_nat.
   (* Strip off the outer [join_sym]. *)
@@ -224,12 +256,8 @@ Proof.
   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.
+  (* Finally, we pass the [functor_join]s through [trijoin_id_sym]. *)
+  apply trijoin_id_sym_nat.
 Defined.
 
 Global Instance join_associator : Associator Type Join.
@@ -293,7 +321,9 @@ Defined.
 
 (** ** The hexagon axiom *)
 
-(** This describes the transformation on [TriJoinRecData] corresponding to precomposition with [functor_join idmap (join_sym C B)], as in the next result. *)
+(** For the hexagon, we'll need to know how to compose [trijoin_id_sym] with something of the form [trijoin_rec f]. For some reason, the proof is harder than it was for [trijoin_twist]. *)
+
+(** This describes the transformation on [TriJoinRecData] corresponding to precomposition with [trijoin_id_sym], as in the next result. *)
 Definition trijoinrecdata_id_sym {A B C P} (f : TriJoinRecData A B C P)
   : TriJoinRecData A C B P.
 Proof.
@@ -305,9 +335,9 @@ Proof.
     apply (j123 f).
 Defined.
 
-(** This is analogous to [trijoin_rec_trijoin_twist] above, with [trijoin_twist] replaced by [join_sym]. *)
+(** This is analogous to [trijoin_rec_trijoin_twist] above, with [trijoin_twist] replaced by [trijoin_id_sym]. *)
 Definition trijoin_rec_id_sym {A B C P} (f : TriJoinRecData A C B P)
-  : trijoin_rec f o functor_join idmap (join_sym B C) == trijoin_rec (trijoinrecdata_id_sym f).
+  : trijoin_rec f o trijoin_id_sym A B C == trijoin_rec (trijoinrecdata_id_sym f).
 Proof.
   (* First we use [functor_join_join_rec] on the LHS. *)
   etransitivity.
@@ -350,10 +380,10 @@ Defined.
         v                            v
     B * (A * C) -> B * (C * A) -> C * (B * A)
 >>
-Here every arrow is either [trijoin_twist _ _ _] or [functor_join idmap (join_sym _ _)], and they alternate as you go around.  These correspond to the permutations (1,2) and (2,3) in the symmetric group on three letters.  We already know that they are their own inverses, i.e., they have order two.  The above says that the composite (1,2)(2,3) has order three.  These are the only relations in this presentation of [S_3].  Note also that every object in this diagram is parenthesized in the same way.  That will be important in our proof. *)
+Here every arrow is either [trijoin_twist _ _ _] or [trijoin_id_sym _ _ _], and they alternate as you go around.  These correspond to the permutations (1,2) and (2,3) in the symmetric group on three letters.  We already know that they are their own inverses, i.e., they have order two.  The above says that the composite (1,2)(2,3) has order three.  These are the only relations in this presentation of [S_3].  Note also that every object in this diagram is parenthesized in the same way.  That will be important in our proof. *)
 Definition hexagon_join_twist_sym A B C
-  : functor_join idmap (join_sym A B) o trijoin_twist A C B o functor_join idmap (join_sym B C)
-    == trijoin_twist B C A o functor_join idmap (join_sym A C) o trijoin_twist A B C.
+  : trijoin_id_sym C A B o trijoin_twist A C B o trijoin_id_sym A B C
+    == trijoin_twist B C A o trijoin_id_sym B A C o trijoin_twist A B C.
 Proof.
   (* It's enough to show that both sides induces the same natural transformation under the covariant Yoneda embedding, i.e., after postcomposing with a general function [f]. *)
   rapply (opyon_faithful_0gpd (A:=Type)).
@@ -401,9 +431,9 @@ Defined.
          v              v              v
     (A * C) * B -> B * (A * C) -> (B * A) * C
 >>
-The right-hand square is a horizontally-compressed version of the rectangle from the previous result, whose horizontal arrows are associativity. In the left-hand square, the new vertical map is [join_assoc A C B] and the horizontal maps are [functor_join idmap (join_sym _ _)] and [join_sym _ _]. *)
+The right-hand square is a horizontally-compressed version of the rectangle from the previous result, whose horizontal arrows are associativity. In the left-hand square, the new vertical map is [join_assoc A C B] and the horizontal maps are [trijoin_id_sym A C B] and [join_sym (Join A C) B]. *)
 Definition hexagon_join_assoc_sym A B C
-  : functor_join (join_sym A B) idmap o join_assoc A B C o functor_join idmap (join_sym C B)
+  : functor_join (join_sym A B) idmap o join_assoc A B C o trijoin_id_sym A C B
     == join_assoc B A C o join_sym (Join A C) B o join_assoc A C B.
 Proof.
   intro x.

theories/Homotopy/Join/TriJoin.v

@@ -15,7 +15,7 @@ Section TriJoinStructure.
   Definition join12 : forall a b, join1 a = join2 b := fun a b => jglue a (joinl b).
   Definition join13 : forall a c, join1 a = join3 c := fun a c => jglue a (joinr c).
   Definition join23 : forall b c, join2 b = join3 c := fun b c => ap joinr (jglue b c).
-  Definition join123 : forall a b c, join12 a b @ join23 b c = join13 a c := fun a b c => triangle_v' a (jglue b c).
+  Definition join123 : forall a b c, join12 a b @ join23 b c = join13 a c := fun a b c => triangle_v a (jglue b c).
 End TriJoinStructure.
 
 Arguments TriJoin A B C : clear implicits.
@@ -28,7 +28,7 @@ Definition ap_triangle {X Y} (f : X -> Y)
   : ap f ab @ ap f bc = ap f ac
   := (ap_pp f ab bc)^ @ ap (ap f) abc.
 
-(** This general result abstracts away the situation where [J] is [TriJoin A B C], [a] is [joinl a'] for some [a'], [jr] is [joinr : Join B C -> J], [jg] is [fun w => jglue a' w], and [p] is [jglue b c].  By working in this generality, we can do induction on [p].  This also allows us to inline the proof of [triangle_v']. *)
+(** This general result abstracts away the situation where [J] is [TriJoin A B C], [a] is [joinl a'] for some [a'], [jr] is [joinr : Join B C -> J], [jg] is [fun w => jglue a' w], and [p] is [jglue b c].  By working in this generality, we can do induction on [p].  This also allows us to inline the proof of [triangle_v]. *)
 Definition ap_trijoin_general {J W P : Type} (f : J -> P)
   (a : J) (jr : W -> J) (jg : forall w, a = jr w)
   {b c : W} (p : b = c)
@@ -80,7 +80,7 @@ Defined.
 
 Definition ap_trijoin_V {A B C P : Type} (f : TriJoin A B C -> P)
   (a : A) (b : B) (c : C)
-  : ap_triangle f (triangle_v' a (jglue b c)^)
+  : ap_triangle f (triangle_v a (jglue b c)^)
      = (1 @@ (ap (ap f) (ap_V joinr _) @ ap_V f _)) @ moveR_pV _ _ _ (ap_trijoin f a b c)^.
 Proof.
   nrapply ap_trijoin_general_V.
@@ -94,7 +94,7 @@ Local Definition trijoin_ind_helper {A BC : Type} (P : Join A BC -> Type)
   (j1' : P (joinl a)) (j2' : P (joinr b)) (j3' : P (joinr c))
   (j12' : jglue a b # j1' = j2') (j13' : jglue a c # j1' = j3') (j23' : (ap joinr bc) # j2' = j3')
   (j123' : transport_pp _ (jglue a b) (ap joinr bc) j1' @ ap (transport _ (ap joinr bc)) j12' @ j23'
-           = transport2 _ (triangle_v' a bc) _ @ j13')
+           = transport2 _ (triangle_v a bc) _ @ j13')
   : ((apD (fun x : BC => transport P (jglue a x) j1') bc)^
        @ ap (transport (fun x : BC => P (joinr x)) bc) j12')
       @ ((transport_compose P joinr bc j2') @ j23') = j13'.
@@ -830,11 +830,11 @@ Definition equiv_functor_trijoin {A B C A' B' C'}
 (** 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
+  : 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'.
+       @ triangle_v (f a) bc'.
 Proof.
   induction bc, beta_jg; simpl.
   transitivity (concat_p1 _ @ functor_join_beta_jglue f g a b).
@@ -853,7 +853,7 @@ Definition functor_join_join_rec {A B C A' P} (f : A -> A') (g : JoinRecData B C
                       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); |}.
+                      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 _) _ _ _).
@@ -870,7 +870,7 @@ Proof.
     refine (ap (ap joinr) _).
     apply join_rec_beta_jg.
   - unfold prism'.
-    change (join123 a b c) with (triangle_v' a (jglue b c)).
+    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.