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

Merge branch 'master' of https://github.com/nmvdw/HITs-Examples

This commit is contained in:
Niels van der Weide 2017-09-25 13:04:28 +02:00
parent 7281bfc0bf 73fbe8716a
commit 35f0452a6a
1 changed files with 15 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
FiniteSets/subobjects/k_finite.v
View File

@ -144,13 +144,27 @@ Section k_properties.
apply (tr (idpath)).
Defined.
Lemma Kf_surjection {X Y : Type} (f : X -> Y) `{IsSurjection f} :
Kf X -> Kf Y.
Proof.
intros HX. apply Kf_unfold. apply Kf_unfold in HX.
destruct HX as [Xf HXf].
exists (fmap FSet f Xf).
intro y.
pose (x' := center (merely (hfiber f y))).
simple refine (@Trunc_rec (-1) (hfiber f y) _ _ _ x'). clear x'; intro x.
destruct x as [x Hfx]. rewrite <- Hfx.
apply fmap_isIn.
apply (HXf x).
Defined.
Lemma Kf_sum {A B : Type} : Kf A -> Kf B -> Kf (A + B).
Proof.
intros HA HB.
kf_unfold.
destruct HA as [X HX].
destruct HB as [Y HY].
exists ((fset_fmap inl X) ∪ (fset_fmap inr Y)).
exists (disjoint_sum X Y).
intros [a | b]; simpl; apply tr; [ left | right ];
apply fmap_isIn.
+ apply (HX a).
@ -194,20 +208,6 @@ Section k_properties.
- apply (HB b).
Defined.
Lemma Kf_surjection {X Y : Type} (f : X -> Y) `{IsSurjection f} :
Kf X -> Kf Y.
Proof.
intros HX. apply Kf_unfold. apply Kf_unfold in HX.
destruct HX as [Xf HXf].
exists (fmap FSet f Xf).
intro y.
pose (x' := center (merely (hfiber f y))).
simple refine (@Trunc_rec (-1) (hfiber f y) _ _ _ x'). clear x'; intro x.
destruct x as [x Hfx]. rewrite <- Hfx.
apply fmap_isIn.
apply (HXf x).
Defined.
Lemma S1_Kfinite : Kf S1.
Proof.
apply Kf_unfold.