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