Stratify cells in wildcat

theories/Algebra/AbGroups/AbelianGroup.v

@@ -94,26 +94,29 @@ Defined.
 (** ** The wild category of abelian groups *)
 
 Global Instance isgraph_abgroup : IsGraph AbGroup
-  := induced_graph abgroup_group.
+  := isgraph_induced abgroup_group.
 
-Global Instance is01cat_AbGroup : Is01Cat AbGroup
-  := induced_01cat abgroup_group.
+Global Instance is01cat_abgroup : Is01Cat AbGroup
+  := is01cat_induced abgroup_group.
 
-Global Instance is01cat_GroupHomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
-  := induced_01cat (@grp_homo_map A B).
+Global Instance is01cat_grouphomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
+  := is01cat_induced (@grp_homo_map A B).
 
-Global Instance is0gpd_GroupHomomorphism {A B : AbGroup}: Is0Gpd (A $-> B)
-  := induced_0gpd (@grp_homo_map A B).
+Global Instance is0gpd_grouphomomorphism {A B : AbGroup} : Is0Gpd (A $-> B)
+  := is0gpd_induced (@grp_homo_map A B).
+
+Global Instance is2graph_abgroup : Is2Graph AbGroup
+  := is2graph_induced abgroup_group.
 
 (** AbGroup forms a 1Cat *)
 Global Instance is1cat_abgroup : Is1Cat AbGroup
-  := induced_1cat _.
+  := is1cat_induced _.
 
 Global Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
-  := induced_hasmorext _.
+  := hasmorext_induced _.
 
 Global Instance hasequivs_abgroup : HasEquivs AbGroup
-  := induced_hasequivs _.
+  := hasequivs_induced _.
 
 (** Zero object of AbGroup *)
 

theories/Algebra/Groups/Group.v

@@ -468,14 +468,17 @@ Global Instance isgraph_group : IsGraph Group
 Global Instance is01cat_group : Is01Cat Group :=
   (Build_Is01Cat Group _ (@grp_homo_id) (@grp_homo_compose)).
 
+Global Instance is2graph_group : Is2Graph Group
+  := fun A B => isgraph_induced (@grp_homo_map A B).
+
 Global Instance isgraph_grouphomomorphism {A B : Group} : IsGraph (A $-> B)
-  := induced_graph (@grp_homo_map A B).
+  := isgraph_induced (@grp_homo_map A B).
 
 Global Instance is01cat_grouphomomorphism {A B : Group} : Is01Cat (A $-> B)
-  := induced_01cat (@grp_homo_map A B).
+  := is01cat_induced (@grp_homo_map A B).
 
 Global Instance is0gpd_grouphomomorphism {A B : Group}: Is0Gpd (A $-> B)
-  := induced_0gpd (@grp_homo_map A B).
+  := is0gpd_induced (@grp_homo_map A B).
 
 Global Instance is0functor_postcomp_grouphomomorphism {A B C : Group} (h : B $-> C)
   : Is0Functor (@cat_postcomp Group _ _ A B C h).

theories/Algebra/Rings/CRing.v

@@ -235,14 +235,14 @@ Global Instance isgraph_cring : IsGraph CRing
 Global Instance is01cat_cring : Is01Cat CRing
   := Build_Is01Cat _ _ rng_homo_id (@rng_homo_compose).
 
-Global Instance isgraph_cringhomomorphism {A B : CRing} : IsGraph (A $-> B)
-  := induced_graph (@rng_homo_map A B).
+Global Instance is2graph_cring : Is2Graph CRing
+  := fun A B => isgraph_induced (@rng_homo_map A B).
 
 Global Instance is01cat_cringhomomorphism {A B : CRing} : Is01Cat (A $-> B)
-  := induced_01cat (@rng_homo_map A B).
+  := is01cat_induced (@rng_homo_map A B).
 
-Global Instance is0gpd_cringhomomorphism {A B : CRing}: Is0Gpd (A $-> B)
-  := induced_0gpd (@rng_homo_map A B).
+Global Instance is0gpd_cringhomomorphism {A B : CRing} : Is0Gpd (A $-> B)
+  := is0gpd_induced (@rng_homo_map A B).
 
 Global Instance is0functor_postcomp_cringhomomorphism {A B C : CRing} (h : B $-> C)
   : Is0Functor (@cat_postcomp CRing _ _ A B C h).

theories/Algebra/Universal/Homomorphism.v

@@ -145,9 +145,9 @@ Proof.
   by apply path_homomorphism.
 Defined.
 
-Global Instance isgraph_homomorphism {σ} (A B : Algebra σ)
-  : IsGraph (A $-> B)
-  := Build_IsGraph _ (fun (f g : A $-> B) => forall s, f s == g s).
+Global Instance is2graph_algebra {σ} : Is2Graph (Algebra σ)
+  := fun A B
+    => Build_IsGraph _ (fun (f g : A $-> B) => forall s, f s == g s).
 
 Global Instance is01cat_homomorphism {σ} (A B : Algebra σ)
   : Is01Cat (A $-> B).

theories/Algebra/ooGroup.v

@@ -289,9 +289,14 @@ End Subgroups.
 
 (** The wild category of oo-groups is induced by the wild category of pTypes *)
 
-Global Instance isgraph_oogroup : IsGraph ooGroup := Build_IsGraph _ ooGroupHom.
-Global Instance is01cat_oogroup : Is01Cat ooGroup := Build_Is01Cat _ _ grouphom_idmap (@grouphom_compose).
-Global Instance is1cat_oogroup : Is1Cat ooGroup := induced_1cat classifying_space.
+Global Instance isgraph_oogroup : IsGraph ooGroup
+  := Build_IsGraph _ ooGroupHom.
+Global Instance is01cat_oogroup : Is01Cat ooGroup
+  := Build_Is01Cat _ _ grouphom_idmap (@grouphom_compose).
+Global Instance is2graph_oogroup : Is2Graph ooGroup
+  := is2graph_induced classifying_space.
+Global Instance is1cat_oogroup : Is1Cat ooGroup
+  := is1cat_induced classifying_space.
 
 (** ** 1-groups as oo-groups *)
 

theories/Homotopy/ExactSequence.v

@@ -90,7 +90,7 @@ Definition iscomplex_cancelR {F X Y Y' : pType}
            (i : F ->* X) (f : X ->* Y) (e : Y <~>* Y') (cx : IsComplex i (e o* f))
   : IsComplex i f :=
   (compose_V_hh e (f o* i))^$ $@ 
-    cat_postwhisker _ ((cat_assoc _ _ _)^$ $@ cx) $@ precompose_pconst _.
+    cat_postwhisker _ ((cat_assoc i _ _)^$ $@ cx) $@ precompose_pconst _.
 
 (** And likewise passage across squares with equivalences *)
 Definition iscomplex_equiv_i {F F' X X' Y : pType}
@@ -211,8 +211,10 @@ Proof.
   pose (I := isexact_equiv_i n i i' g h p f).
   pose (I2 := isexact_homotopic_f n i' q).
   exists (iscomplex_cancelR i' f' k cx_isexact).
-  pose (e := (pequiv_pfiber (id_cate _) k (cat_idr _)^$ : pfiber f' <~>* pfiber (k o* f'))).
-  nrefine (cancelR_isequiv_conn_map n _ e). 1: apply pointed_isequiv.
+  epose (e := (pequiv_pfiber (id_cate _) k (cat_idr (k o* f'))^$
+    : pfiber f' <~>* pfiber (k o* f'))).
+  nrefine (cancelR_isequiv_conn_map n _ e).
+  1: apply pointed_isequiv.
   refine (conn_map_homotopic n (cxfib (cx_isexact)) _ _ _).
   intro u. srapply path_hfiber.
   { reflexivity. }

theories/Pointed/Core.v

@@ -590,9 +590,16 @@ Global Instance is01cat_ptype : Is01Cat pType
   := Build_Is01Cat pType _ (@pmap_idmap) (@pmap_compose).
 
 (** pForall is a graph *)
-Global Instance isgraph_pforall (A : pType) (P : pFam A) : IsGraph (pForall A P)
+Global Instance isgraph_pforall (A : pType) (P : pFam A)
+  : IsGraph (pForall A P)
   := Build_IsGraph _ pHomotopy.
 
+Global Instance is2graph_ptype : Is2Graph pType := fun f g => _.
+
+Global Instance is2graph_pforall (A : pType) (P : pFam A)
+  : Is2Graph (pForall A P)
+  := fun f g => _.
+
 (** pForall is a 0-coherent 1-category *)
 Global Instance is01cat_pforall (A : pType) (P : pFam A) : Is01Cat (pForall A P).
 Proof.
@@ -633,8 +640,9 @@ Defined.
 (** pType has equivalences *)
 Global Instance hasequivs_ptype : HasEquivs pType.
 Proof.
-  srapply (Build_HasEquivs _ _ _ _ pEquiv (fun A B f => IsEquiv f));
-    intros A B f; cbn; intros.
+  srapply (
+    Build_HasEquivs _ _ _ _ _ pEquiv (fun A B f => IsEquiv f));
+  intros A B f; cbn; intros.
   - exact f.
   - exact _.
   - exact (Build_pEquiv _ _ f _).

theories/Pointed/pEquiv.v

@@ -16,7 +16,7 @@ Proof.
 Defined.
 
 (* We can probably get rid of the following notation, and use ^-1$ instead. *)
-Notation "f ^-1*" := (@cate_inv pType _ _ _ hasequivs_ptype _ _ f) : pointed_scope.
+Notation "f ^-1*" := (@cate_inv pType _ _ _ _ hasequivs_ptype _ _ f) : pointed_scope.
 
 (* pointed equivalence is a symmetric relation *)
 Global Instance pequiv_symmetric : Symmetric pEquiv.

theories/WildCat/Core.v

@@ -71,13 +71,16 @@ Class Is0Functor {A B : Type} `{IsGraph A} `{IsGraph B} (F : A -> B)
 
 Arguments fmap {_ _ _ _} F {_ _ _} f.
 
+Class Is2Graph (A : Type) `{IsGraph A}
+  := isgraph_hom : forall (a b : A), IsGraph (a $-> b).
+Global Existing Instance isgraph_hom | 20.
+Typeclasses Transparent Is2Graph.
 
 (** ** Wild 1-categorical structures *)
-Class Is1Cat (A : Type) `{!IsGraph A, !Is01Cat A} :=
+Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
 {
-  isgraph_hom : forall (a b : A), IsGraph (a $-> b) ;
   is01cat_hom : forall (a b : A), Is01Cat (a $-> b) ;
-  isgpd_hom : forall (a b : A), Is0Gpd (a $-> b) ;
+  is0gpd_hom : forall (a b : A), Is0Gpd (a $-> b) ;
   is0functor_postcomp : forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g) ;
   is0functor_precomp : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
   cat_assoc : forall (a b c d : A) (f : a $-> b) (g : b $-> c) (h : c $-> d),
@@ -86,14 +89,13 @@ Class Is1Cat (A : Type) `{!IsGraph A, !Is01Cat A} :=
   cat_idr : forall (a b : A) (f : a $-> b), f $o Id a $== f;
 }.
 
-Global Existing Instance isgraph_hom.
 Global Existing Instance is01cat_hom.
-Global Existing Instance isgpd_hom.
+Global Existing Instance is0gpd_hom.
 Global Existing Instance is0functor_postcomp.
 Global Existing Instance is0functor_precomp.
-Arguments cat_assoc {_ _ _ _ _ _ _ _} f g h.
-Arguments cat_idl {_ _ _ _ _ _} f.
-Arguments cat_idr {_ _ _ _ _ _} f.
+Arguments cat_assoc {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_idl {_ _ _ _ _ _ _} f.
+Arguments cat_idr {_ _ _ _ _ _ _} f.
 
 Definition cat_assoc_opp {A : Type} `{Is1Cat A}
            {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
@@ -123,23 +125,24 @@ Definition cat_prewhisker {A} `{Is1Cat A} {a b c : A}
 Notation "p $@R h" := (cat_prewhisker p h).
 
 (** Often, the coherences are actually equalities rather than homotopies. *)
-Class Is1Cat_Strong (A : Type) `{Is01Cat A} := 
+Class Is1Cat_Strong (A : Type)`{!IsGraph A, !Is2Graph A, !Is01Cat A} := 
 {
-  isgraph_hom_strong : forall (a b : A), IsGraph (a $-> b) ;
   is01cat_hom_strong : forall (a b : A), Is01Cat (a $-> b) ;
-  isgpd_hom_strong : forall (a b : A), Is0Gpd (a $-> b) ;
-  is0functor_postcomp_strong : forall (a b c : A) (g : b $-> c), Is0Functor (cat_postcomp a g) ;
-  is0functor_precomp_strong : forall (a b c : A) (f : a $-> b), Is0Functor (cat_precomp c f) ;
+  is0gpd_hom_strong : forall (a b : A), Is0Gpd (a $-> b) ;
+  is0functor_postcomp_strong : forall (a b c : A) (g : b $-> c),
+    Is0Functor (cat_postcomp a g) ;
+  is0functor_precomp_strong : forall (a b c : A) (f : a $-> b),
+    Is0Functor (cat_precomp c f) ;
   cat_assoc_strong : forall (a b c d : A)
     (f : a $-> b) (g : b $-> c) (h : c $-> d),
-    (h $o g) $o f = h $o (g $o f);
-  cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f;
-  cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f;
+    (h $o g) $o f = h $o (g $o f) ;
+  cat_idl_strong : forall (a b : A) (f : a $-> b), Id b $o f = f ;
+  cat_idr_strong : forall (a b : A) (f : a $-> b), f $o Id a = f ;
 }.
 
-Arguments cat_assoc_strong {_ _ _ _ _ _ _ _} f g h.
-Arguments cat_idl_strong {_ _ _ _ _ _} f.
-Arguments cat_idr_strong {_ _ _ _ _ _} f.
+Arguments cat_assoc_strong {_ _ _ _ _ _ _ _ _} f g h.
+Arguments cat_idl_strong {_ _ _ _ _ _ _} f.
+Arguments cat_idr_strong {_ _ _ _ _ _ _} f.
 
 Definition cat_assoc_opp_strong {A : Type} `{Is1Cat_Strong A}
            {a b c d : A} (f : a $-> b) (g : b $-> c) (h : c $-> d)
@@ -151,9 +154,8 @@ Global Instance is1cat_is1cat_strong (A : Type) `{Is1Cat_Strong A}
 Proof.
   srapply Build_Is1Cat.
   all: intros a b.
-  - apply isgraph_hom_strong.
   - apply is01cat_hom_strong.
-  - apply isgpd_hom_strong.
+  - apply is0gpd_hom_strong.
   - apply is0functor_postcomp_strong.
   - apply is0functor_precomp_strong.
   - intros; apply GpdHom_path, cat_assoc_strong.
@@ -203,9 +205,9 @@ Class Is1Functor {A B : Type} `{Is1Cat A} `{Is1Cat B}
     fmap F (g $o f) $== fmap F g $o fmap F f;
 }.
 
-Arguments fmap2 {A B _ _ _ _ _ _} F {_ _ _ _ _ _} p.
-Arguments fmap_id {A B _ _ _ _ _ _} F {_ _} a.
-Arguments fmap_comp {A B _ _ _ _ _ _} F {_ _ _ _ _} f g.
+Arguments fmap2 {A B _ _ _ _ _ _ _ _} F {_ _ _ _ _ _} p.
+Arguments fmap_id {A B _ _ _ _ _ _ _ _} F {_ _} a.
+Arguments fmap_comp {A B _ _ _ _ _ _ _ _} F {_ _ _ _ _} f g.
 
 (** Identity functor *)
 
@@ -352,3 +354,9 @@ Proof.
   apply gpd_moveL_V1.
   refine (cat_assoc _ _ _ $@ (f $@L gpd_h_Vh g f^$) $@ gpd_isretr f).
 Defined.
+
+Class Is3Graph (A : Type) `{Is2Graph A}
+  := isgraph_hom_hom : forall (a b : A), Is2Graph (a $-> b).
+Global Existing Instance isgraph_hom_hom | 30.
+Typeclasses Transparent Is3Graph.
+

theories/WildCat/EmptyCat.v

@@ -18,6 +18,12 @@ Proof.
   constructor; intros [].
 Defined.
 
+Global Instance is2graph_empty : Is2Graph Empty.
+Proof.
+  intros f g.
+  by apply Build_IsGraph.
+Defined.
+
 Global Instance is1cat_empty : Is1Cat Empty.
 Proof.
   snrapply Build_Is1Cat; intros [].

theories/WildCat/Equiv.v

@@ -31,15 +31,15 @@ Class HasEquivs (A : Type) `{Is1Cat A} :=
 (** Since apparently a field of a record can't be the source of a coercion (Coq complains about the uniform inheritance condition, although as officially stated that condition appears to be satisfied), we redefine all the fields of [HasEquivs]. *)
 
 Definition CatEquiv {A} `{HasEquivs A} (a b : A)
-  := @CatEquiv' A _ _ _ _ a b.
+  := @CatEquiv' A _ _ _ _ _ a b.
 
 Notation "a $<~> b" := (CatEquiv a b).
 Infix "≅" := CatEquiv : wc_iso_scope.
 Arguments CatEquiv : simpl never.
 
 Definition cate_fun {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
   : a $-> b
-  := @cate_fun' A _ _ _ _ a b f.
+  := @cate_fun' A _ _ _ _ _ a b f.
 
 Coercion cate_fun : CatEquiv >-> Hom.
 
@@ -71,7 +71,7 @@ Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
            (f : a $-> b) (g : b $-> a)
            (r : f $o g $== Id b) (s : g $o f $== Id a)
   : a $<~> b
-  := @Build_CatEquiv _ _ _ _ _ a b f (catie_adjointify f g r s).
+  := @Build_CatEquiv _ _ _ _ _ _ a b f (catie_adjointify f g r s).
 
 (** This one we define to construct the whole inverse equivalence. *)
 Definition cate_inv {A} `{HasEquivs A} {a b : A} (f : a $<~> b) : b $<~> a.
@@ -111,11 +111,11 @@ Definition id_cate {A} `{HasEquivs A} (a : A)
   := Build_CatEquiv (Id a).
 
 Global Instance reflexive_cate {A} `{HasEquivs A}
-  : Reflexive (@CatEquiv A _ _ _ _)
+  : Reflexive (@CatEquiv A _ _ _ _ _)
   := id_cate.
 
 Global Instance symmetric_cate {A} `{HasEquivs A}
-  : Symmetric (@CatEquiv A _ _ _ _)
+  : Symmetric (@CatEquiv A _ _ _ _ _)
   := fun a b f => cate_inv f.
 
 (** Equivalences can be composed. *)
@@ -185,7 +185,7 @@ Proof.
 Defined.
 
 Global Instance transitive_cate {A} `{HasEquivs A}
-  : Transitive (@CatEquiv A _ _ _ _)
+  : Transitive (@CatEquiv A _ _ _ _ _)
   := fun a b c f g => g $oE f.
 
 (** Some more convenient equalities for equivalences. The naming scheme is similar to [PathGroupoids.v].*)
@@ -231,7 +231,7 @@ Proof.
 Defined.
 
 Class IsUnivalent1Cat (A : Type) `{HasEquivs A}
-  := { isequiv_cat_equiv_path : forall a b, IsEquiv (@cat_equiv_path A _ _ _ _ a b) }.
+  := { isequiv_cat_equiv_path : forall a b, IsEquiv (@cat_equiv_path A _ _ _ _ _ a b) }.
 Global Existing Instance isequiv_cat_equiv_path.
 
 Definition cat_path_equiv {A : Type} `{IsUnivalent1Cat A} (a b : A)
@@ -258,9 +258,10 @@ Proof.
   - intros a b c ; apply compose_cate.
 Defined.
 
-Global Instance isgraph_core_hom {A : Type} `{HasEquivs A} (a b : core A)
-  : IsGraph (a $-> b).
+Global Instance is2graph_core {A : Type} `{HasEquivs A}
+  : Is2Graph (core A).
 Proof.
+  intros a b.
   apply Build_IsGraph.
   intros f g ; exact (cate_fun f $== cate_fun g).
 Defined.
@@ -298,9 +299,11 @@ Global Instance is0functor_core_precomp {A : Type} `{HasEquivs A}
 Proof.
   apply Build_Is0Functor.
   intros f g al; cbn in h.
-  exact (compose_cate_fun f h
-           $@ (al $@R h)
+  (** Why can't coq resolve this? *)
+  refine (compose_cate_fun f h
+           $@ (_ $@R h)
            $@ (compose_cate_fun g h)^$).
+  exact al.
 Defined.
 
 Global Instance is1cat_core {A : Type} `{HasEquivs A}