From f994f96350cfe5ea01ed479af55811d3e1c8a83e Mon Sep 17 00:00:00 2001 From: Mike Shulman Date: Fri, 13 Mar 2020 10:32:07 -0700 Subject: [PATCH 1/4] Basics of (oo,n)-categories --- _CoqProject | 22 ++ theories/Basics/Notations.v | 8 + theories/Basics/Overture.v | 88 ++++- theories/Basics/Trunc.v | 9 + theories/Types/Bool.v | 18 - theories/ooCat/Cat0.v | 664 ++++++++++++++++++++++++++++++++ theories/ooCat/Cat1.v | 521 +++++++++++++++++++++++++ theories/ooCat/Core.v | 46 +++ theories/ooCat/EquivCat.v | 24 ++ theories/ooCat/Fibrations.v | 27 ++ theories/ooCat/Forall.v | 106 +++++ theories/ooCat/Glob.v | 370 ++++++++++++++++++ theories/ooCat/Laxity.v | 37 ++ theories/ooCat/Paths.v | 60 +++ theories/ooCat/Prod.v | 63 +++ theories/ooCat/Sigma.v | 31 ++ theories/ooCat/Transformation.v | 216 +++++++++++ theories/ooCat/Type.v | 33 ++ theories/ooCat/Unit.v | 26 ++ 19 files changed, 2350 insertions(+), 19 deletions(-) create mode 100644 theories/ooCat/Cat0.v create mode 100644 theories/ooCat/Cat1.v create mode 100644 theories/ooCat/Core.v create mode 100644 theories/ooCat/EquivCat.v create mode 100644 theories/ooCat/Fibrations.v create mode 100644 theories/ooCat/Forall.v create mode 100644 theories/ooCat/Glob.v create mode 100644 theories/ooCat/Laxity.v create mode 100644 theories/ooCat/Paths.v create mode 100644 theories/ooCat/Prod.v create mode 100644 theories/ooCat/Sigma.v create mode 100644 theories/ooCat/Transformation.v create mode 100644 theories/ooCat/Type.v create mode 100644 theories/ooCat/Unit.v diff --git a/_CoqProject b/_CoqProject index 11195a5c161..7f1e243512b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -64,6 +64,28 @@ 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 + + + # # Types # diff --git a/theories/Basics/Notations.v b/theories/Basics/Notations.v index f8d88687248..65e7a86717d 100644 --- a/theories/Basics/Notations.v +++ b/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 "$" (at level 30). +Reserved Infix "$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). diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index c0db434eb17..9499cc82202 100644 --- a/theories/Basics/Overture.v +++ b/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. *) + +Fixpoint 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. *) diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v index 9b27d68225b..5c85c256547 100644 --- a/theories/Basics/Trunc.v +++ b/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. diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v index d73ba79df43..1396bd351af 100644 --- a/theories/Types/Bool.v +++ b/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. diff --git a/theories/ooCat/Cat0.v b/theories/ooCat/Cat0.v new file mode 100644 index 00000000000..99726a0d089 --- /dev/null +++ b/theories/ooCat/Cat0.v @@ -0,0 +1,664 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Export ooCat.Glob. + +(** * 0-coherent oo-categories *) + +Generalizable Variables m n p A B C. + +(** ** Basic definition *) + +(** The implicit oo-category convention is in effect: [IsCat0 n] means "is an (oo,n)-category". The postfix "0" means "0-coherent". There are different choices about what this could mean: + +- It could mean "having only the structure of a (0,n)-category at each dimension": composition, identities, and in the case [n=0] inversion, but no axioms. +- It could mean the maximal difference in dimension between the inputs and outputs of operations is 0, so it has all operations but no axioms. + +We currently choose the latter, which happens to also be "everything that can be stated without referring to equivalences". *) +CoInductive IsCat0 (n : nat) (A : Type) `{IsGlob n A} : Type := +{ + cat_id : forall (a : A), a $-> a ; + cat_comp : forall {a b c : A}, + (b $-> c) -> (a $-> b) -> (a $-> c) where "g $o f" := (cat_comp g f); + isfunctor0_postcomp : forall (a b c : A) (g : b $-> c), + IsFunctor0 (fun f : a $-> b => g $o f) ; + isfunctor0_precomp : forall (a b c : A) (f : a $-> b), + IsFunctor0 (fun g : b $-> c => g $o f) ; + gpd_inv : forall (isz : IsZeroNat n) (a b : A), + (a $-> b) -> (b $-> a) ; + iscat0_hom : forall (a b : A), @IsCat0 (pred n) (a $-> b) _ ; +}. + +Existing Class IsCat0. +Arguments cat_id {n A _ _} a. +Arguments cat_comp {n A _ _ a b c} g f. +Notation "g $o f" := (cat_comp g f). + +(** When we're in a groupoid dimension, we use path-like syntax. *) +Arguments gpd_inv {n A _ _ _ a b} f. +Notation "f ^$" := (gpd_inv f). +Notation "f $@ g" := (@cat_comp 0 _ _ _ _ _ _ g f). + +Global Existing Instances + iscat0_hom isfunctor0_postcomp isfunctor0_precomp. + +Hint Extern 1 (IsCat0 ?n (Hom _ _ _)) => change_dim n : typeclass_instances. +Hint Extern 1 (IsCat0 ?n (Hom _ _ _)) => change_dim_0 n : typeclass_instances. + +Definition cat_postcomp `{IsCat0 n A} + (a : A) {b c : A} (g : b $-> c) + : (a $-> b) -> (a $-> c) + := fun f => g $o f. + +Definition cat_precomp `{IsCat0 n A} + {a b : A} (c : A) (f : a $-> b) + : (b $-> c) -> (a $-> c) + := fun g => g $o f. + +Definition cat_postwhisker `{IsCat0 n A} {a b c : A} + {f g : a $-> b} (h : b $-> c) (p : f $-> g) + : h $o f $-> h $o g + := fmap (cat_postcomp a h) p. +Notation "h $ c} (p : f $-> g) (h : a $-> b) + : f $o h $-> g $o h + := fmap (cat_precomp c h) p. +Notation "p $o> h" := (cat_prewhisker p h). + +(* These seem to be unnecessary; I guess [cat_postcomp] and [cat_precomp] are sufficiently transparent to typeclass search. *) +(* +Global Instance isfunctor0_postcomp' `{IsCat0 n A} + {a b c : A} (g : b $-> c) + : IsFunctor0 (cat_postcomp a g). +Proof. + exact _. +Defined. + +Global Instance isfunctor0_precomp' `{IsCat0 n A} + {a b c : A} (f : a $-> b) + : IsFunctor0 (cat_precomp c f). +Proof. + exact _. +Defined. +*) + +Definition iscat0_induced {A} `{IsCat0 n B} (F : A -> B) + : @IsCat0 n A (isglob_induced F). +Proof. + unshelve econstructor; cbn; intros. + - eapply cat_comp; eassumption. + - apply cat_id. + - exact _. + - exact _. + - apply gpd_inv; assumption. + - exact _. +Defined. + +(** ** Constant functors *) + +CoFixpoint isfunctor0_const `{IsGlob m A} `{IsCat0 n B} (x : B) + : IsFunctor0 (@const A B x). +Proof. + simple notypeclasses refine (Build_IsFunctor0 _ _ _). + { intros a b f. + apply cat_id. } + intros a b. + rapply isfunctor0_const. +Defined. + +Global Existing Instance isfunctor0_const. + + +(** ** Truncatedness and invertibility *) + +(** Truncatedness can be used as a cap on the invertibility dimension *) +CoFixpoint iscat0_cattrunc + {n : nat} `{IsCat0 m A} `{!CatTrunc n.-1 A} + : @IsCat0 n A isglob_reindex. +Proof. + unshelve econstructor. + 1: clear iscat0_cattrunc; intros a b c; cbn; apply cat_comp. + 1: clear iscat0_cattrunc; intros; cbn; apply cat_id. + 1-2: intros; cbn; + apply (@isfunctor0_reindex (pred m) (pred m) (pred n) (pred n)); + exact _. + - destruct n as [|[|n]]; cbn in *. + 1:intros; rapply cat_center. + 1-2:intros []. + - intros; cbn. + rapply (iscat0_cattrunc (pred n) (pred m) (a $-> b)). + destruct n as [|n]; cbn in *. + + apply cattrunc_pred. + + exact _. +Defined. + +(** ** Quasi-isomorphisms *) + +(** A morphism in an (oo,n)-category is an equivalence if either [n=0] or if it has an inverse up to equivalence. Since this is not a coherent structure, we denigrate it with the name "quasi-isomorphism". We define it coinductively, but in practice it suffices to reason about it inductively since all our categories are (oo,n)-categories for some finite n. *) + +CoInductive IsQIso `{IsCat0 n A} {a b : A} (f : a $-> b) := +{ + qiso_inv : b $-> a ; + qiso_issect : (qiso_inv $o f) $-> (cat_id a) ; + qiso_isretr : (f $o qiso_inv) $-> (cat_id b) ; + isqiso_qiso_issect : @IsQIso _ (a $-> a) _ _ _ _ qiso_issect ; + isqiso_qiso_isretr : @IsQIso _ (b $-> b) _ _ _ _ qiso_isretr ; +}. +Existing Class IsQIso. +Arguments qiso_inv {n A _ _ a b} f {_}. +Arguments qiso_issect {n A _ _ a b} f {_}. +Arguments qiso_isretr {n A _ _ a b} f {_}. +Global Existing Instances isqiso_qiso_issect isqiso_qiso_isretr. + +Hint Extern 1 (@IsQIso ?n (Hom _ _ _) _ _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@IsQIso ?n (Hom _ _ _) _ _ _ _ _) => change_dim_0 n : typeclass_instances. + +(** The inverse of a quasi-isomorphism is a quasi-isomorphism. *) +Global Instance isqiso_inv `{IsCat0 n A} + {a b : A} (f : a $-> b) `{!IsQIso f} + : IsQIso (qiso_inv f). +Proof. + unshelve econstructor. + 1: exact f. + 1: exact (qiso_isretr f). + 1: exact (qiso_issect f). + all: exact _. +Defined. + +(** Every morphism in a (-2)- or (-1)-truncated category is a quasi-isomorphism. *) +CoFixpoint isqiso_catcontr `{IsCat0 n A, !CatContr A} + {a b : A} (f : a $-> b) + : IsQIso f. +Proof. + unshelve econstructor. + 1-3:apply cat_center. + 1-2:rapply isqiso_catcontr. +Defined. +Global Existing Instance isqiso_catcontr. + +Global Instance isqiso_catprop `{IsCat0 n A, !CatProp A} + {a b : A} (f : a $-> b) + : IsQIso f. +Proof. + unshelve econstructor. + 1-3:apply cat_center. + 1-2:apply isqiso_catcontr. +Defined. + +(** It follows that in a 0-truncated category, having maps back and forth suffices. *) +Global Instance isqiso_catposet `{IsCat0 n A, !CatPoset A} + {a b : A} (f : a $-> b) (g : b $-> a) + : IsQIso f. +Proof. + unshelve econstructor. + 1:exact g. + 1-2:apply cat_center. + 1-2:apply isqiso_catprop. +Defined. + +(** And in a truncated (1,1)-category, an ordinary "isomorphism" suffices. *) +Global Instance isqiso_cat1cat `{IsCat0 1 A, !Cat1Cat A} + {a b : A} (f : a $-> b) (g : b $-> a) + (s : g $o f $== cat_id a) (r : f $o g $== cat_id b) + : IsQIso f. +Proof. + unshelve econstructor. + - exact g. + - exact s. + - exact r. + - apply isqiso_catposet. + exact (s^$). + - apply isqiso_catposet. + exact (r^$). +Defined. + +(** To prove much of anything else about quasi-isomorphisms (even that the identity is one!) requires more coherence. *) + + +(** ** Equivalences *) + +(** There are various possible coherent definitions of equivalence, some generally applicable and others more specifiec. Rather than mandate a particular one in all cases, we give the user the freedom to choose whichever they prefer for a particular category by instantiating the following typeclass. Note though that we don't actually *require* any coherence of the notion of equivalence, only that it is logically equivalent to quasi-isomorphism. *) + +CoInductive HasEquivs (n : nat) (A : Type) `{IsCat0 n A} := +{ + CatIsEquiv' : forall {a b : A}, (a $-> b) -> Type ; + catie_isqiso' : forall (a b : A) (f : a $-> b), IsQIso f -> CatIsEquiv' f ; + isqiso_catie' : forall (a b : A) (f : a $-> b), CatIsEquiv' f -> IsQIso f ; + hasequivs_hom : forall (a b : A), @HasEquivs (pred n) (a $-> b) _ _ ; +}. +Existing Class HasEquivs. +Global Existing Instance hasequivs_hom. + +Hint Extern 1 (HasEquivs ?n (Hom _ _ _)) => change_dim n : typeclass_instances. +Hint Extern 1 (HasEquivs ?n (Hom _ _ _)) => change_dim_0 n : typeclass_instances. + +(** A field can't be a working [Existing Class] due to a bug in Coq. *) +Class CatIsEquiv `{HasEquivs n A} {a b : A} (f : a $-> b) + := catie_catie : @CatIsEquiv' n A _ _ _ a b f. + +Hint Extern 1 (CatIsEquiv ?n (Hom _ _ _)) => change_dim n : typeclass_instances. +Hint Extern 1 (CatIsEquiv ?n (Hom _ _ _)) => change_dim_0 n : typeclass_instances. + +Arguments CatIsEquiv : simpl never. + +Global Instance isqiso_catie `{HasEquivs n A} + {a b : A} (f : a $-> b) `{!CatIsEquiv f} + : IsQIso f. +Proof. + rapply isqiso_catie'; assumption. +Defined. + +Definition catie_isqiso `{HasEquivs n A} + {a b : A} (f : a $-> b) `{!IsQIso f} + : CatIsEquiv f. +Proof. + rapply catie_isqiso'; assumption. +Defined. + +Record CatEquiv `{HasEquivs n A} (a b : A) := +{ + cate_fun : a $-> b ; + catie_cate : CatIsEquiv cate_fun ; +}. +Notation "a $<~> b" := (CatEquiv a b). +Arguments cate_fun {n A _ _ _ a b} f : rename. +Arguments Build_CatEquiv {n A _ _ _ a b} f fe : rename. +Coercion cate_fun : CatEquiv >-> Hom. +Global Existing Instance catie_cate. + +Definition cate_inverse `{HasEquivs n A} + {a b : A} (f : a $<~> b) + : b $<~> a. +Proof. + exists (qiso_inv f). + rapply catie_isqiso. +Defined. + +(** Because equivalences don't have to be coherent, it's technically possible to just use quasi-isomorphisms. However, this should never be used as "the" definition of equivalences; we only define it as a stepping stone on the way to bi-invertibility as the "default" notion. *) +CoFixpoint hasequivs_with_isqiso (n : nat) (A : Type) `{IsCat0 n A} + : HasEquivs n A. +Proof. + unshelve econstructor. + 1:intros a b f; exact (IsQIso f). + 1-2:intros; assumption. + intros; apply hasequivs_with_isqiso. +Defined. + +(** In truncated cases, however, things are easier. *) +CoFixpoint hasequivs_catcontr `{IsCat0 n A, !CatContr A} + : HasEquivs n A. +Proof. + unshelve econstructor; intros. + - exact Unit. + - exact tt. + - exact _. + - rapply hasequivs_catcontr. +Defined. +Global Existing Instance hasequivs_catcontr | 1000. + +Global Instance hasequivs_catprop `{IsCat0 n A, !CatProp A} + : HasEquivs n A. +Proof. + unshelve econstructor; intros. + - exact Unit. + - exact tt. + - exact _. + - rapply hasequivs_catcontr. +Defined. +Global Existing Instance hasequivs_catprop | 1000. + +Global Instance hasequivs_catposet `{IsCat0 n A, !CatPoset A} + : HasEquivs n A. +Proof. + unshelve econstructor; intros. + - exact (b $-> a). + - cbn. exact (qiso_inv f). + - apply isqiso_catposet. assumption. + - rapply hasequivs_catprop. +Defined. +Global Existing Instance hasequivs_catposet | 1000. + +Class CatIsIso `{IsCat0 1 A, !CatTrunc 1 A} {a b : A} (f : a $-> b) := +{ + catiso_inv : b $-> a ; + catiso_issect : catiso_inv $o f $== cat_id a ; + catiso_isretr : f $o catiso_inv $== cat_id b ; +}. +Arguments catiso_inv {A _ _ _ a b} f {_}. +Arguments catiso_issect {A _ _ _ a b} f {_}. +Arguments catiso_isretr {A _ _ _ a b} f {_}. + +Global Instance hasequivs_cat1cat `{IsCat0 1 A, !Cat1Cat A} + : HasEquivs 1 A | 1000. +Proof. + unshelve econstructor. + - intros a b f; exact (CatIsIso f). + - intros a b f ?; unshelve econstructor. + + exact (qiso_inv f). + + exact (qiso_issect f). + + exact (qiso_isretr f). + - cbn; intros a b f ?; srapply isqiso_cat1cat. + + exact (catiso_inv f). + + exact (catiso_issect f). + + exact (catiso_isretr f). + - intros; apply hasequivs_catposet. +Defined. + + +(** ** Conservative Functors *) + +(** A functor can be conservative at any collection of dimensions but not others, which we represent by a stream of booleans. *) +CoInductive IsConservative (bs : Stream Bool) + `{HasEquivs m A, HasEquivs n B} (F : A -> B) `{!IsFunctor0 F} := +{ + catie_conservative : forall {bt : IsTrue (head bs)} (a b : A) (f : a $-> b), + CatIsEquiv (fmap F f) -> CatIsEquiv f ; + catie_hom : forall (a b : A), + @IsConservative (tail bs) (pred m) (a $-> b) _ _ _ + (pred n) (F a $-> F b) _ _ _ (fmap F) _ ; +}. + +Existing Class IsConservative. +Global Existing Instance catie_hom. + +(** [catie_conservative] can't be an [Instance] because it would go into infinite loops. *) +Hint Immediate catie_conservative : typeclass_instances. + +(** The identity functor is conservative. *) +CoFixpoint isconservative_idmap `{HasEquivs m A} + : @IsConservative (const_stream true) m A _ _ _ m A _ _ _ idmap _. +Proof. + unshelve econstructor; intros. + - apply catie_isqiso, isqiso_catie; assumption. + - exact _. +Defined. +Global Existing Instance isconservative_idmap. + +(** The functor from an induced category structure to the original category should be conservative. First we prove that it reflects quasi-isomorphisms. *) +Local Instance isqiso_induced {A} `{HasEquivs n B} (F : A -> B) + {a b : A} (f : a $-> b) `{!IsQIso (fmap F f)} + : @IsQIso n A _ (iscat0_induced F) a b f. +Proof. + unshelve econstructor; cbn. + - exact (qiso_inv (fmap F f)). + - apply qiso_issect. + - apply qiso_isretr. + - exact (isqiso_qiso_issect (fmap F f) _). + - exact (isqiso_qiso_isretr (fmap F f) _). +Defined. + +(** You might think that's all we have to do, since "clearly" it also preserves quasi-isomorphisms. But actually we have to prove this clear fact, since we don't yet know that arbitrary functors preserve quasi-isomorphisms (which actually requires 1-coherence!). *) +Local Instance isqiso_fmap_induced {A} `{HasEquivs n B} (F : A -> B) + {a b : A} (f : a $-> b) + {fe : @IsQIso n A _ (iscat0_induced F) a b f} + : IsQIso (fmap F f). +Proof. + unshelve econstructor; cbn. + - exact (@qiso_inv _ _ _ _ _ _ f fe). + - exact (@qiso_issect _ _ _ _ _ _ f fe). + - exact (@qiso_isretr _ _ _ _ _ _ f fe). + - exact (@isqiso_qiso_issect _ _ _ _ _ _ f fe). + - exact (@isqiso_qiso_isretr _ _ _ _ _ _ f fe). +Defined. + +(** In order to actually state that the inducing functor is conservative, we need to first prove that the induced category [HasEquivs]. *) +Definition hasequivs_induced {A} `{HasEquivs n B} (F : A -> B) + : @HasEquivs n A _ (iscat0_induced F). +Proof. + unshelve econstructor. + - intros; eapply CatIsEquiv; eassumption. + - cbn; intros. rapply catie_isqiso. + - cbn; intros. apply isqiso_induced, isqiso_catie. exact _. + - intros. cbn. exact _. +Defined. + +Definition isconservative_induced {A} `{HasEquivs n B} (F : A -> B) + : @IsConservative (const_stream true) + n A _ _ (hasequivs_induced F) n B _ _ _ F _. +Proof. + unshelve econstructor; cbn; intros. + - apply catie_isqiso, isqiso_induced, isqiso_catie. + assumption. + - exact _. +Defined. + + +(** ** Categories of equivalences *) + +(** We induce a category structure on [a $<~> b] from [a $-> b]. *) + +Global Instance isglob_catequiv `{HasEquivs m A} (a b : A) + : IsGlob (pred m) (a $<~> b) + := isglob_induced (@cate_fun _ _ _ _ _ a b). + +Global Instance iscat0_catequiv `{HasEquivs m A} (a b : A) + : IsCat0 (pred m) (a $<~> b) + := iscat0_induced (@cate_fun _ _ _ _ _ a b). + +Global Instance hasequivs_catequiv `{HasEquivs m A} (a b : A) + : HasEquivs (pred m) (a $<~> b) + := hasequivs_induced (@cate_fun _ _ _ _ _ a b). + + +(** ** Bi-invertible maps *) + +(** The simplest general coherent definition of equivalence is a bi-invertible map. We will supply this as a default definition that the user can override if desired, by making it an instance with high cost (low priority). *) + +CoInductive CatBiInv `{IsCat0 n A} {a b : A} (f : a $-> b) := +{ + catbiinv_retr : b $-> a ; + catbiinv_issect : (catbiinv_retr $o f) $-> (cat_id a) ; + catbiinv_sect : b $-> a ; + catbiinv_isretr : (f $o catbiinv_sect) $-> (cat_id b) ; + catbiinv_catbiinv_issect : + @CatBiInv _ (a $-> a) _ _ _ _ catbiinv_issect ; + catbiinv_catbiinv_isretr : + @CatBiInv _ (b $-> b) _ _ _ _ catbiinv_isretr ; +}. + +(** Every quasi-isomorphism is bi-invertible. *) +CoFixpoint biinv_isqiso `{IsCat0 n A} {a b : A} (f : a $-> b) `{!IsQIso f} + : CatBiInv f. +Proof. + unshelve econstructor; intros. + 1,3: rapply (qiso_inv f). + 1: apply (qiso_issect f). + 1: apply (qiso_isretr f). + 1-2: apply biinv_isqiso; exact _. +Defined. + +(** However, to prove the converse requires more coherence. *) + +(** ** Displayed 0-coherent oo-categories *) + +(** It's not entirely clear what restrictions there should be on [m] and [n], and how they interact. The following definition amounts to saying that if [n=0] then the projection functor represented by a displayed category is conservative (equivalence-reflecting), and otherwise corecurses into hom-categories. This seems at least reasonable, since it restricts to the correct meaning of [n] when [A=Unit]. *) + +CoInductive IsDCat0 {m A} n B + `{IsDGlob m A n B} `{!IsCat0 m A} : Type := +{ + dcat_id : forall (a : A) (u : B a), DHom (cat_id a) u u ; + dcat_comp : forall (a b c : A) (u : B a) (v : B b) (w : B c) + (g : b $-> c) (f : a $-> b), + DHom g v w -> DHom f u v -> DHom (g $o f) u w ; + isdfunctor0_postcomp : forall (a b c : A) (u : B a) (v : B b) (w : B c) + (g : b $-> c) (q : DHom g v w), + IsDFunctor0 (fun f => g $o f) (fun f p => dcat_comp a b c u v w g f q p) ; + isdfunctor0_precomp : forall (a b c : A) (u : B a) (v : B b) (w : B c) + (f : a $-> b) (p : DHom f u v), + IsDFunctor0 (fun g => g $o f) (fun g q => dcat_comp a b c u v w g f q p) ; + dgpd_inv : forall (iszn : IsZeroNat n) + (a b : A) (u : B a) (v : B b) + (f : a $-> b) (fe : IsQIso f), + DHom f u v -> DHom (qiso_inv f) v u ; + isdcat0_dhom : forall (a b : A) (u : B a) (v : B b), + @IsDCat0 (pred m) (a $-> b) (pred n) (fun f => DHom f u v) _ _ _ ; +}. + +Existing Class IsDCat0. +Arguments dcat_id {m A n B _ _ _ _ a} u. +Arguments dcat_comp {m A n B _ _ _ _ a b c u v w g f} q p. +Notation "q $oD p" := (dcat_comp q p). +Arguments dgpd_inv {m A n B _ _ _ _ _ a b u v f fe} p. +Notation "p ^D$" := (dgpd_inv p). +Global Existing Instances + isdcat0_dhom isdfunctor0_postcomp isdfunctor0_precomp. + +Hint Extern 1 (@IsDCat0 ?m (Hom _ _ _) _ _ _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@IsDCat0 ?m (Hom _ _ _) _ _ _ _ _) => change_dim_0 m : typeclass_instances. +Hint Extern 1 (@IsDCat0 _ _ ?n _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@IsDCat0 _ _ ?n _ _ _ _) => change_dim_0 n : typeclass_instances. + +Definition dcat_postcomp `{IsDCat0 m A n B} + {a b c : A} (u : B a) {v : B b} {w : B c} + {g : b $-> c} (f : a $-> b) (q : DHom g v w) + : DHom f u v -> DHom (g $o f) u w + := fun p => q $oD p. + +Definition dcat_precomp `{IsDCat0 m A n B} + {a b c : A} {u : B a} {v : B b} (w : B c) + (g : b $-> c) {f : a $-> b} (p : DHom f u v) + : DHom g v w -> DHom (g $o f) u w + := fun q => q $oD p. + +Definition dcat_postwhisker `{IsDCat0 m A n B} + {a b c : A} {u : B a} {v : B b} {w : B c} + {f g : a $-> b} {h : b $-> c} {p : f $-> g} + {f' : DHom f u v} {g' : DHom g u v} + (h' : DHom h v w) (p' : DHom p f' g') + : DHom (h $ dcat_postcomp u k h') p'. + +Notation "h' $ c} {p : f $-> g} {h : a $-> b} + {f' : DHom f v w} {g' : DHom g v w} (p' : DHom p f' g') (h' : DHom h u v) + : DHom (p $o> h) (f' $oD h') (g' $oD h') + := dfmap (cat_precomp c h) (fun k => dcat_precomp w k h') p'. + +Notation "p $o>D h" := (dcat_prewhisker p h). + +(** ** Displayed quasi-isomorphisms *) + +CoInductive IsDQIso `{IsDCat0 m A n B} + {a b : A} {f : a $-> b} {fe : IsQIso f} + {u : B a} {v : B b} (g : DHom f u v) : Type := +{ + dqiso_inv : DHom (qiso_inv f) v u ; + dqiso_issect : DHom (qiso_issect f) (dqiso_inv $oD g) (dcat_id u) ; + dqiso_isretr : DHom (qiso_isretr f) (g $oD dqiso_inv) (dcat_id v) ; + isdqiso_issect : @IsDQIso (pred m) (a $-> a) (pred n) (fun h => DHom h u u) + _ _ _ _ _ _ _ _ _ _ dqiso_issect ; + isdqiso_isretr : @IsDQIso (pred m) (b $-> b) (pred n) (fun h => DHom h v v) + _ _ _ _ _ _ _ _ _ _ dqiso_isretr ; +}. + +Existing Class IsDQIso. +Arguments dqiso_inv {m A n B _ _ _ _ a b f _ u v} g {_}. +Arguments dqiso_issect {m A n B _ _ _ _ a b f _ u v} g {_}. +Arguments dqiso_isretr {m A n B _ _ _ _ a b f _ u v} g {_}. +Global Existing Instances isdqiso_issect isdqiso_isretr. + +Hint Extern 1 (@IsDQIso ?m (Hom _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@IsDQIso ?m (Hom _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim_0 m : typeclass_instances. +Hint Extern 1 (@IsDQIso _ _ ?n _ _ _ _ _ _ _ _ _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@IsDQIso _ _ ?n _ _ _ _ _ _ _ _ _ _ _ _) => change_dim_0 n : typeclass_instances. + +Global Instance isdqiso_inv `{IsDCat0 m A n B} + {a b : A} (f : a $-> b) `{!IsQIso f} + {u : B a} {v : B b} (g : DHom f u v) `{!IsDQIso g} + : IsDQIso (dqiso_inv g). +Proof. + unshelve econstructor. + - exact g. + - srapply dqiso_isretr. + - srapply dqiso_issect. + - exact _. + - exact _. +Defined. + +(** TODO: [IsDQIso] in truncated dcats *) + +(** ** Displayed categories with equivalences *) + +CoInductive DHasEquivs {m} {A} (n : nat) (B : A -> Type) + `{IsDCat0 m A n B, !HasEquivs m A} := +{ + DCatIsEquiv' : forall {a b : A} {f : a $-> b} {fe : CatIsEquiv f} + {u : B a} {v : B b}, DHom f u v -> Type ; + dcatie_isdqiso' : forall {a b : A} {f : a $-> b} {fe : IsQIso f} + {u : B a} {v : B b} (g : DHom f u v), + IsDQIso g -> DCatIsEquiv' (fe := catie_isqiso f) g ; + isdqiso_dcatie' : forall {a b : A} {f : a $-> b} {fe : CatIsEquiv f} + {u : B a} {v : B b} (g : DHom f u v), + DCatIsEquiv' g -> IsDQIso g; + dhasequivs_dhom : forall (a b : A) (u : B a) (v : B b), + @DHasEquivs (pred m) (a $-> b) (pred n) (fun f => DHom f u v) _ _ _ _ _ ; +}. +Existing Class DHasEquivs. +Global Existing Instance dhasequivs_dhom. + +Hint Extern 1 (@DHasEquivs ?m (Hom _ _ _) _ _ _ _ _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@DHasEquivs ?m (Hom _ _ _) _ _ _ _ _ _ _) => change_dim_0 m : typeclass_instances. +Hint Extern 1 (@DHasEquivs _ _ ?n _ _ _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@DHasEquivs _ _ ?n _ _ _ _ _ _) => change_dim_0 n : typeclass_instances. + +Class DCatIsEquiv `{DHasEquivs m A n B} {a b f fe u v} (g : DHom f u v) + := dcatie_dcatie : @DCatIsEquiv' m A n B _ _ _ _ _ _ a b f fe u v g. + +Arguments DCatIsEquiv : simpl never. + +Hint Extern 1 (@DCatIsEquiv ?m (Hom _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@DCatIsEquiv ?m (Hom _ _ _) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim_0 m : typeclass_instances. +Hint Extern 1 (@DCatIsEquiv _ _ ?n _ _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@DCatIsEquiv _ _ ?n _ _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim_0 n : typeclass_instances. + +Global Instance isdqiso_dcatie `{DHasEquivs m A n B} + {a b f} {u : B a} {v : B b} (g : DHom f u v) + `{!CatIsEquiv f, !DCatIsEquiv g} + : IsDQIso g. +Proof. + rapply isdqiso_dcatie'; assumption. +Defined. + +Definition dcatie_isdqiso `{DHasEquivs m A n B} + {a b f} {u : B a} {v : B b} (g : DHom f u v) + `{!IsQIso f, !IsDQIso g} + : DCatIsEquiv (fe := catie_isqiso f) g. +Proof. + rapply dcatie_isdqiso'; assumption. +Defined. + +Record DCatEquiv `{DHasEquivs m A n B} {a b} (f : a $<~> b) u v := +{ + dcate_fun : DHom f u v ; + dcatie_dcate : DCatIsEquiv dcate_fun ; +}. +Arguments Build_DCatEquiv {m A n B _ _ _ _ _ _ a b f u v} g ge : rename. +Arguments dcate_fun {m A n B _ _ _ _ _ _ a b f u v} g : rename. +Coercion dcate_fun : DCatEquiv >-> DHom. +Global Existing Instance dcatie_dcate. + +Definition dcate_inverse `{DHasEquivs m A n B} {a b} {f : a $<~> b} {u v} + (g : DCatEquiv f u v) + : DCatEquiv (cate_inverse f) v u. +Proof. + exists (dqiso_inv g). + apply dcatie_isdqiso. + exact _. +Defined. + +CoFixpoint dhasequivs_with_isdqiso {m A} n B + `{IsDCat0 m A n B} + : @DHasEquivs m A n B _ _ _ _ (hasequivs_with_isqiso m A). +Proof. + unshelve econstructor. + 1:intros a b f fe u v g; exact (IsDQIso g). + 1-2:intros; assumption. + intros; apply dhasequivs_with_isdqiso. +Defined. + +(** TODO: [DHasEquivs] in truncated categories *) diff --git a/theories/ooCat/Cat1.v b/theories/ooCat/Cat1.v new file mode 100644 index 00000000000..ea6bc0e767c --- /dev/null +++ b/theories/ooCat/Cat1.v @@ -0,0 +1,521 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Export ooCat.Cat0. + +(** * 1-coherent oo-categories *) + +Generalizable Variables m n p A B C. + +(** ** 1-coherent oo-functors *) + +CoInductive IsFunctor1 {m A n B} `{IsCat0 m A} `{HasEquivs n B} + (F : A -> B) {ff : IsFunctor0 F} : Type := +{ + fmap_id : forall (a : A), fmap F (cat_id a) $<~> cat_id (F a) ; + fmap_comp : forall (a b c : A) (f : a $-> b) (g : b $-> c), + fmap F (g $o f) $<~> fmap F g $o fmap F f ; + isfunctor1_fmap : forall (a b : A), + @IsFunctor1 _ (a $-> b) _ (F a $-> F b) _ _ _ _ _ (fmap' F a b) _ ; +}. + +(** TODO: Generalize to sections. Requires having displayed categories with equivalences. *) + +Existing Class IsFunctor1. +Arguments fmap_id {m A n B _ _ _ _ _} F {_ _} a. +Arguments fmap_comp {m A n B _ _ _ _ _} F {_ _ a b c} f g. +Global Existing Instance isfunctor1_fmap. + +Hint Extern 1 (@IsFunctor1 ?m (Hom _ _ _) _ _ _ _ _ _ _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@IsFunctor1 ?m (Hom _ _ _) _ _ _ _ _ _ _ _ _) => change_dim_0 m : typeclass_instances. +Hint Extern 1 (@IsFunctor1 _ _ ?n _ _ _ _ _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@IsFunctor1 _ _ ?n _ _ _ _ _ _ _ _) => change_dim_0 n : typeclass_instances. + + +(** ** 1-coherent oo-categories *) + +(** As before, we have to choose what "1-coherent" means. At the moment we are choosing "whatever is necessary to have a good theory of equivalences", which is somewhere in between the two principled choices. *) +CoInductive IsCat1 (n : nat) (A : Type) `{HasEquivs n A} := +{ + cat_assoc : 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 : forall (a b : A) (f : a $-> b), cat_id b $o f $<~> f ; + cat_idr : forall (a b : A) (f : a $-> b), f $o cat_id a $<~> f ; + gpd_issect : forall (isz : IsZeroNat n) (a b : A) (f : a $-> b), + f^$ $o f $<~> cat_id a ; + gpd_isretr : forall (isz : IsZeroNat n) (a b : A) (f : a $-> b), + f $o f^$ $<~> cat_id b ; + isfunctor1_postcomp : forall (a b c : A) (g : b $-> c), + IsFunctor1 (cat_postcomp a g) ; + isfunctor1_precomp : forall (a b c : A) (f : a $-> b), + IsFunctor1 (cat_precomp c f) ; + iscat1_hom : forall (a b : A), @IsCat1 (pred n) (a $-> b) _ _ _ ; +}. + +Existing Class IsCat1. +Arguments cat_assoc {n A _ _ _ _ a b c d} f g h. +Arguments cat_idl {n A _ _ _ _ a b} f. +Arguments cat_idr {n A _ _ _ _ a b} f. +Arguments gpd_issect {n A _ _ _ _ _ a b} f. +Arguments gpd_isretr {n A _ _ _ _ _ a b} f. +Global Existing Instances + iscat1_hom isfunctor1_postcomp isfunctor1_precomp. + +Hint Extern 1 (IsCat1 ?n _) => change_dim n : typeclass_instances. +Hint Extern 1 (IsCat1 ?n _) => change_dim_0 n : typeclass_instances. + + +(** ** Equivalences *) + +(** Now we can prove more about equivalences. *) + +(** Every morphism in a groupoid is an equivalence *) +Global Instance isqiso_gpd `{IsCat1 0 A} + {a b : A} (f : a $-> b) + : IsQIso f. +Proof. + unshelve econstructor. + - exact (gpd_inv f). + - exact (gpd_issect f). + - exact (gpd_isretr f). + - exact _. + - exact _. +Defined. + +Global Instance catie_gpd `{IsCat1 0 A} + {a b : A} (f : a $-> b) + : CatIsEquiv f. +Proof. + apply catie_isqiso; exact _. +Defined. + +(** We can "adjointify" in the usual way with equivalences in the next dimension. Note that the possibility of adjointification was basically built into the definition of [HasEquivs]; in concrete cases it needs to be proven. *) +Definition catie_adjointify `{HasEquivs n A} {a b : A} + (f : a $-> b) (g : b $-> a) + (s : g $o f $<~> cat_id a) (r : f $o g $<~> cat_id b) + : CatIsEquiv f. +Proof. + apply catie_isqiso; unshelve econstructor; intros. + - exact g. + - exact s. + - exact r. + - exact _. + - exact _. +Defined. + +Definition cate_adjointify `{HasEquivs n A} {a b : A} + (f : a $-> b) (g : b $-> a) + (s : g $o f $<~> cat_id a) (r : f $o g $<~> cat_id b) + : a $<~> b + := Build_CatEquiv f (catie_adjointify f g s r). + +(** The identity is an equivalence. *) +Global Instance catie_id `{IsCat1 n A} (a : A) + : CatIsEquiv (cat_id a). +Proof. + srapply catie_adjointify. + 1:apply cat_id. + all:apply cat_idl. +Defined. + +Definition cate_id `{IsCat1 n A} (a : A) + : a $<~> a + := Build_CatEquiv (cat_id a) _. + +Global Instance reflexive_cate `{IsCat1 n A} + : Reflexive (@CatEquiv n A _ _ _) + := cate_id. + +(** We use the equivalence inverse notation only in the bundled case. *) +Notation "f ^-1$" := (cate_inverse f). + +Global Instance symmetric_cate `{IsCat1 n A} + : Symmetric (@CatEquiv n A _ _ _) + := @cate_inverse n A _ _ _. + +(** TODO: Consider adjointifying one the following two lemmas so that they satisfy an [isadj] coherence. If we do that, it would be nice to give the user a way to specify that a particular notion of equivalence (e.g. [IsEquiv] for [Type]) is already adjointified, so that in that case these lemmas can preserve the homotopies supplied by the user. *) + +Definition cate_issect `{HasEquivs n A} {a b : A} (f : a $<~> b) + : f^-1$ $o f $<~> cat_id a. +Proof. + exists (qiso_issect f). + rapply catie_isqiso. +Defined. + +Definition cate_isretr `{HasEquivs n A} {a b : A} (f : a $<~> b) + : f $o f^-1$ $<~> cat_id b. +Proof. + exists (qiso_isretr f). + rapply catie_isqiso. +Defined. + +(** Equivalences are closed under composition and preserved by 1-coherent functors. Note that for this to go through, we need [IsCat1] to include 1-coherent functoriality of composition. + +This is a mutual induction on [n], which of course requires [n] to be finite. It can also be proven for (oo,oo)-categories using coinduction rather than induction, but that would require some complicated shenanigans to convince Coq to accept because Coq's guardedness checker for cofixpoints is more rudimentary. + +Note also that like many "chaining equivalence" proofs, this proof is substantially simpler when written for bundled [CatEquiv]s rather than unbundled [CatIsEquiv]s. Below we will deduce the corresponding results for the latter -- and, for technical reasons, redefine these afterwards. *) +Local Fixpoint cate_compose_temp {n : nat} `{IsCat1 n A} + {a b c : A} (f : a $<~> b) (g : b $<~> c) {struct n} + : a $<~> c +with cate_fmap_temp {m n : nat} `{HasEquivs m A} `{IsCat1 n B} + (F : A -> B) `{!IsFunctor0 F, !IsFunctor1 F} + {a b : A} (f : a $<~> b) {struct n} + : F a $<~> F b. +Proof. + - snrapply Build_CatEquiv. + 1:exact (g $o f). + destruct n; [ by apply catie_gpd | snrapply catie_adjointify ]. + + exact (f^-1$ $o g^-1$). + + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ (cat_assoc _ _ _) _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ _ (cate_issect f)). + refine (cate_fmap_temp _ _ _ _ _ _ _ _ _ _ _ + (cat_postcomp _ _) _ _ _ _ _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ (cat_assoc _ _ _)^-1$ _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ _ (cat_idl f)). + refine (cate_fmap_temp _ _ _ _ _ _ _ _ _ _ _ + (cat_precomp _ _) _ _ _ _ _). + apply cate_issect. + + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ (cat_assoc _ _ _) _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ _ (cate_isretr g)). + refine (cate_fmap_temp _ _ _ _ _ _ _ _ _ _ _ + (cat_postcomp _ _) _ _ _ _ _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ (cat_assoc _ _ _)^-1$ _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ _ (cat_idl g^-1$)). + refine (cate_fmap_temp _ _ _ _ _ _ _ _ _ _ _ + (cat_precomp _ _) _ _ _ _ _). + apply cate_isretr. + - snrapply Build_CatEquiv. + 1:exact (fmap F f). + destruct n; [ by apply catie_gpd | snrapply catie_adjointify ]. + + exact (fmap F f^-1$). + + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ (fmap_comp _ _ _)^-1$ _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ _ (fmap_id _ _)). + refine (cate_fmap_temp _ _ _ _ _ _ _ _ _ _ _ (fmap F) _ _ _ _ _). + apply cate_issect. + + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ (fmap_comp _ _ _)^-1$ _). + refine (cate_compose_temp _ _ _ _ _ _ _ _ _ _ (fmap_id _ _)). + refine (cate_fmap_temp _ _ _ _ _ _ _ _ _ _ _ (fmap F) _ _ _ _ _). + apply cate_isretr. +Defined. + +(** Because the underlying morphism of [g $oE f] is, by definition [g $o f] -- at least after [n] is destructed -- we can easily deduce the corresponding facts about unbundled equivalences. *) +Global Instance catie_compose `{IsCat1 n A} + {a b c : A} (f : a $-> b) (g : b $-> c) + `{!CatIsEquiv f} `{!CatIsEquiv g} + : CatIsEquiv (g $o f). +Proof. + destruct n; [ apply catie_gpd | ]. + pose (f' := Build_CatEquiv f _). + pose (g' := Build_CatEquiv g _). + change (CatIsEquiv (cate_compose_temp f' g')). + exact _. +Defined. + +(** Now we redefine [cate_compose] globally by re-bundling this up. The point of this is so that its underlying function computes definitionally without having to destruct [n] first. (I'm not sure whether there is a way to set it up so that the underlying *inverse* function also computes definitionally.) *) +Definition cate_compose {n : nat} `{IsCat1 n A} + {a b c : A} (f : a $<~> b) (g : b $<~> c) + : a $<~> c. +Proof. + snrapply Build_CatEquiv. + - exact (g $o f). + - exact _. +Defined. + +Notation "g $oE f" := (cate_compose f g). + +Global Instance transitive_cate `{IsCat1 n A} + : Transitive (@CatEquiv n A _ _ _) + := @cate_compose n A _ _ _ _. + +(** We do the same for functors. *) + +Global Instance catie_fmap `{HasEquivs m A} `{IsCat1 n B} + (F : A -> B) `{!IsFunctor0 F, !IsFunctor1 F} + {a b : A} (f : a $-> b) `{!CatIsEquiv f} + : CatIsEquiv (fmap F f). +Proof. + destruct n; [ apply catie_gpd | ]. + pose (f' := Build_CatEquiv f _). + change (CatIsEquiv (cate_fmap_temp F f')). + exact _. +Defined. + +Definition cate_fmap {m n : nat} `{HasEquivs m A} `{IsCat1 n B} + (F : A -> B) `{!IsFunctor0 F, !IsFunctor1 F} + {a b : A} (f : a $<~> b) + : F a $<~> F b. +Proof. + snrapply Build_CatEquiv. + - exact (fmap F f). + - exact _. +Defined. + +Notation cate_fmap' F a b := (@cate_fmap _ _ _ _ _ _ _ _ _ _ _ F _ _ a b) (only parsing). + +(** Hence equivalences are also closed under whiskering. *) +Definition cate_postwhisker `{IsCat1 n A} {a b c : A} + {f g : a $-> b} (h : b $-> c) (p : f $<~> g) + : h $o f $<~> h $o g + := cate_fmap (cat_postcomp a h) p. + +Notation "h $ c} (p : f $<~> g) (h : a $-> b) + : f $o h $<~> g $o h + := cate_fmap (cat_precomp c h) p. + +Notation "p $o>E h" := (cate_prewhisker p h) (at level 30). + +Definition cate_postcomp `{IsCat1 n A} + (a : A) {b c : A} (g : b $<~> c) + : (a $<~> b) -> (a $<~> c) + := fun f => g $oE f. + +Definition cate_precomp `{IsCat1 n A} + {a b : A} (c : A) (f : a $<~> b) + : (b $<~> c) -> (a $<~> c) + := fun g => g $oE f. + +Global Instance isfunctor0_cate_postcompose + {n : nat} `{IsCat1 n A} + {a b c : A} (g : b $<~> c) + : IsFunctor0 (cate_postcomp a g). +Proof. + snrapply Build_IsFunctor0. + - intros p q r; cbn. + exact (g $ b) + : IsFunctor0 (cate_precomp c f). +Proof. + snrapply Build_IsFunctor0. + - intros p q r; cbn. + exact (r $o> f). + - intros g h; cbn. + rapply isfunctor0_fmap. +Defined. + +Global Instance isfunctor1_cate_postcompose + {n : nat} `{IsCat1 n A} + {a b c : A} (g : b $<~> c) + : IsFunctor1 (cate_postcomp a g). +Proof. + snrapply Build_IsFunctor1. + - intros f. cbn. + nrapply fmap_id; exact _. + - intros f h k p q. cbn. + nrapply fmap_comp; exact _. + - intros; cbn. + nrapply isfunctor1_fmap. + exact _. +Defined. + +Global Instance isfunctor1_cate_precompose + {n : nat} `{IsCat1 n A} + {a b c : A} (f : a $<~> b) + : IsFunctor1 (cate_precomp c f). +Proof. + snrapply Build_IsFunctor1. + - intros g. cbn. + rapply (fmap_id (cat_precomp c f)). + - intros g h k p q. cbn. + rapply (fmap_comp (cat_precomp c f)). + - intros; cbn. + nrapply isfunctor1_fmap. + exact _. +Defined. + +Global Instance isfunctor0_cate_fmap + {m n : nat} `{HasEquivs m A} `{IsCat1 n B} + (F : A -> B) `{!IsFunctor0 F, !IsFunctor1 F} (a b : A) + : IsFunctor0 (cate_fmap' F a b). +Proof. + snrapply Build_IsFunctor0. + - intros f g p; cbn. + exact (fmap (fmap F) p). + - intros; cbn; exact _. +Defined. + +Global Instance isfunctor1_cate_fmap + {m n : nat} `{HasEquivs m A} `{IsCat1 n B} + (F : A -> B) `{!IsFunctor0 F, !IsFunctor1 F} (a b : A) + : IsFunctor1 (cate_fmap' F a b). +Proof. + snrapply Build_IsFunctor1. + - intros f; cbn. + apply fmap_id. exact _. + - intros f g h p q; cbn. + apply fmap_comp. exact _. + - intros f g. + change (IsFunctor1 (fmap' (fmap' F a b) f g)). + exact _. +Defined. + +(** ** Constant 1-coherent functors *) + +CoFixpoint isfunctor1_const `{IsCat0 m A} `{IsCat1 n B} (x : B) + : IsFunctor1 (@const A B x). +Proof. + snrapply Build_IsFunctor1. + { intro a. + reflexivity. } + { intros a b c f g. + symmetry. + cbn. + apply cat_idl. } + intros a b. + rapply isfunctor1_const. +Defined. + +Global Existing Instance isfunctor1_const. + + +(** ** Composition of 1-coherent functors *) + +CoFixpoint isfunctor1_idmap `{IsCat1 m A} + : @IsFunctor1 m A m A _ _ _ _ _ idmap _. +Proof. + rapply Build_IsFunctor1; intros; reflexivity. +Defined. + +(** We can now prove that 1-coherent functors compose. *) +CoFixpoint isfunctor1_compose `{IsCat1 m A} `{IsCat1 n B} `{IsCat1 p C} + (G : B -> C) `{!IsFunctor0 G, !IsFunctor1 G} + (F : A -> B) `{!IsFunctor0 F, !IsFunctor1 F} + : IsFunctor1 (G o F). +Proof. + unshelve econstructor. + - intros a. + refine (_ $oE cate_fmap (fmap G) (fmap_id F a)). + exact (fmap_id G (F a)). + - intros a b c f g. + refine (_ $oE cate_fmap (fmap G) (fmap_comp F f g)). + exact (fmap_comp G (fmap F f) (fmap F g)). + - intros a b; cbn. + exact (isfunctor1_compose _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fmap G) _ _ (fmap F) _ _). +Defined. + +Global Existing Instances isfunctor1_idmap isfunctor1_compose. + + +(** ** Induced 1-coherent categories *) + +(** This requires that identity maps are equivalences! *) +Global Instance isfunctor1_induced {A} `{IsCat1 n B} (F : A -> B) + : @IsFunctor1 n A n B _ (iscat0_induced F) _ _ _ F _. +Proof. + srapply Build_IsFunctor1; cbn; intros; reflexivity. +Defined. + +Definition iscat1_induced {A} `{IsCat1 n B} (F : A -> B) + : @IsCat1 n A _ _ (hasequivs_induced F). +Proof. + unshelve econstructor; cbn; intros. + - apply cat_assoc. + - apply cat_idl. + - apply cat_idr. + - apply gpd_issect. + - apply gpd_isretr. + - apply (@isfunctor1_postcomp n B _ _ _ _ (F _)). + - apply (@isfunctor1_precomp n B _ _ _ _ _ _ (F _)). + - exact _. +Defined. + +Global Instance iscat1_catequiv `{IsCat1 m A} (a b : A) + : IsCat1 (pred m) (a $<~> b) + := iscat1_induced (@cate_fun _ _ _ _ _ a b). + + + +(** ** Bi-invertible maps revisited *) + +(** Bi-invertible maps are equivalences *) +Fixpoint catie_biinv {n : nat} {A : Type} `{IsCat1 n A} + {a b : A} (f : a $-> b) (fe : CatBiInv f) {struct n} + : CatIsEquiv f. +Proof. + destruct n as [|n]. + 1:exact _. + assert (fissect : catbiinv_retr f fe $o f $<~> cat_id a). + { snrapply Build_CatEquiv. + + apply catbiinv_issect. + + nrapply catie_biinv; try exact _. + apply catbiinv_catbiinv_issect. } + assert (fisretr : f $o catbiinv_sect f fe $<~> cat_id b). + { snrapply Build_CatEquiv. + + apply catbiinv_isretr. + + nrapply catie_biinv; try exact _. + apply catbiinv_catbiinv_isretr. } + snrapply catie_adjointify. + - exact (catbiinv_retr f fe). + - apply fissect. + - refine (fisretr $oE _). + refine (f $E _) $oE _ $oE (_ $ B) `{!IsFunctor0 F, !IsFunctor1 F} + : @IsFunctor1 _ _ _ _ _ _ _ _ hasequivs_nudge_to_biinv F _. +Proof. + unshelve econstructor; intros. + 3: rapply isfunctor1_nudge_to_biinv. + all: snrapply Build_CatEquiv. + 1: apply fmap_id; exact _. + 2: apply fmap_comp; exact _. + all: cbn; apply catie_isqiso. + all: apply isqiso_catie; exact _. +Defined. + +CoFixpoint iscat1_nudge_to_biinv `{IsCat1 n A} + : @IsCat1 n A _ _ hasequivs_nudge_to_biinv. +Proof. + unshelve econstructor; intros. + 1-5: snrapply Build_CatEquiv. + 1: apply cat_assoc. + 2: apply cat_idl. + 3: apply cat_idr. + 4: apply gpd_issect. + 5: apply gpd_isretr. + 1-5: cbn; apply catie_isqiso. + 1-5: cbn; apply isqiso_catie; exact _. + 1-2: rapply isfunctor1_nudge_to_biinv. + cbn. (** This does something to the invisible implicit arguments; without it the corecursive call ends up unguarded. *) + apply iscat1_nudge_to_biinv. +Defined. + +(** If you want to use the default biinv as the [HasEquivs] for some wild category, after defining the [IsGlob] and [IsCat0] instances, construct an instance of the following class. Its field is an [IsCat1] but is *not* declared as an instance; instead we have the following two instances that extract the intended structure. *) + +Class IsCat1_Default n A `{IsCat0 n A} + := { iscat1_default : @IsCat1 n A _ _ (hasequivs_with_isqiso n A) }. + +Global Instance hasequivs_with_biinv `(ac : IsCat1_Default n A) + : HasEquivs n A | 100. +Proof. + rapply hasequivs_nudge_to_biinv. + apply iscat1_default. +Defined. + +Global Instance iscat1_with_biinv `(ac : IsCat1_Default n A) + : @IsCat1 n A _ _ (hasequivs_with_biinv ac) | 100. +Proof. + rapply iscat1_nudge_to_biinv. +Defined. diff --git a/theories/ooCat/Core.v b/theories/ooCat/Core.v new file mode 100644 index 00000000000..df383dc6e13 --- /dev/null +++ b/theories/ooCat/Core.v @@ -0,0 +1,46 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Export ooCat.Cat1. + +Generalizable Variables m n p A B C. + +(** ** Cores and opposites *) + +(** The core of a category is obtained by discarding noninvertible morphisms. We can do this at any selection of dimensions. We don't make this an [Instance], of course; the user must decide when and how to use it. *) +CoFixpoint isglob_gencore (bs : Stream Bool) `{HasEquivs m A} + : IsGlob m A. +Proof. + unshelve econstructor; intros a b; destruct (head bs). + 1:exact (a $<~> b). + 1:exact (a $-> b). + all: cbn; rapply (isglob_gencore (tail bs)). +Defined. + +(** We could combine cores with opposites by using a [Stream Laxity] instead. *) + +CoFixpoint isfunctor0_gencore (bs : Stream Bool) + `{HasEquivs m A, IsCat1 n B} + (F : A -> B) `{!IsFunctor0 F, !IsFunctor1 F} + : @IsFunctor0 m A n B (isglob_gencore bs) (isglob_gencore bs) F. +Proof. + snrapply Build_IsFunctor0; intros a b; cbn; destruct (head bs). + 1:apply (cate_fmap F). + 1:apply (fmap F). + all:cbn; srapply isfunctor0_gencore. +Defined. + +CoFixpoint iscat0_gencore (bs : Stream Bool) `{IsCat1 m A} + : @IsCat0 m A (isglob_gencore bs). +Proof. + unshelve econstructor; cbn; destruct (head bs). + 1: intros a b c g f; exact (g $oE f). + 1: intros a b c g f; exact (g $o f). + 1: intros a; apply cate_id. + 1: intros a; apply cat_id. + 1-4: cbn; intros a b c g; srapply isfunctor0_gencore. + 1: intros _ a b f; exact (f^-1$). + 1: intros; apply gpd_inv; assumption. + all: exact _. +Defined. + diff --git a/theories/ooCat/EquivCat.v b/theories/ooCat/EquivCat.v new file mode 100644 index 00000000000..24fde4103be --- /dev/null +++ b/theories/ooCat/EquivCat.v @@ -0,0 +1,24 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Export ooCat.Cat0. + +Generalizable Variables m n p A B C. + +(** * Equivalences of categories *) + +Class EssSplit {m A n B} `{IsCat0 m A, HasEquivs n B} + (F : A -> B) `{!IsFunctor0 F} := +{ + esssplit_obj : B -> A ; + esssplit_cate : forall a, F (esssplit_obj a) $<~> a ; +}. + +CoInductive IsEquivCat {m A n B} `{IsCat0 m A, HasEquivs n B} + (F : A -> B) `{!IsFunctor0 F} := +{ + isequivcat_esssplit : EssSplit F ; + isequivcat_hom : forall (a b : A), + @IsEquivCat (pred m) (a $-> b) (pred n) (F a $-> F b) + _ _ _ _ _ (fmap F) _; +}. diff --git a/theories/ooCat/Fibrations.v b/theories/ooCat/Fibrations.v new file mode 100644 index 00000000000..bf5d6eb444d --- /dev/null +++ b/theories/ooCat/Fibrations.v @@ -0,0 +1,27 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Export ooCat.Cat0. (* ooCat.Laxity. *) + +Generalizable Variables m n p A B C. + +(** * Fibrations *) + +(** TODO: Do general fibrations with Laxity. *) + + +(** ** Isofibrations *) + +(** An isofibration is a displayed category with isomorphism-lifting in all dimensions. *) +CoInductive IsIsoFib {m A} n B `{DHasEquivs m A n B} := +{ + lift_obj : forall {a b : A} (f : a $<~> b) (u : B a), B b ; + lift_cate : forall {a b : A} (f : a $<~> b) (u : B a), + DCatEquiv f u (lift_obj f u) ; + isisofib_dhom : forall {a b : A} {u : B a} {v : B b}, + @IsIsoFib (pred m) (a $-> b) (pred n) (fun f => DHom f u v) + _ _ _ _ _ _ ; +}. + +Existing Class IsIsoFib. +Global Existing Instance isisofib_dhom. diff --git a/theories/ooCat/Forall.v b/theories/ooCat/Forall.v new file mode 100644 index 00000000000..a8de4d9f1a9 --- /dev/null +++ b/theories/ooCat/Forall.v @@ -0,0 +1,106 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Import ooCat.Cat1. + +(** * Forall oo-groupoids (with plain types as base) *) + +(** [forall] preserves globular types. *) +CoFixpoint isglob_forall {n A} (B : A -> Type) `(forall a, IsGlob n (B a)) + : IsGlob n (forall a, B a). +Proof. + exists (fun f g => forall a, f a $-> g a); intros. + rapply isglob_forall. +Defined. + +Global Existing Instance isglob_forall. + +(** Postcomposing and precomposing between [forall] types preserves 0-coherent oo-functors. (TODO: Should probably be generalized to sections.) *) +CoFixpoint isfunctor0_postcompose {m n A} (B C : A -> Type) + `{forall a, IsGlob m (B a)} `{forall a, IsGlob n (C a)} + (F : forall a, B a -> C a) `{!forall a, IsFunctor0 (F a)} + : IsFunctor0 (fun f a => F a (f a)). +Proof. + unshelve econstructor. + - cbn; intros f g p a. + exact (fmap (F a) (p a)). + - intros; rapply isfunctor0_postcompose. +Defined. + +CoFixpoint isfunctor0_precompose {n A B} (h : A -> B) + (C : B -> Type) `{forall a, IsGlob n (C a)} + : IsFunctor0 (fun f a => f (h a)). +Proof. + unshelve econstructor. + - cbn; intros f g p a. + exact (p (h a)). + - intros; rapply isfunctor0_precompose. +Defined. + +Global Existing Instances isfunctor0_postcompose isfunctor0_precompose. + +(** [forall] preserves 0-coherent oo-categories. *) +CoFixpoint iscat0_forall {n A} (B : A -> Type) + {bg : forall a, IsGlob n (B a)} {bc : forall a, IsCat0 n (B a)} + : IsCat0 n (forall a, B a). +Proof. + unshelve econstructor; cbn. + - intros f g h q p a; exact (q a $o p a). + - intros f a; exact (cat_id (f a)). + - intros; rapply isfunctor0_postcompose. + - intros f g h p; rapply isfunctor0_postcompose. + - intros ? f g p a. apply gpd_inv, p. + - intros; rapply iscat0_forall. +Defined. + +Global Existing Instance iscat0_forall. + +(** A pointwise quasi-isomorphism in a [forall] is a quasi-isomorphism. *) +CoFixpoint isqiso_forall {n A} (B : A -> Type) + {bg : forall a, IsGlob n (B a)} {bc : forall a, IsCat0 n (B a)} + (f g : forall a, B a) + (p : f $-> g) `{forall a, IsQIso (p a)} + : IsQIso p. +Proof. + unshelve econstructor. + - exact (fun a => qiso_inv (p a)). + - cbn; intros a. exact (qiso_issect (p a)). + - cbn; intros a. exact (qiso_isretr (p a)). + - rapply isqiso_forall. intros; exact (isqiso_qiso_issect (p a) _). + - rapply isqiso_forall. intros; exact (isqiso_qiso_isretr (p a) _). +Defined. + +(** And conversely. *) +CoFixpoint isqiso_from_forall {n A} (B : A -> Type) + {bg : forall a, IsGlob n (B a)} {bc : forall a, IsCat0 n (B a)} + (f g : forall a, B a) + (p : f $-> g) `{!IsQIso p} (a : A) + : IsQIso (p a). +Proof. + unshelve econstructor. + - exact (qiso_inv p a). + - exact (qiso_issect p a). + - exact (qiso_isretr p a). + - exact (@isqiso_from_forall _ _ _ _ _ _ _ (qiso_issect p) (isqiso_qiso_issect p _) a). + - exact (@isqiso_from_forall _ _ _ _ _ _ _ (qiso_isretr p) (isqiso_qiso_isretr p _) a). +Defined. + +CoFixpoint hasequivs_forall {n A} (B : A -> Type) + {bg : forall a, IsGlob n (B a)} + {bc : forall a, IsCat0 n (B a)} + {bh : forall a, HasEquivs n (B a)} + : HasEquivs n (forall a, B a). +Proof. + unshelve econstructor. + - intros f g p; exact (forall a, CatIsEquiv (p a)). + - intros f g p pe a; cbn. + apply catie_isqiso; rapply isqiso_from_forall. + - intros f g p pe; cbn. + apply isqiso_forall; intros a. + apply isqiso_catie, pe. + - intros; rapply hasequivs_forall. +Defined. + +Global Existing Instance hasequivs_forall. + +(** TODO: 1-coherent functors and categories *) diff --git a/theories/ooCat/Glob.v b/theories/ooCat/Glob.v new file mode 100644 index 00000000000..e5668b76280 --- /dev/null +++ b/theories/ooCat/Glob.v @@ -0,0 +1,370 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. + +(** * Globular types *) + +Generalizable Variables m n p A B C. + +(** ** Category Dimensions *) + +(** We parametrize by a natural number that will indicate the invertibility dimension, i.e. for [n] we are talking about (oo,n)-categories. Of course, at the level of mere globular sets it doesn't mean anything substative, but it will allow us to use a different notation when we know we're in the invertible dimension. *) + +(** Many of our definitions involve coinductive clauses that pass to hom-types and take the predecessor of the dimension. These are sometimes hard for typeclass inference to find because it can't guess that [n] should be matched as [(n.+1).-1] or that [0] should be matched as [0.-1]. So we use the following hints. We do unfortunately have to declare these hints separately for each typeclass we want it to apply to, and each natural number argument of that class. *) + +Ltac change_dim n := + match n with + | (pred ?m) => fail 1 + | _ => progress change n with (pred (S n)) + end. + +Ltac change_dim_0 n := + match n with + | (pred ?m) => fail 1 + | 0%nat => progress change 0%nat with (pred 0) + end. + + +(** ** Basic Definition *) + +(** Note that this is a "negative coinductive type", defined like a record with "fields" (i.e. destructors) rather than with a constructor (although it does still *have* a constructor, like a record does). Negative coinductive types (new in Coq 8.9) make much more sense both syntactically and semantically than the previous "positive" version and should be used exclusively in new code. It seems that here [A] functions like a "non-uniform parameter", although a negative coinductive type cannot have "indices" like an inductive type. *) +CoInductive IsGlob@{u} (n : nat) (A : Type@{u}) : Type := +{ + Hom : A -> A -> Type@{u} ; + isglob_hom : forall (x y : A), IsGlob n.-1 (Hom x y) ; +}. +(* Technically this definition could allow two universe parameters, [A : Type@{u1}] and [Hom a b : Type@{u0}] with u0 <= u1. But nearly all subsequent definitions force [u0 = u1]. Moreover, curiously, allowing [u0 != u1] here causes [iscat0_type] to fail with a universe error, while forcing [u0 = u1] here allows [iscat0_type] to succeed. I don't fully understand why that is. *) + +Existing Class IsGlob. +Arguments Hom {n} A {_} a b. +Notation "a $-> b" := (@Hom _ _ _ a b). +Notation "a $== b" := (@Hom 0 _ _ a b). (** In the invertible dimensions, we use a notation that looks more like paths or homotopies *) +Global Existing Instance isglob_hom. + +(** Here are our first predecessor hint declarations. *) +Hint Extern 1 (IsGlob ?n (Hom _ _ _)) => change_dim n : typeclass_instances. +Hint Extern 1 (IsGlob ?n (Hom _ _ _)) => change_dim_0 n : typeclass_instances. + +(** Sometimes it's convenient to move the [n] around, since it doesn't matter at the level of globular sets. *) +CoFixpoint isglob_reindex {m n : nat} {A : Type} `{IsGlob m A} + : IsGlob n A. +Proof. + unshelve econstructor. + - rapply (@Hom m). + - intros. nrapply (isglob_reindex (pred m) (pred n)). + clear isglob_reindex; exact _. +Defined. + +(** We can induce a globular structure by pullback along a function. This is not an instance, of course; we have to choose when to apply it. *) +Definition isglob_induced {A} `{IsGlob n B} (F : A -> B) : IsGlob n A + := Build_IsGlob n A (fun a b => F a $-> F b) _. + + +(** ** Dependent/displayed globular types *) + +(** For now, we require no relation between the invertibility dimensions of [A] and [B]. *) +CoInductive IsDGlob {m : nat} {A : Type@{u}} (n : nat) (B : A -> Type@{u}) + `{IsGlob m A} : Type := +{ + DHom : forall (a b : A) (f : a $-> b) (u : B a) (v : B b), Type@{u} ; + isdglob_dhom : forall (a b : A) (u : B a) (v : B b), + @IsDGlob (pred m) (a $-> b) (pred n) (fun f => DHom a b f u v) _ ; +}. + +Existing Class IsDGlob. +Arguments DHom {m A n B _ _ a b} f u v. +(** Since [DHom] has three arguments that generally need to be given explicitly, we don't try to give it an infix notation. *) +Global Existing Instance isdglob_dhom. + +Hint Extern 1 (IsDGlob ?n _) => change_dim n : typeclass_instances. +Hint Extern 1 (IsDGlob ?n _) => change_dim_0 n : typeclass_instances. +Hint Extern 1 (@IsDGlob ?m (Hom _ _ _) _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@IsDGlob ?m (Hom _ _ _) _ _ _) => change_dim_0 m : typeclass_instances. + +CoFixpoint isdglob_reindex {m n m' n' : nat} `{IsDGlob m A n B} + : @IsDGlob m' A n' B isglob_reindex. +Proof. + unshelve econstructor. + - rapply (@DHom m A n B _ _). + - intros. + nrapply (isdglob_reindex (pred m) (pred n) (pred m') (pred n')). + rapply (@isdglob_dhom m A n B _ _ a b u v). +Defined. + +(** Constant families of globular types are dependently globular. *) +CoFixpoint constant_dglob `{IsGlob m A} `{IsGlob n B} + : IsDGlob n (@const A Type B). +Proof. + unshelve econstructor. + - intros ? ? ? u v; exact (u $-> v). + - intros; rapply constant_dglob. +Defined. + +Global Existing Instance constant_dglob. + + +(** ** Sections of dependent globular types, i.e. dependent 0-coherent oo-functors *) + +CoInductive IsCatSect0 {m A n B} `{IsDGlob m A n B} (F : forall a, B a) := +{ + fmapD : forall (a b : A) (f : a $-> b), DHom f (F a) (F b) ; + iscatsect0_fmapD : forall (a b : A), + @IsCatSect0 (pred m) (a $-> b) (pred n) (fun f => DHom f (F a) (F b)) + _ _ (fmapD a b) ; +}. + +Existing Class IsCatSect0. +Arguments fmapD {_ _ _ _ _ _} F {_ a b} f. +Global Existing Instance iscatsect0_fmapD. + +Hint Extern 1 (@IsCatSect0 ?m (Hom _ _ _) _ _ _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@IsCatSect0 ?m (Hom _ _ _) _ _ _ _ _) => change_dim_0 m : typeclass_instances. +Hint Extern 1 (@IsCatSect0 _ _ ?n _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@IsCatSect0 _ _ ?n _ _ _ _) => change_dim_0 n : typeclass_instances. + +(** Often we want to specify the objects explicitly. *) +Notation fmapD' F a b := (@fmapD _ _ _ _ _ _ F _ a b) (only parsing). + +CoFixpoint iscatsect0_reindex {m n m' n' : nat} `{IsDGlob m A n B} + (F : forall a, B a) `{!IsCatSect0 F} + : @IsCatSect0 m' A n' B isglob_reindex isdglob_reindex F. +Proof. + unshelve econstructor. + - cbn. intros a b f; exact (fmapD F f). + - intros a b; cbn. apply iscatsect0_reindex. + apply iscatsect0_fmapD. +Defined. + +(** ** 0-coherent oo-functors, i.e. globular morphisms *) + +(** Just as non-dependent functions are a special case of dependent ones, ordinary functors are definitionally a special case of sections of displayed categories. But it's convenient to make them syntactically distinct. *) + +(* +CoInductive IsFunctor0 {A B : Type} `{IsGlob A} `{IsGlob B} (F : A -> B) : Type := +{ + fmap : forall (a b : A), (a $-> b) -> (F a $-> F b) ; + isfunctor0_fmap : forall (a b : A), @IsFunctor0 (a $-> b) (F a $-> F b) _ _ (fmap a b) ; +}. + +Existing Class IsFunctor0. +Arguments fmap {_ _ _ _} F {_ a b} f. +Global Existing Instance isfunctor0_fmap. +*) + +(** TODO: Consider making this a Notation instead. *) + +Class IsFunctor0 {m A n B} `{IsGlob m A} `{IsGlob n B} (F : A -> B) := + iscatsect0_isfunctor0 : @IsCatSect0 m A n (const B) _ _ F. +Global Existing Instance iscatsect0_isfunctor0. + +(** This is a syntactic variant of [Build_IsCatSect0] for non-dependent functors that leaves its coinductive goal written in terms of [IsFunctor0] instead of [IsCatSect0]. Unfortunately, it is not officially a "constructor" of [IsFunctor0], so tactics like [econstructor] won't use it. *) +Definition Build_IsFunctor0 `{IsGlob m A} `{IsGlob n B} (F : A -> B) + (fmap' : forall (a b : A), (a $-> b) -> (F a $-> F b)) + (isfunctor0_fmap' : forall (a b : A), IsFunctor0 (fmap' a b)) + : IsFunctor0 F + := Build_IsCatSect0 _ _ _ _ _ _ F fmap' isfunctor0_fmap'. + +Definition fmap `{IsGlob m A} `{IsGlob n B} (F : A -> B) `{!IsFunctor0 F} + {a b : A} (f : a $-> b) + : F a $-> F b + := fmapD F f. + +Notation fmap' F a b := (@fmap _ _ _ _ _ _ F _ a b) (only parsing). + +Hint Extern 1 (@IsFunctor0 _ _ ?n _ _ _ _) => change_dim n : typeclass_instances. +Hint Extern 1 (@IsFunctor0 _ _ ?n _ _ _ _) => change_dim_0 n : typeclass_instances. +Hint Extern 1 (@IsFunctor0 ?m (Hom _ _ _) _ _ _ _ _) => change_dim m : typeclass_instances. +Hint Extern 1 (@IsFunctor0 ?m (Hom _ _ _) _ _ _ _ _) => change_dim_0 m : typeclass_instances. + +Global Instance isfunctor0_fmap `{IsGlob m A} `{IsGlob n B} + (F : A -> B) `{!IsFunctor0 F} {a b : A} + : @IsFunctor0 _ (a $-> b) _ (F a $-> F b) _ _ (fmap' F a b) + := iscatsect0_fmapD F _ a b. + +(** Unfortunately, since [isglob_reindex] is not definitionally equal to [isdglob_reindex] applied to a [constant_dglob], we have to prove this separately rather than appeal to [iscatsect0_reindex]. *) +CoFixpoint isfunctor0_reindex {m n m' n' : nat} `{IsGlob m A, IsGlob n B} + (F : A -> B) `{!IsFunctor0 F} + : @IsFunctor0 m' A n' B isglob_reindex isglob_reindex F. +Proof. + snrapply Build_IsFunctor0. + - intros a b f; cbn. apply fmap; assumption. + - intros a b; cbn. apply isfunctor0_reindex. + exact _. +Defined. + +(** The identity functor *) +CoFixpoint isfunctor0_idmap `{IsGlob m A} + : @IsFunctor0 m A m A _ _ idmap. +Proof. + refine (Build_IsFunctor0 _ _ _). +Defined. + +(** Composition of functors *) +CoFixpoint isfunctor0_compose `{IsGlob m A} `{IsGlob n B} `{IsGlob p C} + (G : B -> C) `{!IsFunctor0 G} (F : A -> B) `{!IsFunctor0 F} + : IsFunctor0 (G o F). +Proof. + unshelve econstructor. + - intros a b; exact (fmap G o fmap' F a b). + - intros a b; cbn. + exact (isfunctor0_compose _ _ _ _ _ _ _ _ _ (fmap G) _ (fmap F) _). +Defined. + +Global Existing Instances isfunctor0_idmap isfunctor0_compose. + +Global Instance isfunctor0_induced {A} `{IsGlob n B} (F : A -> B) + : @IsFunctor0 n A n B (isglob_induced F) _ F. +Proof. + rapply Build_IsFunctor0. +Defined. + +(** ** Dependent 0-coherent functors *) + +(** These could alternatively be defined as sections of [B2] pulled back to [sig B1]. Conversely, a section of [B : A -> Type] could be defined as a dependent functor from [const Unit] to [B] over [idmap]. *) +CoInductive IsDFunctor0 {m1 A1 n1 B1 m2 A2 n2 B2} + `{IsDGlob m1 A1 n1 B1} `{IsDGlob m2 A2 n2 B2} + (F : A1 -> A2) `{!IsFunctor0 F} (G : forall a:A1, B1 a -> B2 (F a)) := +{ + dfmap : forall (a b : A1) (u : B1 a) (v : B1 b) (f : a $-> b), + DHom f u v -> DHom (fmap F f) (G a u) (G b v) ; + isdfunctor0_dfmap : forall (a b : A1) (u : B1 a) (v : B1 b), + @IsDFunctor0 _ _ _ _ _ _ _ _ _ _ _ _ (fmap F) _ (dfmap a b u v) ; +}. + +Existing Class IsDFunctor0. +Arguments dfmap {_ _ _ _ _ _ _ _ _ _ _ _} F {_} G {_ a b u v f} p. +Global Existing Instance isdfunctor0_dfmap. + +Hint Extern 1 (@IsDFunctor0 ?m1 _ _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim m1 : typeclass_instances. +Hint Extern 1 (@IsDFunctor0 ?m1 _ _ _ _ _ _ _ _ _ _ _ _ _ _) => change_dim_0 m1 : typeclass_instances. +Hint Extern 1 (@IsDFunctor0 _ _ ?n1 _ _ _ _ _ _ _ _ _ _ _ _) => change_dim n1 : typeclass_instances. +Hint Extern 1 (@IsDFunctor0 _ _ ?n1 _ _ _ _ _ _ _ _ _ _ _ _) => change_dim_0 n1 : typeclass_instances. +Hint Extern 1 (@IsDFunctor0 _ _ _ _ ?m2 _ _ _ _ _ _ _ _ _ _) => change_dim m2 : typeclass_instances. +Hint Extern 1 (@IsDFunctor0 _ _ _ _ ?m2 _ _ _ _ _ _ _ _ _ _) => change_dim_0 m2 : typeclass_instances. +Hint Extern 1 (@IsDFunctor0 _ _ _ _ _ _ ?n2 _ _ _ _ _ _ _ _) => change_dim n2 : typeclass_instances. +Hint Extern 1 (@IsDFunctor0 _ _ _ _ _ _ ?n2 _ _ _ _ _ _ _ _) => change_dim_0 n2 : typeclass_instances. + +(** ** The identity dependent functor *) + +CoFixpoint isdfunctor0_idmap `{IsDGlob m A n B} + : IsDFunctor0 idmap (fun a => idmap). +Proof. + unshelve econstructor. + - intros a b u v f g; exact g. + - intros a b u v; apply isdfunctor0_idmap. +Defined. + +(** ** Composition of dependent functors with sections *) + +CoFixpoint iscatsect0_isdfunctor0_compose {m A n1 B1 n2 B2} + `{IsDGlob m A n1 B1} `{!IsDGlob n2 B2} + (G : forall a:A, B1 a -> B2 a) `{!IsDFunctor0 idmap G} + (F : forall a:A, B1 a) `{!IsCatSect0 F} + : IsCatSect0 (fun a => G a (F a)). +Proof. + unshelve econstructor. + - intros a b f. + exact (dfmap idmap G (fmapD F f)). + - intros a b. + exact (@iscatsect0_isdfunctor0_compose + (pred m) (a $-> b) (pred n1) (fun f => DHom f (F a) (F b)) (pred n2) (fun f => DHom f (G a (F a)) (G b (F b))) + _ _ _ (fun f => dfmap idmap G (f := f)) + (isdfunctor0_dfmap idmap G _ a b (F a) (F b)) (fmapD' F a b) _). +Defined. + +(** ** Pullback of dependent globular types *) + +CoFixpoint isdglob_compose {A1 A2 : Type} (B : A2 -> Type) + `{IsGlob m1 A1} `{IsDGlob m2 A2 n B} + (F : A1 -> A2) `{!IsFunctor0 F} + : IsDGlob n (B o F). +Proof. + unshelve econstructor. + - intros a b f u v; exact (DHom (fmap F f) u v). + - intros a b u v. + refine (isdglob_compose _ (F a $-> F b) (fun g => DHom g u v) + _ _ _ _ _ _ (fmap F) _). +Defined. +Existing Instance isdglob_compose. + +(** Tlsil has suggested that we could also define a dependent globular type to be a globular map into a globular type of spans. This would make [isdglob_compose] an instance of [isfunctor0_compose]. But it would require defining globular maps before dependent globular types, with the effect that globular maps wouldn't be definitionally globular sections of constant dependent globular types. *) + + +(** ** Truncatedness *) + +(** We define a coinductive "categorical" notion of truncatedness. A category is contractible (as a category), a.k.a. (-2)-truncated if it is inhabited and all its hom-categories are contractible. And it is [n.+1]-truncated if all its hom-categories are [n]-truncated. *) + +CoInductive CatTrunc (n : trunc_index) {m : nat} (A : Type) `{IsGlob m A} := +{ + cat_center' : forall (isc : IsMinusTwo n), A ; + cattrunc_hom : forall (a b : A), @CatTrunc (n.-1) _ (a $-> b) _ ; +}. +Existing Class CatTrunc. +Global Existing Instance cattrunc_hom. + +Hint Extern 1 (@CatTrunc _ ?m (Hom _ _ _) _) => change_dim m : typeclass_instances. +Hint Extern 1 (@CatTrunc _ ?m (Hom _ _ _) _) => change_dim_0 m : typeclass_instances. + +Definition cat_center `{CatTrunc (-2) m A} : A + := @cat_center' (-2) m A _ _ tt. + +Global Instance cattrunc_hom_succ `{CatTrunc n.+1 m A} (a b : A) + : CatTrunc n (a $-> b) + := @cattrunc_hom n.+1 m A _ _ a b. + +Global Instance cattrunc_hom_minustwo `{CatTrunc (-2) m A} (a b : A) + : CatTrunc (-2) (a $-> b) + := @cattrunc_hom (-2) m A _ _ a b. + +CoFixpoint cattrunc_pred `{CatTrunc n.-1 m A} + : CatTrunc n A. +Proof. + unshelve econstructor. + - destruct n as [|n]; cbn in *. + + intros; apply cat_center. + + intros []. + - intros; cbn. + apply cattrunc_pred. + rapply cattrunc_hom. +Defined. + +CoFixpoint cattrunc_reindex {m'} `{CatTrunc n m A} + : @CatTrunc n m' A isglob_reindex. +Proof. + unshelve econstructor. + - apply (cat_center' n A _). + - intros; cbn. + rapply (cattrunc_reindex (pred m')). +Defined. +Global Existing Instance cattrunc_reindex. + +Notation CatContr := (CatTrunc (-2)). +Notation CatProp := (CatTrunc (-1)). +Notation CatPoset := (CatTrunc 0). +Notation Cat1Cat := (CatTrunc 1). + +(** TODO: truncated displayed categories *) + +(** ** Universal properties *) + +Class IsInitial `{IsGlob n A} (a : A) := + catcontr_initial : forall b, CatContr (a $-> b). +Global Existing Instance catcontr_initial. + +Class HasInitial `{IsGlob n A} := +{ + initial_obj : A ; + isinitial_initial : IsInitial initial_obj ; +}. +Global Existing Instance isinitial_initial. + +Class IsTerminal `{IsGlob n A} (a : A) := + catcontr_terminal : forall b, CatContr (b $-> a). +Global Existing Instance catcontr_terminal. + +Class HasTerminal `{IsGlob n A} := +{ + terminal_obj : A ; + isterminal_terminal : IsTerminal terminal_obj ; +}. +Global Existing Instance isterminal_terminal. diff --git a/theories/ooCat/Laxity.v b/theories/ooCat/Laxity.v new file mode 100644 index 00000000000..ae8784db498 --- /dev/null +++ b/theories/ooCat/Laxity.v @@ -0,0 +1,37 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Import ooCat.Cat1. + +Generalizable Variables m n p A B C. + +(** ** Laxity *) + +(** Various things in higher category theory, such as comma categories and natural transformations, can be lax, colax, or pseudo separately at all levels. In keeping with our coinductive approach, we define such an infinite list of notions of laxity as a coinductive stream. *) + +Inductive Laxity := +| colax : Laxity +| pseudo : Laxity +| lax : Laxity. + +Notation oplax := colax (only parsing). + +CoFixpoint all_pseudo : Stream Laxity := SCons pseudo all_pseudo. +Definition one_lax : Stream Laxity := SCons lax all_pseudo. +Definition one_colax : Stream Laxity := SCons colax all_pseudo. + +(** It may seem backwards for [colax] to mean a morphism "forwards" and [lax] a morphism "backwards", but that's what matches the standard terminology for natural transformations. *) +Definition lHom (l : Laxity) `{HasEquivs n A} (a b : A) := + match l with + | colax => (a $-> b) + | pseudo => (a $<~> b) + | lax => (b $-> a) + end. + +Definition lcat_id (l : Laxity) `{IsCat1 n A} (a : A) + : lHom l a a + := match l return lHom l a a with + | colax => cat_id a + | pseudo => cate_id a + | lax => cat_id a + end. diff --git a/theories/ooCat/Paths.v b/theories/ooCat/Paths.v new file mode 100644 index 00000000000..bfd8a4d41ae --- /dev/null +++ b/theories/ooCat/Paths.v @@ -0,0 +1,60 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Import ooCat.Cat1. + +Generalizable Variables A B. + +(** * Path oo-groupoids *) + +(** Every type is a globular type with its tower of identity types. *) +CoFixpoint isglob_withpaths (A : Type) : IsGlob 0 A. +Proof. + exists (@paths A); intros. + apply isglob_withpaths. +Defined. + +(** We could make this a global but low-priority instance, but doing so seems to break stuff later. *) +(* Global Existing Instance isglob_withpaths | 1000. *) +Local Existing Instance isglob_withpaths. + +(** Any function is a 0-coherent oo-functor between types equipped with their globular tower of identity types. As for [isglob_withpaths], we don't make this an [Instance]. *) +CoFixpoint isfunctor0_withpaths {A B : Type} (F : A -> B) + : IsFunctor0 F. +Proof. + refine (Build_IsFunctor0 F _ _). + exact (@ap A B F). + (** The coinductive assumption is found by typeclass search. *) +Defined. + +Local Existing Instance isfunctor0_withpaths. + +(** The tower of identity types is a 0-coherent oo-category with path composition. Again, not an [Instance]. *) +CoFixpoint iscat0_withpaths (A : Type) : IsCat0 0 A. +Proof. + unshelve econstructor. + - intros a b c p q; exact (q @ p). + - intros a; exact idpath. + - intros; cbn; apply isfunctor0_withpaths. + - intros; cbn; apply isfunctor0_withpaths. + - intros ? a b f; exact (f^). + - intros; apply iscat0_withpaths. +Defined. + +Local Existing Instance iscat0_withpaths. + +(** TODO: Any dependent type should be a displayed 0-coherent oo-category with its tower of dependent identity types. *) + +(** Every path is a quasi-isomorphism. *) +CoFixpoint isqiso_withpaths {A : Type} {a b : A} (p : a = b) + : IsQIso p. +Proof. + unshelve econstructor. + - exact (p^). + - cbn. apply concat_pV. + - cbn. apply concat_Vp. + - apply isqiso_withpaths. + - apply isqiso_withpaths. +Defined. + +(** TODO: 1-coherent functors, 1-coherent categories *) diff --git a/theories/ooCat/Prod.v b/theories/ooCat/Prod.v new file mode 100644 index 00000000000..2e1cca43ed5 --- /dev/null +++ b/theories/ooCat/Prod.v @@ -0,0 +1,63 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Import ooCat.Cat1. + +Generalizable Variables m n X A B. + +(** * Product categories *) + +(** For now, we assume that [A] and [B] have the same invertibility dimension. We could instead let them be different and take the min for the dimension of the product. *) + +CoFixpoint isglob_prod `{IsGlob n A} `{IsGlob n B} + : IsGlob n (A * B). +Proof. + unshelve econstructor. + - intros [a1 b1] [a2 b2]; exact ((a1 $-> a2) * (b1 $-> b2)). + - intros [a1 b1] [a2 b2]. rapply isglob_prod. +Defined. + +Global Existing Instance isglob_prod. + +CoFixpoint isfunctor0_prod + `{IsGlob m A1} `{IsGlob n B1} `{IsGlob m A2} `{IsGlob n B2} + (F1 : A1 -> B1) (F2 : A2 -> B2) + `{!IsFunctor0 F1} `{!IsFunctor0 F2} + : IsFunctor0 (fun z:A1*A2 => (F1 (fst z), F2 (snd z))). +Proof. + simple notypeclasses refine (Build_IsFunctor0 _ _ _). + - intros [a1 a2] [b1 b2] [f1 f2]; cbn. + exact (fmap F1 f1 , fmap F2 f2). + - intros; cbn; apply isfunctor0_prod; apply isfunctor0_fmap. +Defined. + +CoFixpoint iscat0_prod `{IsCat0 n A} `{IsCat0 n B} + : IsCat0 n (A * B). +Proof. + unshelve econstructor. + - intros [a1 b1] [a2 b2] [a3 b3] [f1 g1] [f2 g2]. + exact (f1 $o f2, g1 $o g2). + - intros [a1 b1]. + exact (cat_id a1, cat_id b1). + - intros [a1 b1] [a2 b2] [a3 b3] [h k]; cbn. + apply isfunctor0_prod; apply isfunctor0_postcomp. + - intros [a1 b1] [a2 b2] [a3 b3] [h k]; cbn. + refine (isfunctor0_prod (fun g => g $o h) (fun g => g $o k)). + - intros ? [a1 b1] [a2 b2] [f g]; exact (f^$, g^$). + - intros; rapply iscat0_prod. +Defined. + +Global Existing Instance iscat0_prod. + +CoFixpoint isfunctor0_pair `{IsGlob m X} `{IsGlob n A} `{IsGlob n B} + (F : X -> A) `{!IsFunctor0 F} (G : X -> B) `{!IsFunctor0 G} + : IsFunctor0 (fun x => (F x, G x)). +Proof. + simple notypeclasses refine (Build_IsFunctor0 _ _ _). + - intros x y f; exact (fmap F f, fmap G f). + - intros x y; rapply isfunctor0_pair. +Defined. + +Global Existing Instance isfunctor0_pair. + +(** TODO: HasEquivs, 1-coherent categories *) diff --git a/theories/ooCat/Sigma.v b/theories/ooCat/Sigma.v new file mode 100644 index 00000000000..657a2671c39 --- /dev/null +++ b/theories/ooCat/Sigma.v @@ -0,0 +1,31 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Import ooCat.Cat1. + +Generalizable Variables m n A B. + +(** * Sigma oo-categories of displayed oo-categories *) + +CoFixpoint isglob_sigma `{IsDGlob n A n B} + : IsGlob n (sig B). +Proof. + unshelve econstructor. + - intros [a u] [b v]; exact { f : a $-> b & DHom f u v }. + - intros [a u] [b v]; exact _. +Defined. + +Global Existing Instance isglob_sigma. + +CoFixpoint iscat0_sigma `{IsDCat0 n A n B} + : IsCat0 n (sig B). +Proof. + unshelve econstructor. + - intros [a u] [b v] [c w] [g q] [f p]. + exists (g $o f). + exact (q $oD p). + - intros [a u]. + exists (cat_id a). + exact (dcat_id u). + - intros [a u] [b v] [c w] [g q]. +Abort. diff --git a/theories/ooCat/Transformation.v b/theories/ooCat/Transformation.v new file mode 100644 index 00000000000..7f82d115fc0 --- /dev/null +++ b/theories/ooCat/Transformation.v @@ -0,0 +1,216 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Export ooCat.Cat1 ooCat.Laxity. + +Generalizable Variables m n p A B C. + +(** * Inserters and natural transformations *) + +(** ** Dependent inserters *) + +Definition GenDInserter (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} + (a : A) + := lHom (head ls) (F a) (G a). + +CoFixpoint isdglob_gendinserter (ls : Stream Laxity) + `{IsGlob m A} `{HasEquivs n B} + (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} + : IsDGlob n (GenDInserter ls F G). +Proof. + unshelve econstructor. + - intros a b f ta tb; revert f. + unfold GenDInserter in ta, tb. + destruct (head ls). + + exact (GenDInserter (tail ls) (cat_postcomp (F a) tb o fmap F) + (cat_precomp (G b) ta o fmap G)). + + exact (GenDInserter (tail ls) (cat_postcomp (F a) tb o fmap F) + (cat_precomp (G b) ta o fmap G)). + + exact (GenDInserter (tail ls) (cat_postcomp (G a) tb o fmap G) + (cat_precomp (F b) ta o fmap F)). + - intros a b ta tb; cbn. + unfold GenDInserter in ta, tb. + set (l := head ls) in *. + destruct l; + apply isdglob_gendinserter. +Defined. +Global Existing Instance isdglob_gendinserter. + +(** We can forget the invertibility of an iso-inserter. *) +Definition colax_pseudo_inserter + (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} (a : A) + : (GenDInserter (SCons pseudo ls) F G a) -> (GenDInserter (SCons colax ls) F G a) + := fun f => cate_fun f. + +Global Instance isdfunctor0_colax_pseudo_inserter + (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} + : IsDFunctor0 idmap (colax_pseudo_inserter ls F G). +Proof. + unshelve econstructor. + - cbn; intros a b u v f g. + exact g. + - cbn; intros a b u v. + apply isdfunctor0_idmap. +Defined. + +(** And we can turn around a lax inserter into a colax one. *) +Definition colax_lax_inserter + (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} (a : A) + : (GenDInserter (SCons lax ls) G F a) -> (GenDInserter (SCons colax ls) F G a) + := fun f => f. + +Global Instance isdfunctor0_colax_lax_inserter + (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} + : IsDFunctor0 idmap (colax_lax_inserter ls F G). +Proof. + unshelve econstructor. + - cbn; intros a b u v f g. + exact g. + - cbn; intros a b u v. + apply isdfunctor0_idmap. +Defined. + +(* +CoFixpoint iscat0_gendinserter (ls : Stream Laxity) + `{IsCat0 m A} `{IsCat1 n B} (F G : A -> B) + `{!IsFunctor0 F, !IsFunctor1 F, !IsFunctor0 G, !IsFunctor1 G} + : IsDCat0 n (GenDInserter ls F G). +Proof. + unshelve econstructor. + - intros a b c ta tb tc g f. + unfold GenDInserter in ta, tb, tc. + cbn; destruct (head ls); cbn; intros p q. + all: unfold GenDInserter in p, q. + all: unfold GenDInserter. + all: destruct (head (tail ls)); cbn in *. + all: unfold cat_precomp, cat_postcomp in *. + (** Should really be using a library for squares. *) + 1,4,7:refine (_ $o (_ $ _) $o _). + 1-3:refine ((cat_assoc _ _ _)^-1$ $o _). + 1-3:refine (_ $o (p $o> _)). + 1-3:refine ((_ $E _) $oE _). + 1-3:refine ((cat_assoc _ _ _)^-1$ $oE _). + 1-3:refine (_ $oE (p $o>E _)). + 1-3:refine ((_ $ _)). + all:refine (_ $o (cat_assoc _ _ _)). + all:refine ((_ $ _) $o _). + all:exact (cat_assoc _ _ _)^-1$. + - unfold GenDInserter; cbn; intros a ta. + destruct (head ls); cbn. + all: unfold GenDInserter. + all: destruct (head (tail ls)); cbn in *. + all: unfold cat_precomp, cat_postcomp in *. + 1,4,7:refine (_ $o (_ $ _) $o _). + 1-3:exact ((cat_idl _)^-1$ $o (cat_idr _)). + 1,3,5:refine (_ $oE (_ $E _) $oE _). + 1-3:exact ((cat_idl _)^-1$ $oE (cat_idr _)). + all:refine (_ $o (fmap_id _ _ $o> _)). + all:refine ((_ $ B) `{!IsFunctor0 F, !IsFunctor0 G} + := sig (GenDInserter l F G). + +Notation IsoInserter := (GenInserter all_pseudo). +Notation Inserter := (GenInserter one_colax). + +(** For instance, the category of prespectra (resp. spectra) should be the inserter (resp. isoinserter) of the identity functor of (nat -> pType) over a functor [shift o loops]. *) + + +(** ** Natural transformations *) + +(** A natural transformation [F $=> G] is a section of their displayed inserter. The freedom to choose laxities at all dimensions carries over, although we insist that a transformation always goes from [F] to [G] so that the inserter is colax at the bottom level. *) + +Definition Transformation {A} `{IsGlob n B} (F G : A -> B) + := forall a, F a $-> G a. +Notation "F $=> G" := (Transformation F G). + +Notation IsGenNatural1 l F G := + (@IsCatSect0 _ _ _ (GenDInserter (SCons colax l) F G) _ _). + +Definition isgennat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} + (alpha : F $=> G) {alnat : IsGenNatural1 ls F G alpha} + {x y : A} (f : x $-> y) + : lHom (head ls) (alpha y $o fmap F f) (fmap G f $o alpha x) + := fmapD (B := GenDInserter (SCons colax ls) F G) alpha f. + +Notation IsNatural1 F G := (IsGenNatural1 all_pseudo F G). + +Definition isnat `{IsGlob m A} `{HasEquivs n B} + {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} + (alpha : F $=> G) {alnat : IsNatural1 F G alpha} + {x y : A} (f : x $-> y) + : (alpha y $o fmap F f) $<~> (fmap G f $o alpha x) + := isgennat all_pseudo alpha f. + +Global Instance isgennat_iscolaxnat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} + (alpha : F $=> G) + {alnat : IsGenNatural1 (SCons colax ls) F G alpha} + (x y : A) + : IsGenNatural1 ls ((cat_postcomp (F x) (alpha y)) o (fmap' F x y)) + ((cat_precomp (G y) (alpha x)) o (fmap' G x y)) + (isgennat (SCons colax ls) alpha) + := iscatsect0_fmapD alpha alnat x y. + +Global Instance isgennat_ispseudonat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} + (alpha : F $=> G) + {alnat : IsGenNatural1 (SCons pseudo ls) F G alpha} + (x y : A) + : IsGenNatural1 ls ((cat_postcomp (F x) (alpha y)) o (fmap' F x y)) + ((cat_precomp (G y) (alpha x)) o (fmap' G x y)) + (fun f => cate_fun (isgennat (SCons pseudo ls) alpha f)). +Proof. + (** We have to nudge this from a section of the iso-inserter to a section of the inserter. *) + pose (iscatsect0_fmapD alpha alnat x y). + exact (iscatsect0_isdfunctor0_compose + (colax_pseudo_inserter ls ((cat_postcomp (F x) (alpha y)) o (fmap' F x y)) + ((cat_precomp (G y) (alpha x)) o (fmap' G x y))) + (@fmapD _ _ _ _ _ _ alpha alnat x y)). +Defined. + +Global Instance isgennat_islaxnat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} + {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} + (alpha : F $=> G) + {alnat : IsGenNatural1 (SCons lax ls) F G alpha} + (x y : A) + : IsGenNatural1 ls ((cat_precomp (G y) (alpha x)) o (fmap' G x y)) + ((cat_postcomp (F x) (alpha y)) o (fmap' F x y)) + (isgennat (SCons lax ls) alpha). +Proof. + (** Similarly here, we have to nudge from a section of the lax inserter in one direction to a section of the colax inserter in the other direction. *) + pose (iscatsect0_fmapD alpha alnat x y). + exact (iscatsect0_isdfunctor0_compose + (colax_lax_inserter ls ((cat_precomp (G y) (alpha x)) o (fmap' G x y)) + ((cat_postcomp (F x) (alpha y)) o (fmap' F x y))) + (@fmapD _ _ _ _ _ _ alpha alnat x y)). +Defined. + +(** If we generalized comma categories (and hence inserters) to act on category-sections rather than just functors, we could in principle iterate this approach to define modifications and higher transfors, analogously to how we iterate [isglob_forall] to define all the higher structure of [Type] and similarly for [pType]. Such a generalization seems to require either that the displayed category is an isofibration, or that we define a more general notion of inserter over a given natural transformation, and either one seems to require 2-coherent categories. In fact, since the level of coherence seems to go down by one each time we apply a comma construction, we probably wouldn't be able to use this to define a whole oo-category of oo-categories at any fixed coherence level. *) diff --git a/theories/ooCat/Type.v b/theories/ooCat/Type.v new file mode 100644 index 00000000000..5e24c303135 --- /dev/null +++ b/theories/ooCat/Type.v @@ -0,0 +1,33 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Import ooCat.Cat1 ooCat.Paths ooCat.Forall. + +(** * The oo-category of types *) + +(** The universe is a globular type with functions, homotopies, and higher homotopies. We obtain this by putting together path-groupoids with forall-categories. *) + +(** The universe is a globular type *) +Global Instance isglob_type : IsGlob 1 Type + := Build_IsGlob + 1 Type (fun A B => A -> B) + (fun A B => isglob_forall (const B) (fun _ => isglob_withpaths B)). + +(** The universe is a 0-coherent (oo,1)-category. *) +Global Instance iscat0_type : IsCat0 1 Type. +Proof. + unshelve econstructor. + - intros A B C g f; exact (g o f). + - intros A; exact idmap. + - intros A B C g; cbn. + apply isfunctor0_postcompose. + intros; apply isfunctor0_withpaths. + - intros A B C f; cbn. + rapply isfunctor0_precompose. + - intros []. + - intros A B. + rapply iscat0_forall. + intros; rapply iscat0_withpaths. +Defined. + +Global Existing Instances iscat0_type. diff --git a/theories/ooCat/Unit.v b/theories/ooCat/Unit.v new file mode 100644 index 00000000000..c4257fc329b --- /dev/null +++ b/theories/ooCat/Unit.v @@ -0,0 +1,26 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Export ooCat.Cat1. + +(** * The unit category *) + +CoFixpoint isglob_unit : IsGlob 0 Unit + := Build_IsGlob 0 Unit (fun _ _ => Unit) (fun _ _ => isglob_unit). + +Global Existing Instance isglob_unit. + +CoFixpoint iscat0_unit : IsCat0 0 Unit. +Proof. + snrapply Build_IsCat0. + 1,2,5: intros; exact tt. + (** We cannot use isfunctor0_const since that requires IsCat0 *) + 1,2: + intros ? ? ? ?; cofix e; + simple notypeclasses refine (Build_IsFunctor0 _ _ _); + intros ? ?; [ intro; exact tt | exact e ]. + intros a b. + apply iscat0_unit. +Defined. + +Global Existing Instance iscat0_unit. From 7dd93ded0fe826499716cb4266e7da9c4af45be2 Mon Sep 17 00:00:00 2001 From: Mike Shulman Date: Fri, 13 Mar 2020 13:10:53 -0700 Subject: [PATCH 2/4] Update theories/Basics/Overture.v Co-Authored-By: Jason Gross --- theories/Basics/Overture.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 9499cc82202..ee5567769f7 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -711,7 +711,7 @@ Hint Resolve tt : core. (** 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. *) -Fixpoint pred (n : nat) : nat +Definition pred (n : nat) : nat := match n with | 0 => 0 | S n => n From 88bb771482ae30066fd902764ad1bb7a1ffa8121 Mon Sep 17 00:00:00 2001 From: Michael Shulman Date: Fri, 13 Mar 2020 13:27:04 -0700 Subject: [PATCH 3/4] rename SCons to scons --- theories/Basics/Overture.v | 6 +++--- theories/ooCat/Laxity.v | 6 +++--- theories/ooCat/Transformation.v | 20 ++++++++++---------- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index ee5567769f7..58343aea723 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -741,18 +741,18 @@ Bind Scope bool_scope with Bool. (** ** Coinductive streams *) -CoInductive Stream (A : Type) := SCons +CoInductive Stream (A : Type) := scons { head : A ; tail : Stream A }. -Arguments SCons {A} _ _. +Arguments scons {A} _ _. Arguments head {A} _. Arguments tail {A} _. CoFixpoint const_stream {A} (a : A) : Stream A - := SCons a (const_stream a). + := scons a (const_stream a). (** *** Typeclasses for case analysis *) diff --git a/theories/ooCat/Laxity.v b/theories/ooCat/Laxity.v index ae8784db498..1c201d8a9d3 100644 --- a/theories/ooCat/Laxity.v +++ b/theories/ooCat/Laxity.v @@ -16,9 +16,9 @@ Inductive Laxity := Notation oplax := colax (only parsing). -CoFixpoint all_pseudo : Stream Laxity := SCons pseudo all_pseudo. -Definition one_lax : Stream Laxity := SCons lax all_pseudo. -Definition one_colax : Stream Laxity := SCons colax all_pseudo. +CoFixpoint all_pseudo : Stream Laxity := scons pseudo all_pseudo. +Definition one_lax : Stream Laxity := scons lax all_pseudo. +Definition one_colax : Stream Laxity := scons colax all_pseudo. (** It may seem backwards for [colax] to mean a morphism "forwards" and [lax] a morphism "backwards", but that's what matches the standard terminology for natural transformations. *) Definition lHom (l : Laxity) `{HasEquivs n A} (a b : A) := diff --git a/theories/ooCat/Transformation.v b/theories/ooCat/Transformation.v index 7f82d115fc0..eb290c3cec6 100644 --- a/theories/ooCat/Transformation.v +++ b/theories/ooCat/Transformation.v @@ -41,7 +41,7 @@ Global Existing Instance isdglob_gendinserter. Definition colax_pseudo_inserter (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} (a : A) - : (GenDInserter (SCons pseudo ls) F G a) -> (GenDInserter (SCons colax ls) F G a) + : (GenDInserter (scons pseudo ls) F G a) -> (GenDInserter (scons colax ls) F G a) := fun f => cate_fun f. Global Instance isdfunctor0_colax_pseudo_inserter @@ -60,7 +60,7 @@ Defined. Definition colax_lax_inserter (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} (F G : A -> B) `{!IsFunctor0 F, !IsFunctor0 G} (a : A) - : (GenDInserter (SCons lax ls) G F a) -> (GenDInserter (SCons colax ls) F G a) + : (GenDInserter (scons lax ls) G F a) -> (GenDInserter (scons colax ls) F G a) := fun f => f. Global Instance isdfunctor0_colax_lax_inserter @@ -151,14 +151,14 @@ Definition Transformation {A} `{IsGlob n B} (F G : A -> B) Notation "F $=> G" := (Transformation F G). Notation IsGenNatural1 l F G := - (@IsCatSect0 _ _ _ (GenDInserter (SCons colax l) F G) _ _). + (@IsCatSect0 _ _ _ (GenDInserter (scons colax l) F G) _ _). Definition isgennat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} (alpha : F $=> G) {alnat : IsGenNatural1 ls F G alpha} {x y : A} (f : x $-> y) : lHom (head ls) (alpha y $o fmap F f) (fmap G f $o alpha x) - := fmapD (B := GenDInserter (SCons colax ls) F G) alpha f. + := fmapD (B := GenDInserter (scons colax ls) F G) alpha f. Notation IsNatural1 F G := (IsGenNatural1 all_pseudo F G). @@ -172,21 +172,21 @@ Definition isnat `{IsGlob m A} `{HasEquivs n B} Global Instance isgennat_iscolaxnat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} (alpha : F $=> G) - {alnat : IsGenNatural1 (SCons colax ls) F G alpha} + {alnat : IsGenNatural1 (scons colax ls) F G alpha} (x y : A) : IsGenNatural1 ls ((cat_postcomp (F x) (alpha y)) o (fmap' F x y)) ((cat_precomp (G y) (alpha x)) o (fmap' G x y)) - (isgennat (SCons colax ls) alpha) + (isgennat (scons colax ls) alpha) := iscatsect0_fmapD alpha alnat x y. Global Instance isgennat_ispseudonat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} (alpha : F $=> G) - {alnat : IsGenNatural1 (SCons pseudo ls) F G alpha} + {alnat : IsGenNatural1 (scons pseudo ls) F G alpha} (x y : A) : IsGenNatural1 ls ((cat_postcomp (F x) (alpha y)) o (fmap' F x y)) ((cat_precomp (G y) (alpha x)) o (fmap' G x y)) - (fun f => cate_fun (isgennat (SCons pseudo ls) alpha f)). + (fun f => cate_fun (isgennat (scons pseudo ls) alpha f)). Proof. (** We have to nudge this from a section of the iso-inserter to a section of the inserter. *) pose (iscatsect0_fmapD alpha alnat x y). @@ -199,11 +199,11 @@ Defined. Global Instance isgennat_islaxnat (ls : Stream Laxity) `{IsGlob m A} `{HasEquivs n B} {F : A -> B} `{!IsFunctor0 F} {G : A -> B} `{!IsFunctor0 G} (alpha : F $=> G) - {alnat : IsGenNatural1 (SCons lax ls) F G alpha} + {alnat : IsGenNatural1 (scons lax ls) F G alpha} (x y : A) : IsGenNatural1 ls ((cat_precomp (G y) (alpha x)) o (fmap' G x y)) ((cat_postcomp (F x) (alpha y)) o (fmap' F x y)) - (isgennat (SCons lax ls) alpha). + (isgennat (scons lax ls) alpha). Proof. (** Similarly here, we have to nudge from a section of the lax inserter in one direction to a section of the colax inserter in the other direction. *) pose (iscatsect0_fmapD alpha alnat x y). From e2686d25b817062e590e7d4dc3472a31fcc6512d Mon Sep 17 00:00:00 2001 From: Mike Shulman Date: Fri, 13 Mar 2020 22:37:25 -0700 Subject: [PATCH 4/4] Working on pType as an (oo,1)-category --- _CoqProject | 1 + theories/Basics/PathGroupoids.v | 40 ++++++++ theories/ooCat/Forall.v | 85 ++++++++++++++++- theories/ooCat/Sigma.v | 2 + theories/ooCat/pType.v | 164 ++++++++++++++++++++++++++++++++ 5 files changed, 288 insertions(+), 4 deletions(-) create mode 100644 theories/ooCat/pType.v diff --git a/_CoqProject b/_CoqProject index 7f1e243512b..2ce29720ad4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -83,6 +83,7 @@ theories/ooCat/Paths.v theories/ooCat/Sigma.v theories/ooCat/Forall.v theories/ooCat/Type.v +theories/ooCat/pType.v diff --git a/theories/Basics/PathGroupoids.v b/theories/Basics/PathGroupoids.v index ab601984e07..95a9d034795 100644 --- a/theories/Basics/PathGroupoids.v +++ b/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. *) diff --git a/theories/ooCat/Forall.v b/theories/ooCat/Forall.v index a8de4d9f1a9..01d8ef3bb9c 100644 --- a/theories/ooCat/Forall.v +++ b/theories/ooCat/Forall.v @@ -3,10 +3,14 @@ Require Import Basics. Require Import ooCat.Cat1. -(** * Forall oo-groupoids (with plain types as base) *) +Generalizable Variables m n p A B C. + +(** * Forall (oo,n)-categories (with plain types as base) *) + +(** ** Forall (oo,n)-categories *) (** [forall] preserves globular types. *) -CoFixpoint isglob_forall {n A} (B : A -> Type) `(forall a, IsGlob n (B a)) +CoFixpoint isglob_forall `(B : A -> Type) `(forall a, IsGlob n (B a)) : IsGlob n (forall a, B a). Proof. exists (fun f g => forall a, f a $-> g a); intros. @@ -58,7 +62,7 @@ Global Existing Instance iscat0_forall. (** A pointwise quasi-isomorphism in a [forall] is a quasi-isomorphism. *) CoFixpoint isqiso_forall {n A} (B : A -> Type) {bg : forall a, IsGlob n (B a)} {bc : forall a, IsCat0 n (B a)} - (f g : forall a, B a) + {f g : forall a, B a} (p : f $-> g) `{forall a, IsQIso (p a)} : IsQIso p. Proof. @@ -73,7 +77,7 @@ Defined. (** And conversely. *) CoFixpoint isqiso_from_forall {n A} (B : A -> Type) {bg : forall a, IsGlob n (B a)} {bc : forall a, IsCat0 n (B a)} - (f g : forall a, B a) + {f g : forall a, B a} (p : f $-> g) `{!IsQIso p} (a : A) : IsQIso (p a). Proof. @@ -104,3 +108,76 @@ Defined. Global Existing Instance hasequivs_forall. (** TODO: 1-coherent functors and categories *) + +(** ** Displayed forall (oo,n)-categories *) + +(** Dependent [forall] preserves globular types. *) +CoFixpoint isdglob_forall + {A : Type} (B : A -> Type) (C : forall a, B a -> Type) + `(forall a, IsGlob m (B a)) `(forall a, IsDGlob n (C a)) + : IsDGlob n (fun (f:forall a, B a) => forall a, C a (f a)). +Proof. + unshelve econstructor. + - intros f g p u v. + exact (forall a:A, DHom (p a) (u a) (v a)). + - intros f g u v. + rapply isdglob_forall. +Defined. + +Global Existing Instance isdglob_forall. + +(** Postcomposing and precomposing between dependent [forall] types preserves displayed 0-coherent oo-functors. *) +CoFixpoint isdfunctor0_postcompose {m n mm nn A} (B C : A -> Type) + `{forall a, IsGlob m (B a)} `{forall a, IsGlob n (C a)} + (BB : forall a, B a -> Type) (CC : forall a, C a -> Type) + `{!forall a, IsDGlob mm (BB a)} `{!forall a, IsDGlob nn (CC a)} + (F : forall a, B a -> C a) {Ff : forall a, IsFunctor0 (F a)} + (FF : forall a b, BB a b -> CC a (F a b)) + {FFf : forall a, IsDFunctor0 (F a) (FF a)} + : IsDFunctor0 (fun (f:forall a:A, B a) => (fun a:A => F a (f a))) + (fun (f:forall a:A, B a) (g:forall a, BB a (f a)) + => (fun a:A => FF a (f a) (g a))). +Proof. + unshelve econstructor. + - cbn; intros f g u v p q a. + exact (dfmap (F a) (FF a) (q a)). + - intros; rapply isdfunctor0_postcompose. +Defined. + +CoFixpoint isdfunctor0_precompose {m n A B} + (h : A -> B) + (C : B -> Type) `{forall a, IsGlob m (C a)} + (D : forall b:B, C b -> Type) `{forall a, IsDGlob n (D a)} + : IsDFunctor0 (fun (f:forall b:B, C b) => (fun a => f (h a))) + (fun (f:forall b:B, C b) (g:forall b, D b (f b)) + => (fun a:A => g (h a))). +Proof. + unshelve econstructor. + - cbn; intros f g u v p q a. + exact (q (h a)). + - intros; rapply isdfunctor0_precompose. +Defined. + +Global Existing Instances isdfunctor0_postcompose isdfunctor0_precompose. + +(** Dependent [forall] preserves 0-coherent displayed oo-categories. *) +CoFixpoint isdcat0_forall + {A : Type} (B : A -> Type) (C : forall a, B a -> Type) + `(forall a, IsGlob m (B a)) `(forall a, IsCat0 m (B a)) + `(forall a, IsDGlob n (C a)) `(forall a, IsDCat0 n (C a)) + : IsDCat0 n (fun (f:forall a, B a) => forall a, C a (f a)). +Proof. + unshelve econstructor; cbn. + - intros f g h u v w q p s r a. + exact (s a $oD r a). + - intros f u a. + exact (dcat_id (u a)). + - intros; rapply isdfunctor0_postcompose. + - intros; rapply isdfunctor0_postcompose. + - intros ? f g u v p pe r a. + pose (isqiso_from_forall B p a). + exact (dgpd_inv (r a)). + - intros; rapply isdcat0_forall. +Defined. + +Global Existing Instance isdcat0_forall. diff --git a/theories/ooCat/Sigma.v b/theories/ooCat/Sigma.v index 657a2671c39..8c61abdbe3c 100644 --- a/theories/ooCat/Sigma.v +++ b/theories/ooCat/Sigma.v @@ -29,3 +29,5 @@ Proof. exact (dcat_id u). - intros [a u] [b v] [c w] [g q]. Abort. + +(* Global Existing Instance iscat0_sigma. *) diff --git a/theories/ooCat/pType.v b/theories/ooCat/pType.v new file mode 100644 index 00000000000..36fc90893cb --- /dev/null +++ b/theories/ooCat/pType.v @@ -0,0 +1,164 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import Basics. +Require Import ooCat.Cat1 ooCat.Paths ooCat.Forall ooCat.Sigma ooCat.Type. + +Generalizable Variables m n p A B C. + +(** ** Pointed families over pointed types *) + +Class IsDPointed {A : Type} `{IsPointed A} (B : A -> Type) + := dpoint : B (point A). + +Global Instance isdpointed_const `{IsPointed A, IsPointed B} + : IsDPointed (@const A Type B) + := point B. + +Arguments dpoint {A _} B {_}. + +(** ** pType *) + +(** Let's define [pType] as a sigma here, since then we can apply the general theorems about sigmas of displayed categories. *) + +Definition pType := sig IsPointed. + + +(** ** [pType] is displayed globular over [Type] *) + +CoFixpoint isdglob_pforall `{IsDPointed A B} + (Bg := fun a => isglob_withpaths (B a)) + : IsDGlob 0 (fun (f : forall a:A, B a) => f (point A) = dpoint B). +Proof. + unshelve econstructor. + - intros f g p fp gp. + exact (p (point A) = fp @ gp^). + - intros f g fp gp; cbn. + rapply isdglob_pforall. +Defined. + +Global Existing Instance isdglob_pforall. + +Global Instance isdglob_ispointed + : IsDGlob 1 IsPointed. +Proof. + unshelve econstructor. + - intros X Y f ? ?. + exact (f (point X) = point Y). + - intros X Y ? ?. cbn. + exact (@isdglob_pforall _ _ (@const X Type Y) _). +Defined. + +Global Instance isglob_ptype : IsGlob 1 pType. +Proof. + unfold pType. + (** What's up with the universes? *) + Fail exact (@isglob_sigma 1 Type IsPointed _ _). +Abort. + + +(** ** [pType] is a displayed 0-coherent category over [Type] *) + +CoFixpoint isdfunctor0_postcomp_pforall + `{IsDPointed A B} {C : A -> Type} `{!IsDPointed C} + (F : forall a, B a -> C a) (Fp : F (point A) (dpoint B) = dpoint C) + (** We expand [ap (F (point A)) p @ Fp] into a singleton here because it makes the applications easier. *) + (G : forall (f : forall a:A, B a) (p : f (point A) = dpoint B), + F (point A) (f (point A)) = dpoint C) + (Gp : forall (f : forall a:A, B a) (p : f (point A) = dpoint B), + G f p = ap (F (point A)) p @ Fp) + (Bg := fun a => isglob_withpaths (B a)) + (Cg := fun a => isglob_withpaths (C a)) + (Fg := fun a => isfunctor0_withpaths (F a)) + : IsDFunctor0 (fun (f : forall a:A, B a) => fun a => F a (f a)) + (fun (f : forall a:A, B a) (p : f (point A) = dpoint B) => G f p). +Proof. + unshelve econstructor. + - cbn; intros f g fp gp p u. + refine (ap (ap (F (point A))) u @ _). + refine (_ @ ((Gp f fp)^ @@ (inverse2 (Gp g gp)^))). + refine (ap_pp _ _ _ @ _ @ (idpath @@ (inv_pp _ _)^)). + refine (_ @ concat_p_pp _ _ _). + refine (idpath @@ _). + refine (ap_V _ _ @ _). + symmetry; apply concat_p_Vp. + - intros f g fp gp. + rapply isdfunctor0_postcomp_pforall. + intros; reflexivity. +Defined. + +(* +CoFixpoint isdfunctor0_precomp_pforall + `{IsDPointed A B} `{!IsPointed C} (h : C -> A) (hp : h (point C) = point A) + (Bg := fun a => isglob_withpaths (B a)) + (Bhp := hp^ # (dpoint B) : IsDPointed (B o h)) + (Bhg := @isdglob_pforall C _ (B o h) _) + : IsDFunctor0 (fun (g : forall a:A, B a) => fun c => g (h c)) + (fun (g : forall a:A, B a) (p : g (point A) = dpoint B) + => moveL_transport_V B hp (g (h (point C))) (dpoint B) (apD g hp @ p)). +Proof. + unshelve econstructor. + - cbn; intros g1 g2 gp1 gp2 p pp. +*) + +CoFixpoint isdcat0_pforall `{IsDPointed A B} + (Bg := fun a => isglob_withpaths (B a)) + (Bc0 := fun a => iscat0_withpaths (B a)) + : IsDCat0 0 (fun (f : forall a:A, B a) => f (point A) = dpoint B). +Proof. + unshelve econstructor; cbn in *. + - intros f g h fp gp hp q p r s. + refine ((whiskerR s _ @ whiskerL _ r) @ _). + refine (concat_pp_p _ _ _ @ _). + refine (idpath @@ _). + apply concat_V_pp. + - intros f fp. + symmetry; apply concat_pV. + - intros f g h fp gp hp q qp; cbn. + refine (@isdfunctor0_postcomp_pforall + A _ (fun a => f a = g a) (fp @ gp^) (fun a => f a = h a) + _ (fun (a:A) (t:f a = g a) => t @ q a) _ _ _). + intros k kp; cbn. + refine (concat_pp_p _ _ _ @ whiskerR _ _). + symmetry; apply ap_concat_r. + - intros f g h fp gp hp p pp; cbn. + refine (@isdfunctor0_postcomp_pforall + A _ (fun a => g a = h a) (gp @ hp^) (fun a => f a = h a) + _ (fun (a:A) (t:g a = h a) => p a @ t) _ _ _). + intros k kp; cbn. + refine (((concat_whisker _ _ _ _ _ _) @@ idpath) @ _). + refine (concat_pp_p _ _ _ @ whiskerR _ _). + symmetry; apply ap_concat_l. + - intros _ f g fp gp p pe pp. + apply (cancelR _ _ (p (point A))). + pose (isqiso_from_forall _ p (point A)). + refine (qiso_isretr (p (point A)) @ _). + refine (_ @ (idpath @@ pp^)). + refine (_ @ concat_pp_p _ _ _). + refine (_ @ ((concat_pV_p _ _)^ @@ idpath)). + symmetry; cbn; apply concat_pV. + - intros f g fp gp; cbn. + rapply isdcat0_pforall. +Defined. + +Global Existing Instance isdcat0_pforall. + +Global Instance isdcat0_ispointed + : IsDCat0 1 IsPointed. +Proof. + unshelve econstructor. + - cbn; intros X Y Z ? ? ? g f gp fp. + exact (ap g fp @ gp). + - cbn; intros X ?; reflexivity. + - cbn; intros X Y Z ? ? ? g gp. + rapply isdfunctor0_postcomp_pforall; cbn. + intros; reflexivity. + - cbn; intros X Y Z ? ? ? f fp. + admit. (** I think this requires some precomposition lemma *) + - intros []. + - intros X Y ? ?; cbn. + exact (@isdcat0_pforall X _ (@const X Type Y) _). +Admitted. + +(* +Global Instance iscat0_ptype : IsCat0 1 pType. + *)