proposition: Lemma roundtrip1_ob_as_equality (sig : Signature C D D') : signature_from_strong_functor (ab_strong_functor_from_signature sig) = sig.
proof: Proof. use total2_paths_f. - apply idpath. - cbn. use total2_paths_f. + apply nat_trans_eq_alt. intro x; apply idpath. + apply dirprodeq. * apply isaprop_θ_Strength1_int. * apply isaprop_θ_Strength2_int. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.Bicategories.MonoidalCategories.PointedFunctorsMonoidal UniMath.Bicategories.MonoidalCategories.Actions UniMath.Bicategories.MonoidalCategories.ConstructionOfActions UniMath.Bicategories.MonoidalCategories.ActionOfEndomorphismsInBicat UniMath.Bicategories.MonoidalCategories.ActionBasedStrength UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorCategory UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SignatureCategory UniMath.CategoryTheory.Core.Univalence