law' : functor' o inverse' = 1 /\ inverse' o functor' = 1 := center _.
Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Identity. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors InitialTerminalCategory.NaturalTransformations. Require Import HoTT.Basics HoTT.Types.