isaprop_isaprop.v

Require Export UniMath.Foundations.Propositions.

(* A simpler definition of proposition. *)
Definition isaprop' (X : UU) : UU := ∏ (x y : X), x = y.

(* Simpler definition implies standard isaprop. *)
Definition isaprop'_to_isaprop {X : UU} :
  isaprop' X → isaprop X.
Proof.
  intros f x y.
  use tpair.
  - exact (! f x x @ f x y).
  - intros p; induction p.
    exact (! pathsinv0l _). (* idpath x = ! f x x @ f x x *)
Defined.

(* isofhlevel n implies isofhlevel (n + 1) *)
Definition isofhlevel_plus_one (n : nat) :
  ∏ (X : UU), isofhlevel n X → isofhlevel (S n) X.
Proof.
  induction n.
  - intros X f x y.
    use tpair.
    + exact (pr2 f x @ ! pr2 f y).
    + intros t. induction t.
      exact (! pathsinv0r _). (* idpath x = pr2 f x @ ! pr2 f x  *)
  - intros X f x y.
    exact (IHn (x = y) (f x y)).
Defined.

(* Special case of above lemma: a proposition is also a set. *)
Definition isaprop_isaset {X : UU} : isaprop X → isaset X :=
  isofhlevel_plus_one 1 X.

(* Being a proposition is itself a proposition. *)
Definition isaprop_isaprop (X : UU) : isaprop (isaprop X).
Proof.
  (* isaprop' (isaprop X) is easier to prove *)
  apply isaprop'_to_isaprop.
  intros f g.
  (* prove propositions equal by functional extensionality *)
  apply funextsec; intro x; apply funextsec; intro y.
  use total2_paths_f.
  - (* because f is also a set, all paths (x = y) are identical *)
    apply (isaprop_isaset f).
  - (* prove sets equal by functional extensionality *)
    apply funextsec. intros t.
    (* because (x = y) is also a set, all homotopies are also identical *)
    apply (isofhlevel_plus_one 2 _).
    apply (isaprop_isaset f).
Defined.