proposition: Theorem ZFS_univalence (x y : ZFS) : (x = y) ≃ (ZFS_iso x y).
proof: Proof. set (P := λ x, λ y, preZFS_univalence x y). set (Q := λ x, (hasuniquerepbranch x ,, isaprop_hasuniquerepbranch x)). apply (substructure_univalence _ _ P Q x y). 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