proposition: Lemma law : @functor _ one _ C o inverse C = 1 /\ inverse C o @functor _ one _ C = 1.
proof: Proof. split; path_functor. exists (path_forall _ _ helper). unfold helper. exp_laws_t. Qed.
imports: Category.Core Functor.Core Functor.Identity Functor.Paths ExponentialLaws.Law1.Functors Functor.Composition.Core InitialTerminalCategory.Core Basics.Trunc ExponentialLaws.Tactics Basics.Tactics