fact: Definition from_1 `{Funext} c : Pseudofunctor 1 := Eval simpl in from_terminal c.
imports: Category.Core Functor.Core Functor.Identity Pseudofunctor.Core InitialTerminalCategory.Core FunctorCategory.Morphisms NaturalTransformation.Paths NatCategory PathGroupoids