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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This comment has been minimized.
@JasonGross, I don't know what you'll think of it, but I was pleased to have come up with it.