proposition: Lemma isapropFiniteStructure X : isaprop (FiniteStructure X).
proof: Proof. intros. apply invproofirrelevance; intros r s. destruct r as [m p]. destruct s as [n q]. apply subtypePairEquality. { intros k. apply invproofirrelevance; intros [[r b] i] [[s c] j]; simpl in r,s,i,j. admit. } { apply weqtoeqstn. exact (weqcomp (pr1 p) (invweq (pr1 q))). } Abort. Theorem enumeration_FiniteOrderedSet (X:FiniteOrderedSet) : iscontr (FiniteStructure X). Proof. intros. simple refine (_,,_). { exists (fincard (finitenessProperty X)). Abort. Theorem isasetFiniteOrderedSet : isaset FiniteOrderedSet. Proof. Abort. Definition isLattice {X:hSet} (le:hrel X) (min max:binop X) := ∑ po : isPartialOrder le, ∑ lub : ∏ x y z, le x z ∧ le y z <-> le (max x y) z, ∑ glb : ∏ x y t, le t x ∧ le t y <-> le t (min x y), unit. Definition istrans2 {X:hSet} (le lt:hrel X) := ∑ transltle: ∏ x y z, lt x y -> le y z -> lt x z, ∑ translelt: ∏ x y z, le x y -> lt y z -> lt x z, unit. Definition iswklin {X} (lt:hrel X) := ∏ x y z, lt x y -> lt x z ∨ lt z y. Definition isComputablyOrdered {X:hSet} (lt:hrel X) (min max:binop X) := let le x y := ¬ lt y x in ∑ latt: isLattice le min max, ∑ trans2: istrans2 le lt, ∑ translt: istrans lt, ∑ irrefl: isirrefl lt, ∑ cotrans: iscotrans lt, unit. Local Ltac expand ic := induction ic as [[[[transle reflle]antisymmle][lub[glb _]]] [[transltle [translelt _]][translt[irrefl[cotrans _]]]]]. Section OtherProperties. Variable (X:hSet) (lt:hrel X) (min max:binop X) (ic:isComputablyOrdered lt min max). Let le x y := ¬ lt y x. Let apart x y := lt y x ∨ lt x y. Local Lemma apart_isirrefl : isirrefl apart. Proof. expand ic. intros x a. unfold apart in a. apply (a hfalse); clear a; intros b. induction b as [b|b]; exact (irrefl _ b). Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions