# favonia/homotopy

Rename files.

1 parent b134eab commit c45779a59c6e214ee688fda4efa7d0d3c2ab4e02 committed Jun 5, 2012
2 Map/Weak-equivalence.agda → Map/WeakEquivalence.agda
 @@ -9,7 +9,7 @@ -- Partly based on Voevodsky's work on univalent foundations. -module Map.Weak-equivalence where +module Map.WeakEquivalence where open import Prelude as P hiding (id) renaming (_∘_ to _⊚_) open import Path
 @@ -37,8 +37,8 @@ import Map.Surjection -- Homotopy Fiber import Map.H-fiber --- Weak-equivalent -import Map.Weak-equivalence +-- Weak equivalent +import Map.WeakEquivalence ------------------------------------------------------------------------ -- Paths (propositional equalities in type theories) @@ -70,7 +70,7 @@ import Path.Sum -- Kristina's theorem: hom is contractable iff we have a dependent -- eliminator. -- (Only the interesting direction.) -import Space.Bool-alternative +import Space.Bool.Initial -- Basic facts about Fin import Space.Fin.Lemmas @@ -98,14 +98,14 @@ import Space.Nat.Lemmas import Space.Sphere -- Alternative definition of spheres (two-point) -import Space.Sphere-alternative +import Space.Sphere.TwoPoints -- Definition of the Hopf junior (S₀ ↪ S₁ → S₁) -- and a proof that the total space is indeed S₁ import Space.Sphere.Hopf-junior -- A proof that Ω₁(S₁) is ℤ -import Space.Sphere.Omega1S1-Z +import Space.Sphere.Omega1 -- Definition of torus --import Space.Torus
6 Space/Bool-alternative.agda → Space/Bool/Initial.agda
 @@ -1,12 +1,12 @@ ------------------------------------------------------------------------ --- Alternative Axioms for Boolean +-- Alternative axioms for Boolean ------------------------------------------------------------------------ -- Copyright (c) 2012 Favonia -- Two equivalent ways to axiomatize Boolean -- with extensionality for functions: --- (1) non-dependent elim + hom +-- (1) non-dependent elim + being inital -- (2) dependent elim {-# OPTIONS --without-K #-} @@ -18,7 +18,7 @@ -- myself (Favonia) as an Agda exercise. The other direction -- should not be hard with extensionalty for functions... -module Space.Bool-alternative where +module Space.Bool.Initial where open import Prelude hiding (Bool; true; false; if_then_else_) open import Path
2 Space/Sphere/Hopf-junior.agda
 @@ -25,7 +25,7 @@ open import Path open import Path.Lemmas open import Path.Sum open import Map.H-equivalence hiding (_∘_; id) -open import Map.Weak-equivalence as Weak hiding (_∘_; id) +open import Map.WeakEquivalence as Weak hiding (_∘_; id) import Univalence.Lemmas; open Univalence.Lemmas univ
4 Space/Sphere/Omega1S1-Z.agda → Space/Sphere/Omega1.agda
 @@ -10,7 +10,7 @@ open import Univalence -module Space.Sphere.Omega1S1-Z +module Space.Sphere.Omega1 (univ : ∀ {ℓ} (A B : Set ℓ) → Univalence-axiom A B) where open import Prelude renaming (zero to ℕzero; suc to ℕsuc) @@ -19,7 +19,7 @@ open import Path.Lemmas open import Path.Sum open import Path.Higher-order open import Map.H-equivalence hiding (_∘_; id) -open import Map.Weak-equivalence as Weak hiding (_∘_; id) +open import Map.WeakEquivalence as Weak hiding (_∘_; id) import Univalence.Lemmas; open Univalence.Lemmas univ
2 Space/Sphere-alternative.agda → Space/Sphere/TwoPoints.agda
 @@ -8,7 +8,7 @@ {-# OPTIONS --without-K #-} -module Space.Sphere-alternative where +module Space.Sphere.TwoPoints where open import Prelude open import Path
2 Univalence.agda
 @@ -14,7 +14,7 @@ module Univalence where open import Prelude open import Path open import Path.Lemmas -open import Map.Weak-equivalence as Weak hiding (_∘_; id) +open import Map.WeakEquivalence as Weak hiding (_∘_; id) ------------------------------------------------------------------------ -- The univalence axiom
2 Univalence/Lemmas.agda
 @@ -16,7 +16,7 @@ open import Prelude open import Path open import Path.Lemmas open import Map.H-equivalence hiding (_∘_; id) -open import Map.Weak-equivalence as Weak hiding (_∘_; id) +open import Map.WeakEquivalence as Weak hiding (_∘_; id) ------------------------------------------------------------------------ -- Conversions between homotopy equivalences, weak equivalences, and identities