Added proof that KFinite types with decidable equality are Bishop finite (UniMath#2047)

Author: klinashka

UniMath/Combinatorics/FiniteSets.v

@@ -618,3 +618,12 @@ Delimit Scope finset with finset.
 Notation "'∑' x .. y , P" := (FiniteSetSum (λ x,.. (FiniteSetSum (λ y, P))..))
                                (at level 200, x binder, y binder, right associativity) : finset.
 (* type this in emacs in agda-input method with \sum *)
+
+(* A surjection from stn 0 is an equivalence *)
+Lemma surj_from_stn0_to_neg {X : UU} (f : ⟦ 0 ⟧ → X ) : (issurjective f) → nelstruct 0 X.
+Proof.
+  intros surj. apply tpair with (pr1 := f). intros x.
+  apply fromempty, (squash_to_prop (surj x) (isapropempty)).
+  intros [contra eq]; clear surj.
+  apply negstn0, contra.
+Qed.

UniMath/Combinatorics/KFiniteTypes.v

@@ -23,6 +23,7 @@
 Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.MoreFoundations.PartA.
 Require Import UniMath.MoreFoundations.Notations.
+Require Import UniMath.MoreFoundations.DecidablePropositions.
 Require Import UniMath.Combinatorics.FiniteSets.
 Require Import UniMath.Combinatorics.StandardFiniteSets.
 
@@ -241,3 +242,90 @@ Section kfinite_definition.
     := hinhfun kfinstruct_finstruct.
 
 End kfinite_definition.
+
+Section iskfinite_isdeceq_isfinite.
+(** 
+  This section provides the necessary construction to prove that 
+  every K-Finite type with decidable equality is Bishop-finite. 
+  
+  Proof outline: 
+  Let X be a K-Finite type. Then there exists n : nat with a surjection 
+  from stn n to X.
+
+  The proof goes by induction on n, with the type X being generalized.
+  In the base case, we have a surjection from an uninhabited type to X.
+  Thus, X must also have no elements and therefore, X is equivalent with 
+  stn 0.
+
+  In the inductive step, we assume that for any type X for which there 
+  exists a surjection from stn n to X and has decidable equality is 
+  Bishop finite. We have to show that if there exists a surjection f 
+  from stn (S n) to X and X has decidable equality, then X is Bishop 
+  finite.
+  Let g : stn n -> X such that g (x) := f x. If X has decidable equality, 
+  then it is decidable whether f (n) is included in the image of g. 
+
+  We will thus proceed by case analysis on whether f n is included in the image of g.
+  If f n is included in the image of g, then g must be a surjection as well. By the inductive 
+  hypothesis X is Bishop finite. If f n is not included in the image of g, we will denote 
+  y := f n. We now consider the type X / y (pair X (\x -> x != y)) which is inhabited by 
+  terms different than y. First, we note that X / y has decidable equality. Secondly, we note 
+  that X / y + unit is equivalent to X. Lastly, we note that by restricting the codomain of g 
+  to X / y, we obtain a surjection g1 : stn n -> X / y. By the inductive hypothesis, the type 
+  X / y is Bishop finite, and thus equivalent to stn m for some m : nat. 
+  To conclude, we have the following chain of equivalences 
+  X ≃ X / y + 1 ≃ stn m + 1 ≃ stn (S m). Thus, X is Bishop finite.
+
+  *)
+
+  Lemma issurjective_stnfun_singleton_complement {X : UU} {n : nat} (f : stn (S n) → X) 
+        (nfib : ¬ hfiber (fun_stnsn_to_stnn f) (f lastelement)) : issurjective f → 
+        issurjective (stnfun_singleton_complement f nfib).
+  Proof.
+    intros surjf y.
+    destruct y as [x neq].
+    use squash_to_prop.
+    - exact (hfiber f x).
+    - exact (surjf x).
+    - apply propproperty.
+    - intros [[m lth] q]; clear surjf. apply hinhpr.
+      induction (natlehchoice _ _ (natlthsntoleh _ _ lth)).
+      + apply (tpair _ (m ,, a)).
+        unfold stnfun_singleton_complement, fun_stnsn_to_stnn, make_stn.
+        apply subtypePath_prop; cbn.
+        induction q. apply maponpaths, stn_eq, idpath. 
+      + assert (H : (m ,, lth = lastelement)) by apply stn_eq, b.
+        apply fromempty. induction neq. induction H. apply pathsinv0, q.
+  Qed.
+
+  Lemma kfinstruct_dec_finstruct {X : UU} : isdeceq X → kfinstruct X → finstruct X.
+  Proof.
+    intros deceqX [n [f surj]].
+    generalize dependent X.
+    induction n; intros.
+    - apply tpair with (pr1 := 0).
+      apply surj_from_stn0_to_neg with (f := f). assumption. 
+    - set (g := fun_stnsn_to_stnn f).
+      set (y := f lastelement).
+      induction (isdeceq_isdecsurj g y deceqX).
+      + apply IHn with (f := g); try apply surj_fun_stnsn_to_stnn; assumption.
+      + set (g' := stnfun_singleton_complement f b).
+        set (surjg' := (issurjective_stnfun_singleton_complement f b surj)).
+        specialize IHn with (f := g').
+        apply IHn in surjg';
+        [ | apply isdeceq_subtype; try assumption; intros x; apply isapropneg ].
+        destruct surjg' as [s1 s2].
+        apply tpair with (pr1 := (S s1)); unfold nelstruct.
+        eapply weqcomp. 
+        * apply invweq, weqdnicoprod, lastelement.
+        * eapply weqcomp.
+          { eapply weqcoprodf1, s2. }
+          apply weq_singleton_complement_unit; assumption.
+  Qed.
+
+  Lemma iskfinite_dec_to_isfinite {X : UU} : isdeceq X → iskfinite X → isfinite X.
+  Proof.
+    intros deceqX. apply hinhfun, kfinstruct_dec_finstruct, deceqX.
+  Qed.
+
+End iskfinite_isdeceq_isfinite.

UniMath/Combinatorics/StandardFiniteSets.v

@@ -2025,3 +2025,55 @@ Lemma stn_ord_bij {n : nat} (f : ⟦ n ⟧ ≃ ⟦ n ⟧) :
 Proof.
   apply (stn_ord_inj (weqtoincl f)).
 Defined.
+
+(* Functions with domain in Standard finite sets. *)
+Definition fun_stnsn_to_stnn {X : UU} {n : nat} (f : stn (S n) → X) : stn n → X := f ∘ dni_lastelement.
+
+Definition stnfun_singleton_complement {X : UU} {n : nat} (f : stn (S n) → X) : 
+      ¬ hfiber (fun_stnsn_to_stnn f) (f lastelement) → stn n → 
+      (singleton_complement (f lastelement)).
+Proof.
+  intros X0 X1.
+  exists (fun_stnsn_to_stnn f X1).
+  intros contra. apply X0.
+  eexists. apply contra.
+Defined.
+
+Lemma isdeceq_isdecsurj {X : UU} {n : nat} (f : ⟦ n ⟧ → X ) (y : X) : 
+    isdeceq X → decidable (hfiber f y).
+Proof.
+  generalize dependent X.
+  induction n; intros X f x deceqX.
+  - right. intros contra. eapply weqstn0toempty, pr1, contra.
+  - set (g := fun_stnsn_to_stnn f). specialize IHn with (f := g) (y := x).
+    set (H := IHn deceqX).
+    induction H.
+    + left. induction a as [p eq]. induction p as [m lth].
+      apply tpair with (pr1 := (m ,, (natlthtolths _ _ lth))), eq.
+    + induction (deceqX (f (lastelement)) x); [left | right].
+      * apply (tpair _ lastelement). assumption.
+      * intros H. induction H as [p eq]. induction p as [m lth]. 
+        induction (natlehchoice _ _ (natlthsntoleh _ _ lth)).
+        -- apply b. apply tpair with (pr1 := (m ,, a)).
+           induction eq. unfold g, fun_stnsn_to_stnn, make_stn. unfold funcomp.
+           apply maponpaths, stn_eq, idpath.
+        -- apply b0. unfold lastelement. induction b1, eq.
+           apply maponpaths, stn_eq, idpath.
+Qed.
+
+Lemma surj_fun_stnsn_to_stnn {X : UU} {n : nat} (f : ⟦ S n ⟧ → X) : isdeceq X → issurjective f → 
+      hfiber (fun_stnsn_to_stnn f) (f lastelement) → issurjective (fun_stnsn_to_stnn f).
+Proof.
+  intros deceqX surj x. induction x as [x eq].
+  intros y'.
+  induction (deceqX (f lastelement) y').
+  - induction a. apply hinhpr, tpair with (pr1 := x), eq.
+  - apply (squash_to_prop (surj y')); try apply propproperty.
+    intros m. induction m as [m eq']; induction m as [m lth]. apply hinhpr.
+    induction (natlehchoice _ _ (natlthsntoleh _ _ lth)).
+    + apply tpair with (pr1 := m ,, a).
+      unfold fun_stnsn_to_stnn, make_stn, funcomp.
+      induction eq'. apply maponpaths, stn_eq, idpath.
+    + induction eq', b0. apply fromempty, b. 
+      apply maponpaths, stn_eq, idpath.
+Qed.

UniMath/MoreFoundations/DecidablePropositions.v

@@ -456,6 +456,39 @@ Definition natneq_DecidableProposition : DecidableRelation nat :=
 
 End DecidablePropositions.
 
+Section DecidableEquality.
+
+Lemma isdeceq_subtype {X : UU} (P : hsubtype X) : 
+  isdeceq X → isdeceq P.
+Proof.
+  intros deceqX predP. apply isdeceq_total2.
+  + apply deceqX.
+  + intros x. apply isdeceqifisaprop, propproperty.
+Qed.
+
+  Definition singleton_complement {X : UU} (y : X) : hsubtype X := λ x, make_hProp (x != y) (isapropneg (x = y)).
+
+  Lemma weq_singleton_complement_unit {X : UU} (y : X) : isdeceq X → carrier (singleton_complement y) ⨿ unit ≃ X.
+  Proof.
+    intros deceqx.
+    use weq_iso.
+    - intros [[x neq] | tt]; [apply x | apply y].
+    - intros x. induction (deceqx x y); [right; apply tt | left].
+      apply tpair with (pr1 := x), b. 
+    - intros [[x neq] | tt].
+      + induction (deceqx x y).
+        * apply fromempty. induction neq. assumption.
+        * cbn. apply maponpaths, subtypePath_prop, idpath. 
+      + induction (deceqx y y).
+        * induction tt. apply idpath.
+        * apply fromempty, b, idpath.
+    - intros x; cbn beta.
+      induction (deceqx x y); cbn beta;
+      try induction a; apply idpath.
+  Qed.
+
+End DecidableEquality.
+
 Declare Scope decidable_nat.
 Notation " x < y " := (natlth_DecidableProposition x y) (at level 70, no associativity) :
                         decidable_nat.