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

Merge branch 'bloop'

This commit is contained in:
Dan Frumin 2017-06-14 13:09:52 +02:00
parent abec9ecd00 a1a6912cb2
commit 036d1599b2
1 changed files with 19 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
FiniteSets/properties.v
View File

@ -479,18 +479,18 @@ Defined.
Lemma eq1 (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y). Lemma eq1 (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
Proof. Proof.
unshelve eapply BuildEquiv. eapply equiv_iff_hprop_uncurried.
{ intro H. rewrite H. split; apply union_idem. } split.
unshelve esplit. - intro H. split.
{ intros [H1 H2]. etransitivity. apply H1^. apply (comm Y X @ ap (U X) H^ @ union_idem X).
rewrite comm. apply H2. } apply (ap (U X) H^ @ union_idem X @ H).
intro; apply path_prod; apply set_path2. - intros [H1 H2]. etransitivity. apply H1^.
all: intro; apply set_path2. apply (comm Y X @ H2).
Defined. Defined.
Lemma subset_union_l `{Funext} X : Lemma subset_union_l `{Funext} X :
forall Y, subset X (U X Y) = true. forall Y, subset X (U X Y) = true.
Proof.
hinduction X; hinduction X;
try (intros; apply path_forall; intro; apply set_path2). try (intros; apply path_forall; intro; apply set_path2).
- reflexivity. - reflexivity.
@ -511,12 +511,12 @@ Lemma subset_union_equiv `{Funext}
: forall X Y : FSet A, subset X Y = true <~> U X Y = Y. : forall X Y : FSet A, subset X Y = true <~> U X Y = Y.
Proof. Proof.
intros X Y. intros X Y.
unshelve eapply BuildEquiv. eapply equiv_iff_hprop_uncurried.
apply subset_union. split.
unshelve esplit. - apply subset_union.
{ intros HXY. rewrite <- HXY. clear HXY. - intros HXY. etransitivity.
apply subset_union_l. } apply (ap _ HXY^).
all: intro; apply set_path2. apply subset_union_l.
Defined. Defined.
Lemma eq_subset `{Funext} (X Y : FSet A) : Lemma eq_subset `{Funext} (X Y : FSet A) :
@ -528,7 +528,7 @@ Proof.
eapply equiv_functor_prod'; apply subset_union_equiv. eapply equiv_functor_prod'; apply subset_union_equiv.
Defined. Defined.
Lemma subset_isIn `{FE : Funext} (X Y : FSet A) : Lemma subset_isIn `{FE :Funext} (X Y : FSet A) :
(forall (a : A), isIn a X = true -> isIn a Y = true) (forall (a : A), isIn a X = true -> isIn a Y = true)
<-> (subset X Y = true). <-> (subset X Y = true).
Proof. Proof.
@ -584,24 +584,6 @@ Proof.
intros; intro; intros; apply set_path2. intros; intro; intros; apply set_path2.
Defined. Defined.
Lemma HPropEquiv (X Y : Type) (P : IsHProp X) (Q : IsHProp Y) :
(X <-> Y) -> (X <~> Y).
Proof.
intros [f g].
simple refine (BuildEquiv _ _ _ _).
apply f.
simple refine (BuildIsEquiv _ _ _ _ _ _ _).
- apply g.
- unfold Sect.
intro x.
apply Q.
- unfold Sect.
intro x.
apply P.
- intros.
apply set_path2.
Defined.
Theorem fset_ext `{Funext} (X Y : FSet A) : Theorem fset_ext `{Funext} (X Y : FSet A) :
X = Y <~> (forall (a : A), isIn a X = isIn a Y). X = Y <~> (forall (a : A), isIn a X = isIn a Y).
Proof. Proof.
@ -609,18 +591,10 @@ Proof.
transitivity transitivity
((forall a, isIn a Y = true -> isIn a X = true) ((forall a, isIn a Y = true -> isIn a X = true)
*(forall a, isIn a X = true -> isIn a Y = true)). *(forall a, isIn a X = true -> isIn a Y = true)).
- eapply equiv_functor_prod'. - eapply equiv_functor_prod';
apply HPropEquiv. apply equiv_iff_hprop_uncurried;
exact _.
exact _.
split ; apply subset_isIn. split ; apply subset_isIn.
apply HPropEquiv. - apply equiv_iff_hprop_uncurried.
exact _.
exact _.
split ; apply subset_isIn.
- apply HPropEquiv.
exact _.
exact _.
split. split.
* intros [H1 H2 a]. * intros [H1 H2 a].
specialize (H1 a) ; specialize (H2 a). specialize (H1 a) ; specialize (H2 a).