Basics of wild 1-categories; jww alizter, emilyriehl, mpopie, tslilc

_CoqProject

@@ -42,6 +42,22 @@ theories/Basics/Equivalences.v
 theories/Basics/Trunc.v
 theories/Basics/Decidable.v
 
+#
+#   Wildcat
+#
+theories/WildCat.v
+theories/WildCat/Core.v
+theories/WildCat/UnitCat.v
+theories/WildCat/EmptyCat.v
+theories/WildCat/Prod.v
+theories/WildCat/Equiv.v
+theories/WildCat/Sum.v
+theories/WildCat/Opposite.v
+theories/WildCat/Type.v
+theories/WildCat/Induced.v
+theories/WildCat/FunctorCat.v
+theories/WildCat/Yoneda.v
+
 #
 #   Types
 #
@@ -268,6 +284,7 @@ theories/Pointed/pEquiv.v
 theories/Pointed/pTrunc.v
 theories/Pointed/pHomotopy.v
 theories/Pointed/pSusp.v
+theories/Pointed/pType.v
 
 #
 #   Spectra

theories/Basics/Notations.v

@@ -13,6 +13,16 @@ Reserved Infix "=n" (at level 70, no associativity).
 Reserved Infix "o*" (at level 40).
 Reserved Infix "oL" (at level 40, left associativity).
 Reserved Infix "oR" (at level 40, left associativity).
+Reserved Infix "$->" (at level 99).
+Reserved Infix "$<~>" (at level 85).
+Reserved Infix "$o" (at level 40).
+Reserved Infix "$oE" (at level 40).
+Reserved Infix "$==" (at level 70).
+Reserved Infix "$o@" (at level 30).
+Reserved Infix "$@" (at level 30).
+Reserved Infix "$@L" (at level 30).
+Reserved Infix "$@R" (at level 30).
+Reserved Infix "$=>" (at level 99).
 Reserved Notation "~~ A" (at level 75, right associativity, only parsing).
 Reserved Notation "A <~> B" (at level 85).
 Reserved Notation "a // 'CAT'" (at level 40, left associativity).
@@ -28,8 +38,10 @@ Reserved Notation "F '_0' x" (at level 10, no associativity).
 Reserved Notation "F '_0' x" (at level 10, no associativity, only parsing).
 Reserved Notation "f ^-1" (at level 3, format "f '^-1'").
 Reserved Notation "f ^-1*" (at level 3, format "f '^-1*'").
+Reserved Notation "f ^-1$" (at level 3, format "f '^-1$'").
 Reserved Notation "F '_1' m" (at level 10, no associativity).
 Reserved Notation "f ^*" (at level 20).
+Reserved Notation "f ^$" (at level 20).
 Reserved Notation "f *E g" (at level 40, no associativity).
 Reserved Notation "f +E g" (at level 50, left associativity).
 Reserved Notation "f == g" (at level 70, no associativity).

theories/Basics/Overture.v

@@ -164,7 +164,7 @@ Notation pr2 := projT2.
 Notation "x .1" := (pr1 x) : fibration_scope.
 Notation "x .2" := (pr2 x) : fibration_scope.
 
-Definition uncurry {A B C} (f: A -> B -> C) (p: A * B): C := f (fst p) (snd p).
+Definition uncurry {A B C} (f : A -> B -> C) (p : A * B) : C := f (fst p) (snd p).
 
 (** Composition of functions. *)
 

theories/Categories.v

@@ -65,7 +65,7 @@ Require CategoryOfSections.
 (** ** The Dependent Product *)
 Require DependentProduct.
 (** ** The Yoneda Lemma *)
-Require Yoneda.
+Require Categories.Yoneda.
 (** ** The Structure Identity Principle *)
 Require Structure.
 (** ** Fundamental Pregroupoids *)
@@ -105,7 +105,7 @@ Include LaxComma.Core.
 Include DualFunctor.
 Include CategoryOfSections.Core.
 Include DependentProduct.
-Include Yoneda.
+Include Categories.Yoneda.
 Include Structure.Core.
 Include FundamentalPreGroupoidCategory.
 Include HomotopyPreCategory.

theories/HoTT.v

@@ -5,6 +5,7 @@
 
 Require Export HoTT.Basics.
 Require Export HoTT.Types.
+Require Export HoTT.WildCat.
 Require Export HoTT.Cubical.
 Require Export HoTT.Pointed.
 Require Export HoTT.Truncations.

theories/Pointed/Loops.v

@@ -346,7 +346,7 @@ Local Notation "( X , x )" := (Build_pType X x).
 Definition loops_type `{Univalence} (A : Type)
   : loops (Type,A) <~>* (A <~> A, equiv_idmap).
 Proof.
-  apply issig_pequiv.
+  apply issig_pequiv'.
   exists (equiv_equiv_path A A).
   reflexivity.
 Defined.
@@ -357,7 +357,7 @@ Lemma local_global_looping `{Univalence} (A : Type) (n : nat)
 Proof.
   induction n.
   { refine (_ o*E pequiv_loops_functor (loops_type A)).
-    apply issig_pequiv.
+    apply issig_pequiv'.
     exists (equiv_inverse (equiv_path_arrow 1%equiv 1%equiv)
             oE equiv_inverse (equiv_path_equiv 1%equiv 1%equiv)).
     reflexivity. }

theories/Pointed/pEquiv.v

@@ -1,6 +1,7 @@
 Require Import Basics.
 Require Import Types.
-Require Import Pointed.Core.
+Require Import Pointed.Core Pointed.pMap Pointed.pHomotopy.
+Require Import UnivalenceImpliesFunext.
 
 Local Open Scope pointed_scope.
 
@@ -44,8 +45,28 @@ Defined.
 
 Notation "g o*E f" := (pequiv_compose f g) : pointed_scope.
 
-(* The record for pointed equivalences is equivalently a sigma type *)
 Definition issig_pequiv (A B : pType)
+  : { f : A ->* B & IsEquiv f } <~> (A <~>* B).
+Proof.
+  issig.
+Defined.
+
+(* Two pointed equivalences are equal if their underlying pointed functions are pointed homotopic. *)
+Definition equiv_path_pequiv `{Funext} {A B : pType} (f g : A <~>* B)
+  : (f ==* g) <~> (f = g).
+Proof.
+  transitivity ((issig_pequiv A B)^-1 f = (issig_pequiv A B)^-1 g).
+  - refine (equiv_path_sigma_hprop _ _ oE _).
+    apply (equiv_path_pmap f g).
+  - symmetry; exact (equiv_ap' (issig_pequiv A B)^-1 f g).
+Defined.
+
+Definition path_pequiv `{Funext} {A B : pType} (f g : A <~>* B)
+  : (f ==* g) -> (f = g)
+  := fun p => equiv_path_pequiv f g p.
+
+(* The record for pointed equivalences is equivalently a different sigma type *)
+Definition issig_pequiv' (A B : pType)
   : { f : A <~> B & f (point A) = point B } <~> (A <~>* B).
 Proof.
   transitivity { f : A ->* B & IsEquiv f }.
@@ -71,7 +92,7 @@ Proof.
   destruct A as [A a], B as [B b].
   refine (equiv_ap issig_ptype (A;a) (B;b) oE _).
   refine (equiv_path_sigma _ _ _ oE _).
-  refine (_ oE (issig_pequiv _ _)^-1); simpl.
+  refine (_ oE (issig_pequiv' _ _)^-1); simpl.
   refine (equiv_functor_sigma' (equiv_path_universe A B) _); intros f.
   apply equiv_concat_l.
   apply transport_path_universe.
@@ -137,4 +158,4 @@ Proof.
   serapply (isequiv_adjointify f f').
   1: apply r.
   apply s.
-Defined.
+Defined.

theories/Pointed/pFiber.v

@@ -23,7 +23,7 @@ Definition pfib {A B : pType} (f : A ->* B) : pfiber f ->* A
 Definition pfiber2_loops {A B : pType} (f : A ->* B)
 : pfiber (pfib f) <~>* loops B.
 Proof.
-  apply issig_pequiv; simple refine (_;_).
+  apply issig_pequiv'; simple refine (_;_).
   - simpl; unfold hfiber.
     refine (_ oE (equiv_sigma_assoc _ _)^-1); simpl.
     refine (_ oE (equiv_functor_sigma'

theories/Pointed/pType.v

@@ -0,0 +1,75 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+Require Import Basics Types.
+Require Import Pointed.Core.
+Require Import WildCat.
+Require Import pHomotopy pMap pEquiv.
+
+Local Open Scope pointed_scope.
+Local Open Scope path_scope.
+
+(** * pType as a wild category *)
+
+Global Instance is01cat_ptype : Is01Cat pType
+  := Build_Is01Cat pType pMap (@pmap_idmap) (@pmap_compose).
+
+Global Instance is01cat_pmap (A B : pType) : Is01Cat (A ->* B).
+Proof.
+  srapply (Build_Is01Cat (A ->* B) (@pHomotopy A B)).
+  - reflexivity.
+  - intros a b c f g; transitivity b; assumption.
+Defined.
+
+Global Instance is0gpd_pmap (A B : pType) : Is0Gpd (A ->* B).
+Proof.
+  srapply Build_Is0Gpd.
+  intros; symmetry; assumption.
+Defined.
+
+Global Instance is1cat_ptype : Is1Cat pType.
+Proof.
+  simple refine (Build_Is1Cat _ _ _ _ _ _ _ _); try exact _.
+  - intros A B C; rapply Build_Is0Functor.
+    intros [f1 f2] [g1 g2] [p q]; cbn.
+    transitivity (f1 o* g2).
+    + apply pmap_postwhisker; assumption.
+    + apply pmap_prewhisker; assumption.
+  - intros ? ? ? ? f g h; exact (pmap_compose_assoc h g f).
+  - intros ? ? f; exact (pmap_postcompose_idmap f).
+  - intros ? ? f; exact (pmap_precompose_idmap f).
+Defined.
+
+Global Instance hasmorext_ptype `{Funext} : HasMorExt pType.
+Proof.
+  srapply Build_HasMorExt; intros A B f g.
+  refine (isequiv_homotopic (equiv_path_pmap f g)^-1 _).
+  intros []; reflexivity.
+Defined.
+
+
+Global Instance hasequivs_ptype : HasEquivs pType.
+Proof.
+  srapply (Build_HasEquivs _ _ _ pEquiv (fun A B f => IsEquiv f));
+    intros A B f; cbn; intros.
+  - exact f.
+  - exact _.
+  - exact (Build_pEquiv _ _ f _).
+  - reflexivity.
+  - exact ((Build_pEquiv _ _ f _)^-1*).
+  - apply peissect.
+  - cbn. refine (peisretr (Build_pEquiv _ _ f _)).
+  - rapply (isequiv_adjointify f g).
+    + intros x; exact (pointed_htpy r x).
+    + intros x; exact (pointed_htpy s x).
+Defined.
+
+Global Instance isunivalent_ptype `{Univalence} : IsUnivalent1Cat pType.
+Proof.
+  srapply Build_IsUnivalent1Cat; intros A B.
+  refine (isequiv_homotopic (equiv_path_ptype A B)^-1 _).
+  intros []; apply path_pequiv.
+  cbn.
+  srefine (Build_pHomotopy _ _).
+  - intros x; reflexivity.
+  - cbn.
+    (* Some messy path algebra here. *)
+Abort.

theories/WildCat.v

@@ -0,0 +1,11 @@
+Require Export WildCat.Core.
+Require Export WildCat.Equiv.
+Require Export WildCat.UnitCat.
+Require Export WildCat.EmptyCat.
+Require Export WildCat.Opposite.
+Require Export WildCat.Type.
+Require Export WildCat.Induced.
+Require Export WildCat.FunctorCat.
+Require Export WildCat.Yoneda.
+Require Export WildCat.Prod.
+Require Export WildCat.Sum.