Instantly share code, notes, and snippets.

# jcmckeown/CoherentCategoriesModulo.v Last active Aug 29, 2015

Trying to get at a definition of Categories internal to coq/HoTT, with all the compositions and their equations and Nothing Else; the gist of this gist is: do not assume equations before you need them, and prove them if possible! Third revision: added some comments, removed some NOP proof lines. Maybe some other tweaks?
 Require Import HoTT. Open Scope path_scope. Open Scope type_scope. Section Categories. (** Everyone knows a category has an underlying graph, so we should mention them *) Definition Graph := { two_obs : Type & two_obs -> two_obs -> Type }. (** And the heart of what makes a category is a unital associative compositions of chainable arrows *) Record PreCat (T : Graph) := { COb := T .1 ; CAr := T .2 ; CId : forall (t : COb ), (CAr t t); CComp : forall a b c : COb, (CAr a b) -> (CAr b c) -> (CAr a c); CCompLeftId : forall ( a b : COb ) (f : CAr a b), CComp _ _ _ (CId a) f = f }. (** so, why only CompLeftId? Ahah! Don't ask for too many equations! *) Global Arguments COb { T } _ . Global Arguments CAr { T } _ _ _. Local Arguments CId { T } { _ } _. Local Arguments CComp { T } { _ } { _ _ _ } _ _. (** of course we want a category with objects the arrows of Our Category. *) Record Arrow {T : Graph} (P : PreCat T) := { ASrc : COb P; ATrg : COb P; AAr : CAr P ASrc ATrg }. Notation theArr f := (Build_Arrow _ _ _ _ f). Local Arguments ASrc { T } { P } _. Local Arguments ATrg { T } { P } _. Local Arguments AAr { T } { P } _. (** There are several candidates for a morphism between arrows; another one is a factoring of one through the other ( f = a . g . b ), but that is not Our Category, today. *) Record Sqr {T : Graph} { P : PreCat T } (f g : Arrow P) := { SSrc : CAr P (ASrc f) (ASrc g); STrg : CAr P (ATrg f) (ATrg g); SAr : CComp (AAr f) STrg = CComp SSrc (AAr g) }. Definition graphOfArrows { T : Graph } (P : PreCat T) : Graph := ( Arrow P ; @Sqr T P ). (** I don't know why I settled on this being Notation rather than Definition; probably because I didn't want Too Many Types floating around; have the "pre-processor" do computations for us, if it can. *) Notation compn obs ars := (forall (a b c : obs), (ars a b) -> (ars b c) -> (ars a c)) (only parsing). (** it occurs to me that I haven't got a good convention for distinguishing names of types-as-desiderata vs. types-as-lemmata. Maybe, at least, I should call the things we ask for [Definition]s, and the impressive feats [Lemma]ta. We Say a composition of [Sqr]s "respects composition", and "respects identity" if the top and bottom edges are what we think they should be. Put another way: a [compn Arrow Sqr] is noteworthy if its top and bottom edge maps from graphOfArrows to the underlying Graph is, so far as we can yet express it, a "functor". *) Definition SqCompRespects { T : Graph} { P : PreCat T } ( cc : compn (Arrow P) (@Sqr T P)) := forall (a b c : Arrow P), forall (s : Sqr a b) (t : Sqr b c), ( (SSrc _ _ (cc _ _ _ s t)) = (CComp (SSrc _ _ s) (SSrc _ _ t)) ) * ( (STrg _ _ (cc _ _ _ s t)) = (CComp (STrg _ _ s) (STrg _ _ t)) ). Definition IdRespects { T : Graph } { P : PreCat T } ( i : forall a : Arrow P, Sqr a a ) := forall ( a : Arrow P ), (( SSrc _ _ (i a)) = (CId (ASrc a)) ) * ((STrg _ _ (i a)) = (CId (ATrg a))). (** In words, a type family over precats is "Helpful" if one instance of it on one precats tells us both how to compose squares and how to find an instance of it over the derived PreCat of squares. *) Definition HelpfulType ( r : forall T, PreCat T -> Type ) := forall T, forall P : PreCat T, forall w : r T P, { PC : PreCat (graphOfArrows P) & (SqCompRespects (@CComp _ PC)) * (IdRespects (@CId _ PC)) * r _ PC }. (** which means, in particular, we can construct ... these things. Categories of n-cubes *) Lemma helpedCubes ( r : forall T, PreCat T -> Type ) (H : HelpfulType r) (T : Graph) (P : PreCat T) (w : r T P) (n : nat) : { Tn : Graph & { Pn : PreCat Tn & r Tn Pn } }. Proof. induction n. exists T. exists P. auto. destruct IHn as [ Tpn [ Ppn wpn ]]. exists (graphOfArrows Ppn). assert (helper := H Tpn Ppn wpn ). destruct helper. exists x. apply p. Defined. (** this will be useful when we get to proving that composable equations are really handy *) Definition CrossId { T : Graph} { P : PreCat T } { a b c : COb P } (f : CAr P a b)( g : CAr P b c ): Sqr (theArr f) (theArr g) := Build_Sqr _ _ (theArr f) (theArr g) f g idpath. Section IfAHelper. Hypotheses (r : forall T, PreCat T -> Type) (VH : HelpfulType r). (** We didn't ask PreCat to provide associativity; so it happens that if we can compose equations of composites, we get associativity for free *) Lemma CompAssoc { T : Graph } (P : PreCat T)( w : r T P ) : forall ( a b c d : COb P ) (f : CAr P a b ) (g : CAr P b c )( h : CAr P c d), CComp f (CComp g h) = CComp (CComp f g) h. Proof. intros. assert (helper := (VH T P w)). destruct helper as [ pc [ [ goodcomp _ ] _ ] ]. set ( lc := CrossId f g ). set ( rc := CrossId g h ). set ( v := @CComp _ pc _ _ _ lc rc ). set ( gc := goodcomp _ _ _ lc rc ). destruct gc as [ gcs gct ]. simpl in *. path_via (CComp f (STrg _ _ v) ). apply ap. refine ( _ ^ ). auto. path_via (CComp (SSrc _ _ v) h). exact ( SAr _ _ v ). refine ( ap (fun x => CComp x h) _ ). auto. Defined. (** Similarly, having an "identity square" that *respects* identity at the ends, trivially then id is a central transformation; being also neutral at one end means it must be neutral at the other. *) Lemma CompRightId { T : Graph } (P : PreCat T)( w : r T P ) : forall ( a b : COb P ) (f : CAr P a b), CComp f (CId b) = f. Proof. assert (helper := (VH T P w)). destruct helper as [ pc [ [ goodcomp goodid ] _ ] ]. intros. path_via (CComp (CId a) f). set (arf := theArr f). set (theSquare := (@CId _ pc arf)) in *. refine ( _ @ SAr _ _ theSquare @ _ ); simpl. apply ap. refine ( _ ^ ). unfold theSquare. exact (snd (goodid arf)). apply (ap (fun x => CComp x f)). exact (fst (goodid arf)). apply CCompLeftId. Defined. End IfAHelper. (** When I started, I wasn't sure I could even write this. But coq thinks it's a perfectly acceptable definition. It must be nested-postive anyways. *) Inductive minhelper : forall (T : Graph) (P : PreCat T), Type := CoherentAnd (T : Graph) (P : PreCat T) : forall (PC : PreCat (graphOfArrows P)), SqCompRespects (@CComp _ PC) -> IdRespects (@CId _ PC) -> minhelper (graphOfArrows P) (PC) -> minhelper T P. (** The obvious conclusion *) Lemma minhelperIsHelper : HelpfulType minhelper. Proof. intros T P w. destruct w. exists PC. auto. Defined. (** But we've a vague suspicion that the (really genuinely categories!) ( U & E : U -> Type ) with arrows Ar u v = ( E u -> E v ) are Hard To Proveide a [minhelper T]. So, here's something we're sure we can prove all of. Even if it gets icky. *) Inductive filteredMinHelper : forall (T : Graph) (P : PreCat T), nat -> Type := | cohereHelpsSome ( T : _ ) ( P : PreCat T ) (PC : PreCat (graphOfArrows P)) ( scr : SqCompRespects (@CComp _ PC)) ( sir : IdRespects (@CId _ PC)) : filteredMinHelper T P 0 | graphHelpOneMore ( T : _ ) (P : PreCat T) (n : nat) : forall PC : PreCat (graphOfArrows P), SqCompRespects (@CComp _ PC) -> IdRespects (@CId _ PC) -> filteredMinHelper (graphOfArrows P) PC n -> filteredMinHelper T P (S n). Record Category : Type := { UGraph : Graph; UPre : PreCat UGraph; Coherence : minhelper UGraph UPre }. Record LayerwiseCat : Type := { UGraph_f : Graph ; UPre_f : PreCat UGraph_f; Cohere_f : forall n, filteredMinHelper UGraph_f UPre_f n }. (** the different layers *might* change the compositions in the upper layers, which means they *might* change the underlying types of higher layers (because they're defined by equations) but I don't think there's *much* scope for these changes *) End Categories. Close Scope path_scope. Close Scope type_scope.
Owner Author

### jcmckeown commented May 21, 2014

 @JasonGross, I don't know what you'll think of it, but I was pleased to have come up with it.