proposition: Lemma from_nat_functor_eq {X Y : UU} : ∏ f g : nat_functor X → Y, (f (true,, fromempty) = g (true,, fromempty)) -> (∏ h, f (false,, λ _, h tt) = g (false,, λ _, h tt)) -> f = g.
proof: Proof. intros f g ? eqfalse. apply funextsec; intro pair. induction pair as [b bfun]. induction b. - refine (maponpaths (λ z, f (true,, z)) (eqfromempty bfun) @ _). refine (_ @ !maponpaths (λ z, g (true,, z)) (eqfromempty bfun)). assumption. - cbn in eqfalse. refine (maponpaths (λ z, f (false,, z)) (eta_unit bfun) @ _). refine (_ @ !maponpaths (λ z, g (false,, z)) (eta_unit bfun)). apply eqfalse. Defined.
imports: UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.Type.Core UniMath.Induction.FunctorAlgebras_legacy UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core UniMath.Induction.W.Fibered