fact: Record Metacategory := { arrow := N; pairs : M.t arrow; composite (f g h : arrow) := M.find (f, g) pairs = Some h; defined (f g : arrow) := ∃ h, composite f g h; composite_defined {f g h : arrow} (H : composite f g h) : defined f g := (h; H); composite_correct {f g h fg gh : arrow} : composite f g fg -> composite g h gh → ∃ fgh, composite fg h fgh; composition_law {f g h fg gh : arrow} : composite f g fg -> composite g h gh -> ∀ fgh, composite fg h fgh ↔ composite f gh fgh; is_identity (u : arrow) := (∀ f, defined f u → composite f u f) ∧ (∀ g, defined u g → composite u g g); identity_law (x y f : arrow) : composite x y f -> ∃ u u', is_identity u → is_identity u' -> composite f u f ∧ composite u' f f }.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor