fact: Definition from_0 `{Funext} : Pseudofunctor 0 := Eval simpl in from_initial.
imports: Category.Core Functor.Core Functor.Identity Pseudofunctor.Core InitialTerminalCategory.Core FunctorCategory.Morphisms NaturalTransformation.Paths NatCategory PathGroupoids