proposition: Lemma law1' : functor' o inverse' = 1 /\ inverse' o functor' = 1.
proof: Proof. unfold functor', inverse'. t_prod. Qed.
imports: HoTT.Basics HoTT.Types Category.Core Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Prod Functor.Prod Functor.Composition.Core Functor.Identity Functor.Composition.Laws