dan/HITs-Examples
1
0
Fork 0
mirror of https://github.com/nmvdw/HITs-Examples synced 2025-11-03 15:13:51 +01:00
Code Issues Releases Wiki Activity

Correspondence between enumerated subobjects and k-finite subobjects

Browse Source
This commit is contained in:
Dan Frumin
2017-08-03 23:21:43 +02:00
parent f106be08de
commit 90d795b708
3 changed files with 75 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
FiniteSets/fsets/isomorphism.v
View File

@@ -54,10 +54,8 @@ Section Iso.
- intros a x HR. rewrite HR. reflexivity.
Defined.
Theorem repr_iso: FSet A <~> FSetC A.
Global Instance: IsEquiv FSet_to_FSetC.
Proof.
simple refine (@BuildEquiv (FSet A) (FSetC A) FSet_to_FSetC _ ).
apply isequiv_biinv.
unfold BiInv. split.
exists FSetC_to_FSet.
@@ -66,6 +64,17 @@ Section Iso.
unfold Sect. apply repr_iso_id_r.
Defined.
Global Instance: IsEquiv FSetC_to_FSet.
Proof.
change (IsEquiv (FSet_to_FSetC)^-1).
apply isequiv_inverse.
Defined.
Theorem repr_iso: FSet A <~> FSetC A.
Proof.
simple refine (@BuildEquiv (FSet A) (FSetC A) FSet_to_FSetC _ ).
Defined.
Theorem fset_fsetc : FSet A = FSetC A.
Proof.
apply (equiv_path _ _)^-1.