dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

path_ishprop now in extensionality

This commit is contained in:
Niels 2017-08-11 13:15:31 +02:00
parent 89808c7297
commit 5766024f95
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
FiniteSets/fsets/extensionality.v
View File

@ -40,7 +40,7 @@ Section ext.
forall Y, X ⊆ X ∪ Y. forall Y, X ⊆ X ∪ Y.
Proof. Proof.
hinduction X ; try (repeat (intro; intros; apply path_forall); hinduction X ; try (repeat (intro; intros; apply path_forall);
intro ; apply equiv_hprop_allpath ; apply _). intro ; apply path_ishprop).
- apply (fun _ => tt). - apply (fun _ => tt).
- intros a Y. - intros a Y.
apply (tr(inl(tr idpath))). apply (tr(inl(tr idpath))).
@ -69,7 +69,7 @@ Section ext.
eapply equiv_iff_hprop_uncurried. eapply equiv_iff_hprop_uncurried.
split. split.
- hinduction X ; - hinduction X ;
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _). try (intros; repeat (apply path_forall; intro); apply path_ishprop).
+ intros ; reflexivity. + intros ; reflexivity.
+ intros a f. + intros a f.
apply f. apply f.
@ -89,7 +89,7 @@ Section ext.
left. left.
apply Ha. apply Ha.
- hinduction X ; - hinduction X ;
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _). try (intros; repeat (apply path_forall; intro); apply path_ishprop).
+ intros. contradiction. + intros. contradiction.
+ intros b f a. + intros b f a.
simple refine (Trunc_ind _ _) ; cbn. simple refine (Trunc_ind _ _) ; cbn.