proposition: Lemma abs_from_one {n : nat} (s : (L (S n) : hSet)) (t : (L n : hSet)) : abs s = t ≃ (app' L • extend_tuple (λ _, lift_constant _ (one L)) t = t) × (extended_composition (app' L) (λ _, t) = s).
proof: Proof. use (logeqweq (make_hProp _ (setproperty _ _ _)) (make_hProp _ (isapropdirprod _ _ (setproperty _ _ _) (setproperty _ _ _)))). - intro H1. assert (H2 : extended_composition (app' L) (λ _, t) = s). { refine (!app_from_app' _ @ _). refine (!maponpaths _ H1 @ _). apply H. } refine (make_dirprod _ H2). refine (_ @ H1). exact (!aux1 H2). - intro H'. induction H' as [H1 H2]. refine (_ @ H1). exact (aux1 H2). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.LambdaTheoryCategoryCore