Augmented Category

An Augmented Category is what you get when you pass from category theory ala Simplicial sets to category theory ala Augmented Simplicial Sets.

This definition seems to work particularly nice in Displayed Type Theory, especially in the presence of symmetries; we can get duality by just using sym!

` The data of an augmented 1-category. If `sym` computed through the Martin-Lof identity type then
` laws would be easy.
def ACat : Type :=
  sig
    ( Ix : Type
    , Ob : Type⁽ᵈ⁾ Ix
    , Hom : Type⁽ᵈᵈ⁾ Ix Ob Ob
    , id : (i : Ix) (x : Ob i) → Hom i x x
    , comp : (i : Ix) (x y z : Ob i) → Hom i y z → Hom i x y → Hom i x z
    )

` Taking opposites is as easy as applying symmetry when we can.
def ACat.op (C : ACat) : ACat :=
  ( Ix := C .Ix
  , Ob := C .Ob
  , Hom := sym (C .Hom)
  , id := i x ↦ sym (C .id i x)
  , comp := i x y z f g ↦ sym (C .comp i z y x (sym g) (sym f))
  )