proposition: Lemma isweq_Up_to_Up (T : Tree) (x : pr11 T) (y : pr11 (Up x)): isweq (Up_to_Up T x y).
proof: Proof. set (f := Up_to_Up T x y). set (g := Up_to_Up_inv T x y). assert (L : ∏ x, f (g x) = x). { intros z. unfold g ; unfold Up_to_Up_inv. unfold f ; unfold Up_to_Up. destruct z as [z π]. apply total2_paths_equiv. assert (H : (pr1 z,, pr122 (pr221 T) x (pr1 y) (pr1 z) (pr2 y) π) = z). { apply total2_paths_equiv. exists (idpath (pr1 z)). apply propproperty. } exists H. apply propproperty. } assert (LL : ∏ x, g (f x) = x). { intros z. unfold g ; unfold Up_to_Up_inv. unfold f ; unfold Up_to_Up. reflexivity. } apply (@weq_iso _ _ _ _ LL L). Qed.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions