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;