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?

CoherentCategoriesModulo.v

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.

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