fact: Fixpoint denote `(o : Obj) : ∀ {C : Category} {A : @Cartesian C} `{@Closed C A} `{@Cocartesian C} `{@Terminal C} `{@Initial C}, C := fun _ _ _ _ _ _ => match o with | One_ => 1 | Prod_ x y => denote x × denote y | Exp_ x y => denote y ^ denote x | Zero_ => 0 | Coprod_ x y => denote x + denote y end.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Structure.Cocartesian Category.Instance.Sets