(c : Functor 1 C) : Functors.from_terminal C (c (center _)) = c. Proof. path_functor. exists (path_forall _ _ (fun x => ap (object_of c) (contr _))). abstract ( exp_laws_t; simpl; rewrite <- identity_of; f_ap; symmetry; apply contr ). Defined.
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.