Library Equations.HSetInstances

From Equations Require Import Init DepElim HSets.

Set Universe Polymorphism.

Instance eqdec_hset (A : Type) `(EqDec A) : HSet A.
Proof.
red. red. apply eq_proofs_unicity.
Defined.

Standard instances.

Instance unit_eqdec : EqDec unit.
Proof. eqdec_proof. Defined.

Instance bool_eqdec : EqDec bool.
Proof. eqdec_proof. Defined.

Instance nat_eqdec : EqDec nat.
Proof. eqdec_proof. Defined.

Instance prod_eqdec {A B} `(EqDec A) `(EqDec B) : EqDec (prod A B).
Proof. eqdec_proof. Defined.

Instance sum_eqdec {A B} `(EqDec A) `(EqDec B) : EqDec (A + B).
Proof. eqdec_proof. Defined.

Instance list_eqdec {A} `(EqDec A) : EqDec (list A).
Proof. eqdec_proof. Defined.

Any signature made up entirely of decidable types is decidable.

Polymorphic Definition eqdec_sig_Id@{i} {A : Type@{i}} {B : A -> Type@{i}}
            `(HSets.EqDec A) `(forall a, HSets.EqDec (B a)) :
  HSets.EqDec@{i} (sigma A B).
Proof.
  Set Printing Universes.
  intros. intros [xa xb] [ya yb].
  case (HSets.eq_dec xa ya). intros Hxya. destruct Hxya. case (HSets.eq_dec xb yb).
  + intros He; destruct He. left. reflexivity.
  + intros. right. apply Id_simplification_sigma2@{i i}. apply e.
  + intros. right. apply Id_simplification_sigma1@{i i}.
    intros He _; revert He. apply e.
Defined.

Existing Instance eqdec_sig_Id.