Basics of (oo,n)-categories

_CoqProject

@@ -64,6 +64,29 @@ theories/WildCat/Yoneda.v
 theories/WildCat/TwoOneCat.v
 theories/WildCat/NatTrans.v
 
+#
+#   ooCat
+#
+theories/ooCat/Glob.v
+theories/ooCat/Cat0.v
+theories/ooCat/Cat1.v
+#
+theories/ooCat/Core.v
+theories/ooCat/Laxity.v
+theories/ooCat/Transformation.v
+theories/ooCat/EquivCat.v
+theories/ooCat/Fibrations.v
+#
+theories/ooCat/Unit.v
+theories/ooCat/Prod.v
+theories/ooCat/Paths.v
+theories/ooCat/Sigma.v
+theories/ooCat/Forall.v
+theories/ooCat/Type.v
+theories/ooCat/pType.v
+
+
+
 #
 #   Types
 #

theories/Basics/Notations.v

@@ -63,7 +63,12 @@ Reserved Infix "=n" (at level 70, no associativity).
 Reserved Infix "$->" (at level 99).
 Reserved Infix "$<~>" (at level 85).
 Reserved Infix "$o" (at level 40).
+Reserved Infix "$oD" (at level 40).
 Reserved Infix "$oE" (at level 40).
+Reserved Infix "$<o" (at level 30).
+Reserved Infix "$o>" (at level 30).
+Reserved Infix "$<oD" (at level 30).
+Reserved Infix "$o>D" (at level 30).
 Reserved Infix "$==" (at level 70).
 Reserved Infix "$o@" (at level 30).
 Reserved Infix "$@" (at level 30).
@@ -72,7 +77,10 @@ Reserved Infix "$@R" (at level 30).
 Reserved Infix "$=>" (at level 99).
 Reserved Notation "T ^op" (at level 3, format "T ^op").
 Reserved Notation "f ^-1$" (at level 3, format "f '^-1$'").
+Reserved Notation "f ^-1'$" (at level 3, format "f '^-1'$'").
+Reserved Notation "f ^-1D$" (at level 3, format "f '^-1D$'").
 Reserved Notation "f ^$" (at level 3, format "f '^$'").
+Reserved Notation "f ^D$" (at level 3, format "f '^D$'").
 
 (** Cubical *)
 Reserved Infix "@@h" (at level 30).

theories/Basics/Overture.v

@@ -169,7 +169,7 @@ 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).
 
-(** Composition of functions. *)
+(** *** Composition of functions. *)
 
 Notation compose := (fun g f x => g (f x)).
 
@@ -694,6 +694,8 @@ Class Irreflexive {A} (R : Relation A) :=
 Class Asymmetric {A} (R : Relation A) :=
   asymmetry : forall {x y}, R x y -> (complement R y x : Type).
 
+(** *** Unit type *)
+
 (** Likewise, we put [Unit] here, instead of in [Unit.v], because [Trunc] uses it. *)
 Inductive Unit : Type0 :=
     tt : Unit.
@@ -705,6 +707,90 @@ Definition Unit_rect := Unit_ind.
 (** A [Unit] goal should be resolved by [auto] and [trivial]. *)
 Hint Resolve tt : core.
 
+(** ** Natural numbers *)
+
+(** The natural numbers are defined in [Coq.Init.Datatypes] (we weren't able to excise them from the stdlib), and studied further in [Spaces.Nat].  But her we give some basic definitions. *)
+
+Definition pred (n : nat) : nat
+  := match n with
+     | 0 => 0
+     | S n => n
+     end.
+
+Notation "n .-1" := (pred n) : nat_scope.
+
+(** *** Booleans *)
+
+(* coq calls it "bool", we call it "Bool" *)
+Local Unset Elimination Schemes.
+Inductive Bool : Type0 :=
+  | true : Bool
+  | false : Bool.
+Scheme Bool_ind := Induction for Bool Sort Type.
+Scheme Bool_rec := Minimality for Bool Sort Type.
+(* For compatibility with Coq's [induction] *)
+Definition Bool_rect := Bool_ind.
+
+Add Printing If Bool.
+
+Declare Scope bool_scope.
+
+Delimit Scope bool_scope with Bool.
+
+Bind Scope bool_scope with Bool.
+
+(** ** Coinductive streams *)
+
+CoInductive Stream (A : Type) := scons
+{
+  head : A ;
+  tail : Stream A
+}.
+
+Arguments scons {A} _ _.
+Arguments head {A} _.
+Arguments tail {A} _.
+
+CoFixpoint const_stream {A} (a : A) : Stream A
+  := scons a (const_stream a).
+
+
+(** *** Typeclasses for case analysis *)
+
+(** Versions of [n = 0] and [n > 0] that are typeclasses and can be found automatically. *)
+Definition IsZeroNat (n : nat) : Type :=
+  match n with
+  | O => Unit
+  | S _ => Empty
+  end.
+Existing Class IsZeroNat.
+Global Instance iszeronat : IsZeroNat 0 := tt.
+
+Definition IsPosNat (n : nat) : Type :=
+  match n with
+  | O => Empty
+  | S _ => Unit
+  end.
+Existing Class IsPosNat.
+Global Instance isposnat (n : nat) : IsPosNat (S n) := tt.
+
+Definition IsTrue (b : Bool) : Type :=
+  match b with
+  | true => Unit
+  | false => Empty
+  end.
+Existing Class IsTrue.
+Global Instance istrue : IsTrue true := tt.
+
+Definition IsFalse (b : Bool) : Type :=
+  match b with
+  | true => Empty
+  | false => Unit
+  end.
+Existing Class IsFalse.
+Global Instance isfalse : IsFalse false := tt.
+
+
 (** *** Pointed types *)
 
 (** A space is pointed if that space has a point. *)

theories/Basics/PathGroupoids.v

@@ -990,10 +990,18 @@ Proof.
 Defined.
 
 (** 2-dimensional path inversion *)
+
 Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q)
   : p^ = q^
 := ap inverse h.
 
+Definition inv_concat2 {A} {x y z : A} {p q : x = y} {r s : y = z}
+           {h : p = q} {k : r = s}
+  : (h @@ k)^ = h^ @@ k^.
+Proof.
+  path_induction; reflexivity.
+Defined.
+
 (** Some higher coherences *)
 
 Lemma ap_pp_concat_pV {A B} (f : A -> B) {x y : A} (p : x = y)
@@ -1188,6 +1196,38 @@ Definition concat_whisker {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p =
     end
   end.
 
+(** [concat2] can equivalently be defined in terms of whiskering. *)
+Definition concat2_is_whiskerL_whiskerR
+           {A} {x y z : A} {p q : x = y} {r s : y = z}
+           {h : p = q} {k : r = s}
+  : (h @@ k) = (h @@ idpath) @ (idpath @@ k).
+Proof.
+  by destruct h, k.
+Defined.
+
+(** In two ways. *)
+Definition concat2_is_whiskerR_whiskerL
+           {A} {x y z : A} {p q : x = y} {r s : y = z}
+           {h : p = q} {k : r = s}
+  : (h @@ k) = (idpath @@ k) @ (h @@ idpath).
+Proof.
+  by destruct h, k.
+Defined.
+
+(** And whiskering can equivalently be defined in terms of [ap]. *)
+Definition ap_concat_r {A} {x y z : A} {p q : x = y} (s : p = q) (r : y = z)
+  : ap (fun t => t @ r) s = whiskerR s r.
+Proof.
+  by destruct s.
+Defined.
+
+Definition ap_concat_l {A} {x y z : A} (p : x = y) {q r : y = z} (s : q = r)
+  : ap (fun t => p @ t) s = whiskerL p s.
+Proof.
+  by destruct s.
+Defined.
+
+
 (** Structure corresponding to the coherence equations of a bicategory. *)
 
 (** The "pentagonator": the 3-cell witnessing the associativity pentagon. *)

theories/Basics/Trunc.v

@@ -133,6 +133,15 @@ Defined.
 Notation "n '.-1'" := (trunc_index_pred n) : trunc_scope.
 Notation "n '.-2'" := (n.-1.-1) : trunc_scope.
 
+(** A version of [n = -2] that's a typeclass. *)
+Definition IsMinusTwo (n : trunc_index) : Type :=
+  match n with
+  | minus_two => Unit
+  | trunc_S _ => Empty
+  end.
+Existing Class IsMinusTwo.
+Global Instance isminustwo : IsMinusTwo (-2) := tt.
+
 Definition trunc_index_leq_minus_two {n}
   : n <= -2 -> n = -2.
 Proof.

theories/Types/Bool.v

@@ -6,24 +6,6 @@ Require Import Types.Prod Types.Equiv.
 
 Local Open Scope path_scope.
 
-(* coq calls it "bool", we call it "Bool" *)
-Local Unset Elimination Schemes.
-Inductive Bool : Type0 :=
-  | true : Bool
-  | false : Bool.
-Scheme Bool_ind := Induction for Bool Sort Type.
-Scheme Bool_rec := Minimality for Bool Sort Type.
-(* For compatibility with Coq's [induction] *)
-Definition Bool_rect := Bool_ind.
-
-Add Printing If Bool.
-
-Declare Scope bool_scope.
-
-Delimit Scope bool_scope with Bool.
-
-Bind Scope bool_scope with Bool.
-
 Definition andb (b1 b2 : Bool) : Bool := if b1 then b2 else false.
 
 Definition orb (b1 b2 : Bool) : Bool := if b1 then true else b2.