Formalize the proof that every set is well ordered implies AC implies contradiction with univalence (Theorem 3.2.2 from HoTT book, Diaconescu's theorem)
Assume A is a linear order, show q : List A -> SList A this has a section, define is-sorted and sorted using fibre and image, show that tail of sorted list is a sorted list
TODOs:
q : List A -> SList Athis has a section, defineis-sortedandsortedusing fibre and image, show that tail of sorted list is a sorted list