Name changes. (Following Chris' suggestions.)

Bijection -> H-equivalence
Preimage -> H-fiber

Map/Bijection.agda → Map/H-equivalence.agda

@@ -1,27 +1,22 @@
 ------------------------------------------------------------------------
--- Bijections
+-- Homotopy equivalence
 ------------------------------------------------------------------------
 
 -- Copyright (c) 2012 Favonia
 -- Copyright (c) 2011-2012 Nils Anders Danielsson
 
 {-# OPTIONS --without-K #-}
 
--- This is actually
--- (1) Homotopy isomorphism
--- (2) Homotopy equivalence
-
-module Map.Bijection where
+module Map.H-equivalence where
 
 open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)
 open import Path
 
-import Map.Equivalence as Equivalence
 open import Map.Injection using (Injective; _↣_)
 open import Map.Surjection as Surjection using (_↠_; module _↠_)
 
 ------------------------------------------------------------------------
--- Bijections
+-- Homotopy equivalence
 
 infix 0 _↔_
 
@@ -71,7 +66,8 @@ id = record
 inverse : ∀ {a b} {A : Set a} {B : Set b} → A ↔ B → B ↔ A
 inverse A↔B = record
   { surjection = record
-    { equivalence      = Equivalence.inverse equivalence
+    { from         = to
+    ; to           = from
     ; right-inverse-of = left-inverse-of
     }
   ; left-inverse-of = right-inverse-of

Map/Preimage.agda → Map/H-fiber.agda

@@ -1,5 +1,5 @@
 ------------------------------------------------------------------------
--- Preimages
+-- Homotopy Fibers
 ------------------------------------------------------------------------
 
 -- Copyright (c) 2012 Favonia
@@ -9,15 +9,15 @@
 
 -- Partly based on Voevodsky's work on univalent foundations.
 
-module Map.Preimage where
+module Map.H-fiber where
 
 open import Prelude
 open import Path
 
 open import Map.Surjection hiding (id; _∘_)
-open import Map.Bijection hiding (id; _∘_)
+open import Map.H-equivalence hiding (id; _∘_)
 
--- The preimage of y under f is denoted by f ⁻¹ y.
+-- The homotopy fiber of y under f is denoted by f ⁻¹ y.
 
 infix 5 _⁻¹_
 
@@ -29,11 +29,11 @@ id⁻¹-contractible : ∀ {ℓ} {A : Set ℓ} (x : A) → Contractible (id ⁻
 id⁻¹-contractible y = (y , refl y) , λ {(_ , p) → elim″ (λ {x} p → (y , refl y) ≡ (x , p)) (refl _) p}
 
 postulate
-  bijection⁻¹-contractible :
+  hequiv⁻¹-contractible :
     ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (A↔B : A ↔ B) →
     let open _↔_ A↔B in ∀ y → Contractible (to ⁻¹ y)
 {-
-bijection⁻¹-contractible A↔B y =
+hequiv⁻¹-contractible A↔B y =
   (from y , right-inverse-of y) ,
   λ {(x , to-x≡y) → elim′ (λ {x} p → (from y , right-inverse-of y) ≡ (x , p)) (refl _) to-x≡y}
   where

Map/Surjection.agda

@@ -12,9 +12,6 @@ module Map.Surjection where
 open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)
 open import Path
 
-open import Map.Equivalence as Equivalence
-  using (_⇔_; module _⇔_) renaming (_∘_ to _⊙_)
-
 ------------------------------------------------------------------------
 -- Surjections
 
@@ -24,11 +21,8 @@ infix 0 _↠_
 
 record _↠_ {f t} (From : Set f) (To : Set t) : Set (f ⊔ t) where
   field
-    equivalence : From ⇔ To
-
-  open _⇔_ equivalence
-
-  field
+    to   : From → To
+    from : To → From
     right-inverse-of : ∀ x → to (from x) ≡ x
 
   -- A lemma.
@@ -39,16 +33,15 @@ record _↠_ {f t} (From : Set f) (To : Set t) : Set (f ⊔ t) where
     to (from x)  ≡⟨ right-inverse-of x ⟩∎
     x            ∎
 
-  open _⇔_ equivalence public
-
 ------------------------------------------------------------------------
 -- Preorder
 
 -- _↠_ is a preorder.
 
 id : ∀ {a} {A : Set a} → A ↠ A
 id = record
-  { equivalence      = Equivalence.id
+  { to               = P.id
+  ; from             = P.id
   ; right-inverse-of = refl
   }
 
@@ -57,7 +50,8 @@ infixr 9 _∘_
 _∘_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
       B ↠ C → A ↠ B → A ↠ C
 f ∘ g = record
-  { equivalence      = equivalence f ⊙ equivalence g
+  { to               = to f ⊚ to g
+  ; from             = from g ⊚ from f
   ; right-inverse-of = to∘from
   }
   where

Map/Weak-equivalence.agda

@@ -14,15 +14,14 @@ module Map.Weak-equivalence where
 open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)
 open import Path
 
-open import Map.Equivalence hiding (id; _∘_; inverse)
 open import Map.Surjection using (_↠_; module _↠_)
-open import Map.Bijection as Bijection hiding (id; _∘_; inverse)
-open import Map.Preimage as Preimage
+open import Map.H-equivalence as H-equiv hiding (id; _∘_; inverse)
+open import Map.H-fiber as H-fiber
 
 ------------------------------------------------------------------------
 -- Is-weak-equivalence
 
--- A function f is a weak equivalence if all preimages under f are
+-- A function f is a weak equivalence if all h-fibers under f are
 -- contractible.
 
 Is-weak-equivalence : ∀ {a b} {A : Set a} {B : Set b} →
@@ -56,31 +55,29 @@ record _≈_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
       cong (proj₁ {B = λ x′ → to x′ ≡ to x}) $
         proj₂ (is-weak-equivalence (to x)) (x , refl (to x))
 
-  bijection : A ↔ B
-  bijection = record
+  hequivalence : A ↔ B
+  hequivalence = record
     { surjection = record
-      { equivalence = record
-        { to   = to
-        ; from = from
-        }
+      { to               = to
+      ; from             = from
       ; right-inverse-of = right-inverse-of
       }
     ; left-inverse-of = left-inverse-of
     }
 
-  open _↔_ bijection public
+  open _↔_ hequivalence public
     hiding (from; to; right-inverse-of; left-inverse-of)
 
   abstract
 
-    -- All preimages of an element under the weak equivalence are
+    -- All homotopy fibers of an element under the weak equivalence are
     -- equal.
 
     irrelevance : ∀ y (p : to ⁻¹ y) → (from y , right-inverse-of y) ≡ p
     irrelevance = proj₂ ⊚ is-weak-equivalence
 
     -- The two proofs left-inverse-of and right-inverse-of are
-    -- related.
+    -- related. (I.e., zigzag identity for adjoint equivalences.)
 
     left-right-lemma :
       ∀ x → cong to (left-inverse-of x) ≡ right-inverse-of (to x)
@@ -119,12 +116,12 @@ record _≈_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
              trans (cong f (sym (refl (proj₁ f⁻¹y)))) (proj₂ f⁻¹y)    ≡⟨ refl _ ⟩∎
              trans (cong f (sym (cong pr (refl f⁻¹y)))) (proj₂ f⁻¹y)  ∎)
 
--- Bijections are weak equivalences.
+-- Homotopy equivalences are weak equivalences.
 
 ↔⇒≈ : ∀ {a b} {A : Set a} {B : Set b} → A ↔ B → A ≈ B
 ↔⇒≈ A↔B = record
   { to                  = _↔_.to A↔B
-  ; is-weak-equivalence = Preimage.bijection⁻¹-contractible A↔B
+  ; is-weak-equivalence = H-fiber.hequiv⁻¹-contractible A↔B
   }
 
 ------------------------------------------------------------------------
@@ -134,20 +131,20 @@ record _≈_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
 
 -- This is subject to changes
 id : ∀ {a} {A : Set a} → A ≈ A
--- id = ↔⇒≈ Bijection.id
+-- id = ↔⇒≈ H-equiv.id
 id = record
   { to                  = P.id
-  ; is-weak-equivalence = Preimage.id⁻¹-contractible
+  ; is-weak-equivalence = H-fiber.id⁻¹-contractible
   }
 
 inverse : ∀ {a b} {A : Set a} {B : Set b} → A ≈ B → B ≈ A
-inverse = ↔⇒≈ ⊚ Bijection.inverse ⊚ _≈_.bijection
+inverse = ↔⇒≈ ⊚ H-equiv.inverse ⊚ _≈_.hequivalence
 
 infixr 9 _∘_
 
 _∘_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
       B ≈ C → A ≈ B → A ≈ C
-f ∘ g = ↔⇒≈ $ Bijection._∘_ (_≈_.bijection f) (_≈_.bijection g)
+f ∘ g = ↔⇒≈ $ H-equiv._∘_ (_≈_.hequivalence f) (_≈_.hequivalence g)
 
 -- Equational reasoning combinators.
 

Path/Sum.agda

@@ -7,18 +7,18 @@
 {-# OPTIONS --without-K #-}
 
 -- The public interface includes
---  * A bijection between (a₁ , b₁) ≡ (a₂ , b₂)
+--  * A homotopy equivalence between (a₁ , b₁) ≡ (a₂ , b₂)
 --    and Σ (a₁ ≡ a₂) (λ p → subst B p b₁ ≡ b₂)
 
 module Path.Sum where
 
 open import Prelude
 open import Path
 open import Path.Lemmas
-open import Map.Bijection hiding (id; _∘_; inverse)
+open import Map.H-equivalence hiding (id; _∘_; inverse)
 
 ------------------------------------------------------------------------
--- A bijection between ((a₁ , b₁) ≡ (a₂ , b₂)) and
+-- A homotopy equivalence between ((a₁ , b₁) ≡ (a₂ , b₂)) and
 -- Σ (a₁ ≡ a₂) (λ p → subst B p b₁ ≡ b₂)
 
 -- Compose equalities in a Σ type
@@ -45,17 +45,15 @@ open import Map.Bijection hiding (id; _∘_; inverse)
       subst (B ∘ proj₁) s≡s b₁  ≡⟨ cong[dep] (B ∘ proj₁) proj₂ s≡s ⟩∎
       b₂                        ∎
 
--- Composition and decomposition form a bijection!
+-- Composition and decomposition form a homotopy equivalence!
 
 ≡Σ↔Σ≡ : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} (B : A → Set ℓ₂) {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} →
           ((a₁ , b₁) ≡ (a₂ , b₂)) ↔ Σ (a₁ ≡ a₂) (λ p → subst B p b₁ ≡ b₂)
 ≡Σ↔Σ≡ B {a₁} {a₂} {b₁} {b₂} =
   record
   { surjection = record
-    { equivalence = record
-      { to = ≡Σ⇒Σ≡ B
-      ; from = Σ≡⇒≡Σ B
-      }
+    { to               = ≡Σ⇒Σ≡ B
+    ; from             = Σ≡⇒≡Σ B
     ; right-inverse-of = right-inverse-of
     }
   ; left-inverse-of = left-inverse-of
@@ -79,7 +77,7 @@ open import Map.Bijection hiding (id; _∘_; inverse)
         pa pb
 
 ------------------------------------------------------------------------
--- A bijection between ((a₁ , b₁) ≡ (a₂ , b₂)) and
+-- A homotopy equivalence between ((a₁ , b₁) ≡ (a₂ , b₂)) and
 -- (a₁ ≡ a₂) × (b₁ ≡ b₂). I.e., non-dependent version
 
 -- Compose equalities in a Σ type
@@ -102,17 +100,15 @@ open import Map.Bijection hiding (id; _∘_; inverse)
     a≡a = cong proj₁ s≡s
     b≡b = cong proj₂ s≡s
 
--- Composition and decomposition form a bijection!
+-- Composition and decomposition form a homotopy equivalence!
 
 ≡×↔×≡ : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} (B : Set ℓ₂) {a₁ a₂ : A} {b₁ b₂ : B} →
           ((a₁ , b₁) ≡ (a₂ , b₂)) ↔ (a₁ ≡ a₂) × (b₁ ≡ b₂)
 ≡×↔×≡ B {a₁} {a₂} {b₁} {b₂} =
   record
   { surjection = record
-    { equivalence = record
-      { to = ≡×⇒×≡
-      ; from = ×≡⇒≡×
-      }
+    { to               = ≡×⇒×≡
+    ; from             = ×≡⇒≡×
     ; right-inverse-of = right-inverse-of
     }
   ; left-inverse-of = left-inverse-of

README.agda

@@ -24,20 +24,17 @@ import Prelude
 ------------------------------------------------------------------------
 -- Maps, continuous functions between spaces
 
--- H-iso style equivalence
-import Map.Bijection
-
--- A record with only to & from (no proofs)
-import Map.Equivalence
+-- Homotopy equivalence
+import Map.H-equivalence
 
 -- Injections
 import Map.Injection
 
 -- Surjections
 import Map.Surjection
 
--- Preimage
-import Map.Preimage
+-- Homotopy Fiber
+import Map.H-fiber
 
 -- Weak-equivalent
 import Map.Weak-equivalence