Last active
April 5, 2019 23:26
-
-
Save fizruk/fd7b785cc6558efb340ad8fcfc98a604 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment