proposition: Lemma lambda_theory_morphism_eq {L L' : lambda_theory} (F F' : lambda_theory_morphism L L') (H : (F : algebraic_theory_morphism L L') = F') : F = F'.
proof: Proof. apply subtypePath. { intro. apply isapropunit. } apply subtypePath. { intro. apply isapropdirprod; do 2 (apply impred_isaprop; intro); apply setproperty. } apply H. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheories