diff options
author | Jason Gross <jasongross9@gmail.com> | 2016-08-01 13:22:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-08-01 13:22:21 -0700 |
commit | 212b073990426dccd8799294c583e2e58a015463 (patch) | |
tree | 546ae1c8fc26f3f73f71e94bc49072caf598191a /src/Util/Isomorphism.v | |
parent | b92653291b6ac977d2bf1b72420d686580adf2f4 (diff) |
Add documentation: Equality, HProp, Isomorphism, Sigma (#41)
* Add doc: Equality, HProp, Isomorphism, Sigma
* Update documentation with suggestions from Andres
Diffstat (limited to 'src/Util/Isomorphism.v')
-rw-r--r-- | src/Util/Isomorphism.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/Util/Isomorphism.v b/src/Util/Isomorphism.v index 0e6553dcd..25984483e 100644 --- a/src/Util/Isomorphism.v +++ b/src/Util/Isomorphism.v @@ -1,3 +1,32 @@ +(** * Isomorphisms *) +(** Following the category-theoretic definition, [f : A → B] is an + isomorphism when it has an inverse [f⁻¹ : B → A] which is both a + left and a right inverse. In the language of homotopy type + theory, we are formalizing quasi-invertibility; this notion of + isomorphism is not an hProp. The better notations of equivalence + (such that all proofs of [IsEquiv f] are equal when only assuming + function extensionality) are more complicated. Possibilities + include: *) + +(** - Adjoint equivalence, the default of HoTT/HoTT: *) +(** +<< +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. +>> *) +(** - Contractible fibers: [∀ y : B, Contr { x : A | f x = y }] where + [Contr T := { center : T | forall y, center = y }] *) + +(** This is useful for classifying equalities in a theoretically nice + way. *) + Class IsIso {A B} (f : A -> B) := { iso_inv : B -> A; is_right_inv : forall x, f (iso_inv x) = x; |