theories/Pointed/Core.v

@@ -599,27 +599,6 @@ Defined.
 Definition path_zero_morphism_pconst (A B : pType)
   : (@pconst A B) = zero_morphism := idpath.
 
-Instance Is0Bifunctor_ptype_comp (A B C : pType)
-  : Is0Bifunctor (cat_comp (A:= pType)(a:=A)(b:=B)(c:=C)).
-Proof.
-  apply Build_Is0Bifunctor''; constructor; intros.
-  - by apply pmap_postwhisker.
-  - by apply pmap_prewhisker.
-Defined.
-
-Instance isTruncatedBicat_ptype : IsTruncatedBicat pType.
-Proof.
-  snrapply Build_IsTruncatedBicat.
-  - exact _.
-  - exact _.
-  - intros A B C D f g h. apply pmap_compose_assoc.
-  - intros; symmetry; apply pmap_compose_assoc.
-  - intros. apply pmap_postcompose_idmap.
-  - intros. symmetry; apply pmap_postcompose_idmap.
-  - intros. apply pmap_precompose_idmap.
-  - intros; symmetry; apply pmap_precompose_idmap.
-Defined.
-
 (** pForall is a 1-category *)
 Instance is1cat_pforall (A : pType) (P : pFam A) : Is1Cat (pForall A P) | 10.
 Proof.
@@ -645,84 +624,81 @@ Defined.
 Instance is3graph_ptype : Is3Graph pType
   := fun f g => is2graph_pforall _ _.
 
-Instance is1Bifunctor_ptype_comp (A B C : pType): Is1Bifunctor (cat_comp (a:=A) (b:=B) (c:=C)).
+Instance is21cat_ptype : Is21Cat pType.
 Proof.
-  snrapply Build_Is1Bifunctor''.
-  - intro g. apply Build_Is1Functor.
-    + intros f f' h h' eq_h. simpl. srapply Build_pHomotopy.
-      * intro. apply (ap (ap g)). apply eq_h.
-      * by pelim eq_h h h' f f' g.
-    + intro f; srapply Build_pHomotopy.
-      * reflexivity.
-      * by pelim f g.
-    + intros f0 f1 f2 alpha beta. srapply Build_pHomotopy.
-      * intro. cbn; exact (ap_pp _ _ _).
-      * by pelim beta alpha f0 f1 f2 g.
-  - intro f. apply Build_Is1Functor.
-    + intros g g' h h' eqh. simpl.
+  unshelve econstructor.
+  - exact _.
+  - intros A B C f; napply Build_Is1Functor.
+    + intros g h p q r.
       srapply Build_pHomotopy.
-      * intro. simpl. apply eqh.
-      * cbn beta zeta. by pelim f eqh h h' g g'.
-    + intro g. srapply Build_pHomotopy.
-      * reflexivity.
-      * destruct f as [f f_eq], g as [g g_eq]. simpl in *.
-        destruct f_eq, g_eq; reflexivity.
-    + intros g0 g1 g2 alpha beta. simpl. snrapply Build_pHomotopy.
-      * reflexivity.
-      * by pelim f beta alpha g0 g1 g2.
-  - intros g g' beta f f' alpha.
-    simpl.
-    unfold pmap_compose, fmap10, fmap01; simpl.
+      1: exact (fun _ => ap _ (r _)).
+      by pelim r p q g h f.
+    + intros g.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim g f.
+    + intros g h i p q.
+      srapply Build_pHomotopy.
+      1: cbn; exact (fun _ => ap_pp _ _ _).
+      by pelim p q g h i f.
+  - intros A B C f; napply Build_Is1Functor.
+    + intros g h p q r.
+      srapply Build_pHomotopy.
+      1: intro; exact (r _).
+      by pelim f r p q g h.
+    + intros g.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim f g.
+    + intros g h i p q.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim f p q i g h.
+  - intros A B C f g h k p q.
+    snapply Build_pHomotopy.
+    + intros x.
+      exact (concat_Ap q _)^.
+    + by pelim p f g q h k.
+  - intros A B C D f g.
+    snapply Build_Is1Natural.
+    intros r1 r2 s1.
     srapply Build_pHomotopy.
-    * simpl. intro x. symmetry; apply concat_Ap.
-    * by pelim alpha f f' beta g g'.
-Defined.
-
-Instance isbicat_ptype : IsBicategory pType.
-Proof.
-  snrapply Build_IsBicategory.
-  1-3: exact _.
-  - intros; constructor.
-    + unfold bicat_assoc_opp; symmetry.
-      apply (phomotopy_compose_pV (pmap_compose_assoc h g f)).
-    + unfold bicat_assoc_opp; symmetry; apply (phomotopy_compose_Vp).
-  - intros; constructor; unfold bicat_idl_opp; symmetry.
-    + apply (phomotopy_compose_pV).
-    + apply (phomotopy_compose_Vp).
-  - intros; constructor; unfold bicat_idr_opp; symmetry.
-    + apply (phomotopy_compose_pV).
-    + apply (phomotopy_compose_Vp).
-  - intros a b c d. snrapply Build_Is1Natural.
-    intros ((h, g), f) ((h',g'),f') ((tau,sigma),rho). simpl in *.
-    snrapply Build_pHomotopy.
-    + simpl. intro x.
-      rewrite concat_1p, concat_p1.
-      rewrite ap_compose.
-      rewrite concat_p_pp.
-      apply (ap (fun z => z @ tau (g' (f' x)))).
-      rewrite <- ap_pp.
-      reflexivity.
-    + pelim rho f f' sigma g g' tau.
-      by pelim h h'.
-  - intros a b; snrapply Build_Is1Natural.
-    intros f f' h; snrapply Build_pHomotopy.
-    + intro; simpl; by autorewrite with paths.
-    + by pelim h f f'.
-  - intros a b; snrapply Build_Is1Natural.
-    intros f f' h; snrapply Build_pHomotopy.
-    + intro; simpl; by autorewrite with paths.
-    + by pelim h f f'.
-  - intros a b c d e f g h k.
-    snrapply Build_pHomotopy.
-    + reflexivity.
-    + by pelim f g h k.
-  - intros a b c f g. snrapply Build_pHomotopy.
-    + reflexivity.
-    + by pelim f g.
+    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
+    by pelim f g s1 r1 r2.
+  - intros A B C D f g.
+    snapply Build_Is1Natural.
+    intros r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
+    by pelim f s1 r1 r2 g.
+  - intros A B C D f g.
+    snapply Build_Is1Natural.
+    intros r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: cbn; exact (fun _ => concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
+    by pelim s1 r1 r2 f g.
+  - intros A B.
+    snapply Build_Is1Natural.
+    intros r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: exact (fun _ => concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
+    by pelim s1 r1 r2.
+  - intros A B.
+    snapply Build_Is1Natural.
+    intros r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
+    simpl; by pelim s1 r1 r2.
+  - intros A B C D E f g h j.
+    srapply Build_pHomotopy.
+    1: reflexivity.
+    by pelim f g h j.
+  - intros A B C f g.
+    srapply Build_pHomotopy.
+    1: reflexivity.
+    by pelim f g.
 Defined.
 
-Global Instance is21cat_ptype : Is21Cat pType := {}.
-
 (** The forgetful map from pType to Type is a 0-functor *)
 Instance is0functor_pointed_type : Is0Functor pointed_type.
 Proof.
@@ -766,7 +742,7 @@ Proof.
   intros I x.
   snapply Build_Product.
   - exact (pproduct x).
-  - exact pproduct_proj.
+  - exact pproduct_proj. 
   - exact (pproduct_corec x).
   - intros Z f i.
     snapply Build_pHomotopy.

theories/WildCat/Core.v

@@ -173,17 +173,6 @@ Record RetractionOf {A} `{Is1Cat A} {a b : A} (f : a $-> b) :=
     is_retraction : comp_left_inverse $o f $== Id a
   }.
 
-Record AreInverse {A} `{Is1Cat A} {a b : A} (f : a $->b) (g : b $->a) := {
-  gf_id : Id a $== g $o f;
-  fg_id : Id b $== f $o g
-}.
-
-Definition inverse_op {A} `{Is1Cat A} {a b : A} (f : a $-> b) (g : b $->a) (p : AreInverse f g) : AreInverse g f :=
-{|
-  gf_id := fg_id _ _ p;
-  fg_id := gf_id _ _ p
-|}.
-
 (** Often, the coherences are actually equalities rather than homotopies. *)
 Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
 {

theories/WildCat/Paths.v

@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.
-Require Import WildCat.Core WildCat.TwoOneCat WildCat.NatTrans WildCat.Bifunctor.
+Require Import WildCat.Core WildCat.TwoOneCat WildCat.NatTrans.
 
 (** * Path groupoids as wild categories *)
 
@@ -48,11 +48,6 @@ Proof.
   exact (@ap _ _ (cat_precomp c f)).
 Defined.
 
-(** Composition is a 0-bifunctor when the 2-cells are paths. *)
-Instance is0bifunctor_cat_comp_paths (A :Type) `{Is01Cat A} (a b c :A)
-    : Is0Bifunctor (cat_comp (a:=a) (b:=b) (c:=c))
-    := Build_Is0Bifunctor'' _ .
-
 (** Any type is a 1-category with n-morphisms given by paths. *)
 Instance is1cat_paths {A : Type} : Is1Cat A.
 Proof.
@@ -67,20 +62,6 @@ Proof.
   - exact (@concat_1p A).
 Defined.
 
-Instance IsTruncatedBicat_paths (A: Type) : IsTruncatedBicat A.
-Proof.
-  snrapply Build_IsTruncatedBicat.
-  - exact _.
-  - intros a b c. simpl. change concatR with (cat_comp (a:=a) (b:=b) (c:=c)).
-    rapply is0bifunctor_cat_comp_paths.
-  - intros a b c d; apply concat_p_pp.
-  - intros a b c d; apply concat_pp_p.
-  - intros a b f; apply concat_p1.
-  - intros a b f; symmetry; apply concat_p1.
-  - intros a b f; apply concat_1p.
-  - intros a b f; symmetry; apply concat_1p.
-Defined.
-
 (** Any type is a 1-groupoid with morphisms given by paths. *)
 Instance is1gpd_paths {A : Type} : Is1Gpd A.
 Proof.
@@ -89,49 +70,55 @@ Proof.
   - exact (@concat_Vp A).
 Defined.
 
-Instance Is1Bifunctor_cat_comp_paths (A: Type) (a b c : A)
-  : Is1Bifunctor (cat_comp (a:=a) (b:=b) (c:=c)).
+(** Any type is a 2-category with higher morphhisms given by paths. *)
+Instance is21cat_paths {A : Type} : Is21Cat A.
 Proof.
-  apply Build_Is1Bifunctor''.
-  - intro q. snrapply Build_Is1Functor.
-    + intros ? ? ? ?. exact( (ap (fun x => whiskerR x _))).
+  snapply Build_Is21Cat.
+  - exact _.
+  - exact _.
+  - intros x y z p.
+    snapply Build_Is1Functor.
+    + intros a b q r.
+      exact (ap (fun x => whiskerR x _)).
     + reflexivity.
-    + intros p0 p1 p2. apply whiskerR_pp.
-  - intro p. snrapply Build_Is1Functor.
-    + intros ? ? ? ?. exact (ap (whiskerL p)).
+    + intros a b c.
+      exact (whiskerR_pp p).
+  - intros x y z p.
+    snapply Build_Is1Functor.
+    + intros a b q r.
+      exact (ap (whiskerL p)).
     + reflexivity.
-    + intros p0 p1 p2. exact (whiskerL_pp p).
-  - intros q q' beta p p' alpha. exact (concat_whisker _ _ _ _ _ _)^.
-Defined.
-
-(** Any type is a 2-category with higher morphisms given by paths. *)
-Instance is21cat_paths {A : Type} : Is21Cat A.
-Proof.
-  snrapply Build_Is21Cat; [snrapply Build_IsBicategory | | ].
-  1-3, 12-13: exact _.
-  - (* assoc and assoc_opp are inverse *)
-    intros a b c d f g h. constructor; simpl; destruct h, g, f; reflexivity.
-  - (* idl and idl_opp are inverse *)
-    intros a b f; constructor; destruct f; reflexivity.
-  - (* idr and idr_opp are inverse *)
-    intros a b f; constructor; destruct f; reflexivity.
-  - (* assoc is natural *)
-    intros a b c d.
-    snrapply Build_Is1Natural.
-    intros ((h, g), f) ((h', g'), f') ((s,r),q). simpl in s, r, q. simpl.
-    destruct q, s, h, r, g, f; reflexivity.
-  - (* idl is natural *)
-    intros a b; snrapply Build_Is1Natural.
-    intros f f' alpha; destruct alpha, f; reflexivity.
-  - (* idr is natural *)
-    intros a b; snrapply Build_Is1Natural.
-    intros f f' alpha; destruct alpha, f; reflexivity.
-  - (* Pentagon *)
-    intros a b c d e p q r s.
-    symmetry.
-    lhs nrapply concat_p_pp.
-    apply pentagon.
-  - (* Triangle *)
-    intros a b c p q.
+    + intros a b c.
+      exact (whiskerL_pp p).
+  - intros a b c q r s t h g.
+    exact (concat_whisker q r s t h g)^.
+  - intros a b c d q r.
+    snapply Build_Is1Natural.
+    intros s t h.
+    apply concat_p_pp_nat_r.
+  - intros a b c d q r.
+    snapply Build_Is1Natural.
+    intros s t h.
+    apply concat_p_pp_nat_m.
+  - intros a b c d q r.
+    snapply Build_Is1Natural.
+    intros s t h.
+    apply concat_p_pp_nat_l.
+  - intros a b.
+    snapply Build_Is1Natural.
+    intros p q h; cbn.
+    apply moveL_Mp.
+    lhs napply concat_p_pp.
+    exact (whiskerR_p1 h).
+  - intros a b.
+    snapply Build_Is1Natural.
+    intros p q h.
+    apply moveL_Mp.
+    lhs rapply concat_p_pp.
+    exact (whiskerL_1p h).
+  - intros a b c d e p q r s.
+    lhs napply concat_p_pp.
+    exact (pentagon p q r s).
+  - intros a b c p q.
     exact (triangulator p q).
 Defined.