Initial commit

theories/WildCat/Core.v

@@ -9,6 +9,20 @@ Class IsGraph (A : Type) :=
   Hom : A -> A -> Type
 }.
 
+Module Graph.
+  Record type := Build_Graph {
+  Ob : Type;
+  is_graph : IsGraph (Ob : Type)
+}.
+End Graph.
+(* Have to define these outside the module because 
+   you have to import the module to use it 
+   and it seems preferable to keep a more fine-grained 
+   namespace. *)
+Coercion Graph.Ob : Graph.type >-> Sortclass.
+Existing Instance Graph.is_graph.
+Notation Graph := Graph.type.
+
 Notation "a $-> b" := (Hom a b).
 
 Definition graph_hfiber {B C : Type} `{IsGraph C} (F : B -> C) (c : C)
@@ -108,34 +122,35 @@ Class Is1Cat (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A} :=
 
 Global Existing Instance is01cat_hom.
 Global Existing Instance is0gpd_hom.
-Global Existing Instance is0functor_postcomp.
+Global Existing Instance is0functor_postcomp. 
 Global Existing Instance is0functor_precomp.
 Arguments cat_assoc {_ _ _ _ _ _ _ _ _} f g h.
 Arguments cat_assoc_opp {_ _ _ _ _ _ _ _ _} f g h.
 Arguments cat_idl {_ _ _ _ _ _ _} f.
 Arguments cat_idr {_ _ _ _ _ _ _} f.
 
-
 Module Category.
-  Record class_of (A : Type) := Class {
+  Class class_of (A : Type) := Class {
     is_graph : IsGraph A;
-    is_01_cat : Is01Cat A;
+    is01cat : Is01Cat A;
     is2graph : Is2Graph A;
     is1cat : Is1Cat A (* This can be seen as the "mixin" in the sense of packed classes. *)
   }.
 
-  Record Category := {
-    Ob :> Type;
+  Record type := {
+    Ob : Type;
     is_class_of : class_of Ob
   }.
-
-  Module Exports.
-    Notation Category := Category.
-  End Exports.
 End Category.
-Export Category.Exports.
-
-(** An alternate constructor that doesn't require the proof of [cat_assoc_opp].  This can be used for defining examples of wild categories, but shouldn't be used for the general theory of wild categories. *)
+Coercion Category.Ob : Category.type >-> Sortclass.
+Existing Instance Category.is_class_of.
+Existing Instance Category.is_graph.
+Existing Instance Category.is2graph.
+Existing Instance Category.is01cat.
+Existing Instance Category.is1cat.
+Notation Category := Category.type.
+
+(** An alternate constructor that doesn't require the proof of [cat_assoc_opp]. This can be used for defining examples of wild categories, but shouldn't be used for the general theory of wild categories. *)
 Definition Build_Is1Cat' (A : Type) `{!IsGraph A, !Is2Graph A, !Is01Cat A}
   (is01cat_hom : forall a b : A, Is01Cat (a $-> b))
   (is0gpd_hom : forall a b : A, Is0Gpd (a $-> b))

theories/WildCat/FunctorCat.v

@@ -7,204 +7,3 @@ Require Import WildCat.NatTrans.
 
 (** * Wild functor categories *)
 
-(** ** Categories of 0-coherent 1-functors *)
-
-Record Fun01 (A B : Type) `{IsGraph A} `{IsGraph B} := {
-  fun01_F : A -> B;
-  fun01_is0functor : Is0Functor fun01_F;
-}.
-
-Coercion fun01_F : Fun01 >-> Funclass.
-Global Existing Instance fun01_is0functor.
-
-Arguments Build_Fun01 A B {isgraph_A isgraph_B} F {fun01_is0functor} : rename.
-
-Definition issig_Fun01 (A B : Type) `{IsGraph A} `{IsGraph B}
-  : _  <~> Fun01 A B := ltac:(issig).
-
-(* Note that even if [A] and [B] are fully coherent oo-categories, the objects of our "functor category" are not fully coherent.  Thus we cannot in general expect this "functor category" to itself be fully coherent.  However, it is at least a 0-coherent 1-category, as long as [B] is a 1-coherent 1-category. *)
-
-Global Instance isgraph_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : IsGraph (Fun01 A B).
-Proof.
-  srapply Build_IsGraph.
-  intros [F ?] [G ?].
-  exact (NatTrans F G).
-Defined.
-
-Global Instance is01cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is01Cat (Fun01 A B).
-Proof.
-  srapply Build_Is01Cat.
-  - intros [F ?]; cbn.
-    exact (nattrans_id F).
-  - intros F G K gamma alpha; cbn in *.
-    exact (nattrans_comp gamma alpha).
-Defined.
-
-Global Instance is2graph_fun01 (A B : Type) `{IsGraph A, Is1Cat B}
-  : Is2Graph (Fun01 A B).
-Proof.
-  intros [F ?] [G ?]; apply Build_IsGraph.
-  intros [alpha ?] [gamma ?].
-  exact (forall a, alpha a $== gamma a).
-Defined.
-
-(** In fact, in this case it is automatically also a 0-coherent 2-category and a 1-coherent 1-category, with a totally incoherent notion of 2-cell between 1-coherent natural transformations. *)
-
-Global Instance is1cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is1Cat (Fun01 A B).
-Proof.
-  srapply Build_Is1Cat.
-  - intros [F ?] [G ?]; srapply Build_Is01Cat.
-    + intros [alpha ?] a; cbn.
-      reflexivity.
-    + intros [alpha ?] [gamma ?] [phi ?] nu mu a.
-      exact (mu a $@ nu a).
-  - intros [F ?] [G ?]; srapply Build_Is0Gpd.
-    intros [alpha ?] [gamma ?] mu a.
-    exact ((mu a)^$).
-  - intros [F ?] [G ?] [K ?] [alpha ?].
-    srapply Build_Is0Functor.
-    intros [phi ?] [mu ?] f a.
-    exact (alpha a $@L f a).
-  - intros [F ?] [G ?] [K ?] [alpha ?].
-    srapply Build_Is0Functor.
-    intros [phi ?] [mu ?] f a.
-    exact (f a $@R alpha a).
-  - intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
-    srapply cat_assoc.
-  - intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
-    srapply cat_assoc_opp.
-  - intros [F ?] [G ?] [alpha ?] a; cbn.
-    srapply cat_idl.
-  - intros [F ?] [G ?] [alpha ?] a; cbn.
-    srapply cat_idr.
-Defined.
-
-(** It also inherits a notion of equivalence, namely a natural transformation that is a pointwise equivalence.  Note that this is not a "fully coherent" notion of equivalence, since the functors and transformations are not themselves fully coherent. *)
-
-Global Instance hasequivs_fun01 (A B : Type) `{Is01Cat A} `{HasEquivs B}
-  : HasEquivs (Fun01 A B).
-Proof.
-  srapply Build_HasEquivs.
-  1: intros F G; exact (NatEquiv F G).
-  all: intros F G alpha; cbn in *.
-  - exact (forall a, CatIsEquiv (alpha a)).
-  - exact alpha.
-  - intros a; exact _.
-  - apply Build_NatEquiv'.
-  - cbn; intros; apply cate_buildequiv_fun.
-  - exact (natequiv_inverse alpha).
-  - intros; apply cate_issect.
-  - intros; apply cate_isretr.
-  - intros [gamma ?] r s a; cbn in *.
-    refine (catie_adjointify (alpha a) (gamma a) (r a) (s a)).
-Defined.
-
-(** Bundled opposite functors *)
-Definition fun01_op (A B : Type) `{IsGraph A} `{IsGraph B}
-  : Fun01 A B -> Fun01 A^op B^op.
-Proof.
-  intros F.
-  rapply (Build_Fun01 A^op B^op F).
-Defined.
-
-(** ** Categories of 1-coherent 1-functors *)
-
-Record Fun11 (A B : Type) `{Is1Cat A} `{Is1Cat B} :=
-{
-  fun11_fun : A -> B ;
-  is0functor_fun11 : Is0Functor fun11_fun ;
-  is1functor_fun11 : Is1Functor fun11_fun
-}.
-
-Coercion fun11_fun : Fun11 >-> Funclass.
-Global Existing Instance is0functor_fun11.
-Global Existing Instance is1functor_fun11.
-
-Arguments Build_Fun11 A B
-  {isgraph_A is2graph_A is01cat_A is1cat_A
-   isgraph_B is2graph_B is01cat_B is1cat_B}
-  F {is0functor_fun11 is1functor_fun11} : rename.
-
-Coercion fun01_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
-           (F : Fun11 A B)
-  : Fun01 A B.
-Proof.
-  exists F; exact _.
-Defined.
-
-Global Instance isgraph_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
-  : IsGraph (Fun11 A B)
-  := isgraph_induced fun01_fun11.
-
-Global Instance is01cat_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
-  : Is01Cat (Fun11 A B)
-  := is01cat_induced fun01_fun11.
-
-Global Instance is2graph_fun11 {A B : Type} `{Is1Cat A, Is1Cat B}
-  : Is2Graph (Fun11 A B)
-  := is2graph_induced fun01_fun11.
-
-Global Instance is1cat_fun11 {A B :Type} `{Is1Cat A} `{Is1Cat B}
-  : Is1Cat (Fun11 A B)
-  := is1cat_induced fun01_fun11.
-
-Global Instance hasequivs_fun11 {A B : Type} `{Is1Cat A} `{HasEquivs B}
-  : HasEquivs (Fun11 A B)
-  := hasequivs_induced fun01_fun11.
-
-(** * Identity functors *)
-
-Definition fun01_id {A} `{IsGraph A} : Fun01 A A
-  := Build_Fun01 A A idmap.
-
-Definition fun11_id {A} `{Is1Cat A} : Fun11 A A
-  := Build_Fun11 _ _ idmap.
-
-(** * Composition of functors *)
-
-Definition fun01_compose {A B C} `{IsGraph A, IsGraph B, IsGraph C}
-  : Fun01 B C -> Fun01 A B -> Fun01 A C
-  := fun G F => Build_Fun01 _ _ (G o F).
-
-Definition fun01_postcomp {A B C}
-  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
-  : Fun01 A B -> Fun01 A C
-  := fun01_compose (A:=A) F.
-
-(** Warning: [F] needs to be a 1-functor for this to be a 0-functor. *)
-Global Instance is0functor_fun01_postcomp {A B C}
-  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
-  : Is0Functor (fun01_postcomp (A:=A) F).
-Proof.
-  apply Build_Is0Functor.
-  intros a b f.
-  rapply nattrans_postwhisker.
-  exact f.
-Defined.
-
-Global Instance is1functor_fun01_postcomp {A B C}
-  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
-  : Is1Functor (fun01_postcomp (A:=A) F).
-Proof.
-  apply Build_Is1Functor.
-  - intros a b f g p x.
-    rapply fmap2.
-    rapply p.
-  - intros f x.
-    rapply fmap_id.
-  - intros a b c f g x.
-    rapply fmap_comp.
-Defined.
-
-Definition fun11_fun01_postcomp {A B C}
-  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
-  : Fun11 (Fun01 A B) (Fun01 A C)
-  := Build_Fun11 _ _ (fun01_postcomp F).
-
-Definition fun11_compose {A B C} `{Is1Cat A, Is1Cat B, Is1Cat C}
-  : Fun11 B C -> Fun11 A B -> Fun11 A C.
-Proof.
-  intros F G.
-  nrapply Build_Fun11.
-  rapply (is1functor_compose G F).
-Defined.