fixes

Cubical/CW/Connected.agda

@@ -66,20 +66,24 @@ yieldsConnectedCWskel A k =
   Σ[ sk ∈ yieldsCWskel A ] ((sk .fst 0 ≡ 1) × ((n : ℕ) → n <ᵗ k → sk .fst (suc n) ≡ 0))
 
 -- Alternatively, we may say that its colimit is n-connected
-yieldsConnectedCWskel' : (A : ℕ → Type ℓ) (n : ℕ) → Type _
-yieldsConnectedCWskel' A n = Σ[ sk ∈ yieldsCWskel A ] isConnected (2 +ℕ n) (realise (_ , sk))
+yieldsCombinatorialConnectedCWskel : (A : ℕ → Type ℓ) (n : ℕ) → Type _
+yieldsCombinatorialConnectedCWskel A n =
+  Σ[ sk ∈ yieldsCWskel A ] isConnected (2 +ℕ n) (realise (_ , sk))
 
 connectedCWskel : (ℓ : Level) (n : ℕ) → Type (ℓ-suc ℓ)
 connectedCWskel ℓ n = Σ[ X ∈ (ℕ → Type ℓ) ] (yieldsConnectedCWskel X n)
 
-connectedCWskel' : (ℓ : Level) (n : ℕ) → Type (ℓ-suc ℓ)
-connectedCWskel' ℓ n = Σ[ X ∈ (ℕ → Type ℓ) ] (yieldsConnectedCWskel' X n)
+combinatorialConnectedCWskel : (ℓ : Level) (n : ℕ) → Type (ℓ-suc ℓ)
+combinatorialConnectedCWskel ℓ n =
+  Σ[ X ∈ (ℕ → Type ℓ) ] (yieldsCombinatorialConnectedCWskel X n)
 
 isConnectedCW : ∀ {ℓ} (n : ℕ) → Type ℓ → Type (ℓ-suc ℓ)
-isConnectedCW {ℓ = ℓ} n A = Σ[ sk ∈ connectedCWskel ℓ n ] realise (_ , (snd sk .fst)) ≃ A
+isConnectedCW {ℓ = ℓ} n A =
+  Σ[ sk ∈ connectedCWskel ℓ n ] realise (_ , (snd sk .fst)) ≃ A
 
 isConnectedCW' : ∀ {ℓ} (n : ℕ) → Type ℓ → Type (ℓ-suc ℓ)
-isConnectedCW' {ℓ = ℓ} n A = Σ[ sk ∈ connectedCWskel' ℓ n ] realise (_ , (snd sk .fst)) ≃ A
+isConnectedCW' {ℓ = ℓ} n A =
+  Σ[ sk ∈ combinatorialConnectedCWskel ℓ n ] realise (_ , (snd sk .fst)) ≃ A
 
 --- Goal: show that these two definitions coincide (note that indexing is off by 2) ---
 -- For the base case, we need to analyse α₀ : Fin n × S⁰ → X₁ (recall,
@@ -89,13 +93,13 @@ isConnectedCW' {ℓ = ℓ} n A = Σ[ sk ∈ connectedCWskel' ℓ n ] realise (_
 -- us to iteratively shrink X₁ by contracting the image of α₀(a,-).
 
 -- Decision producedures
-hasDecidableImage-Fin×S⁰ : {A : Type ℓ}
+inhabitedFibres?-Fin×S⁰ : {A : Type ℓ}
   (da : Discrete A) (n : ℕ) (f : Fin n × S₊ 0 → A)
-  → hasDecidableImage f
-hasDecidableImage-Fin×S⁰ {A = A} da n =
-  subst (λ C → (f : C → A) → hasDecidableImage f)
+  → inhabitedFibres? f
+inhabitedFibres?-Fin×S⁰ {A = A} da n =
+  subst (λ C → (f : C → A) → inhabitedFibres? f)
         (isoToPath (invIso Iso-Fin×Bool-Fin))
-        (hasDecidableImageFin da _)
+        (inhabitedFibres?Fin da _)
 
 private
   allConst? : {A : Type ℓ} {n : ℕ} (dis : Discrete A)
@@ -112,11 +116,11 @@ private
   ... | yes p | inr x = inr (_ , (snd x))
   ... | no ¬p | q = inr (_ , ¬p)
 
--- α₀ must be is surjective
+-- α₀ must have a section
 isSurj-α₀ : (n m : ℕ) (f : Fin n × S₊ 0 → Fin (suc (suc m)))
   → isConnected 2 (Pushout f fst)
   → (y : _) → Σ[ x ∈ _ ] f x ≡ y
-isSurj-α₀ n m f c y with (hasDecidableImage-Fin×S⁰ DiscreteFin n f y)
+isSurj-α₀ n m f c y with (inhabitedFibres?-Fin×S⁰ DiscreteFin n f y)
 ... | inl x = x
 isSurj-α₀ n m f c x₀ | inr q = ⊥.rec nope
   where
@@ -521,7 +525,7 @@ module CWLemmas-0Connected where
 
 -- Uning this, we can show that a 0-connected CW complex can be
 -- approximated by one with trivial 1-skeleton.
-module _ (A : ℕ → Type ℓ) (sk+c : yieldsConnectedCWskel' A 0) where
+module _ (A : ℕ → Type ℓ) (sk+c : yieldsCombinatorialConnectedCWskel A 0) where
   private
     open CWLemmas-0Connected
     c = snd sk+c

Cubical/CW/Subcomplex.agda

@@ -1,5 +1,19 @@
 {-# OPTIONS --safe --lossy-unification #-}
 
+{-
+This file contains a definition of a notion of (strict)
+subcomplexes of a CW complex. Here, a subomplex of a complex
+C = colim ( C₀ → C₁ → ...)
+is simply the complex
+C⁽ⁿ⁾ := colim (C₀ → ... → Cₙ = Cₙ = ...)
+
+This file contains.
+1. Definition of above
+2. A `strictification' of finite CW complexes in terms of above
+3. An elmination principle for finite CW complexes
+4. A proof that C and C⁽ⁿ⁾ has the same homolog in appropriate dimensions.
+-}
+
 module Cubical.CW.Subcomplex where
 
 open import Cubical.Foundations.Prelude
@@ -8,6 +22,7 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
 
 open import Cubical.Data.Nat
 open import Cubical.Data.Fin.Inductive.Base
@@ -36,20 +51,24 @@ private
   variable
     ℓ ℓ' ℓ'' : Level
 
--- finite subcomplex of a cw complex
+-- finite subcomplex C⁽ⁿ⁾ of a cw complex C.
 module _ (C : CWskel ℓ) where
+  -- The underlying family of types is that of C but ending at some
+  -- fixed n.
   subComplexFam : (n : ℕ) (m : ℕ) → Type ℓ
   subComplexFam n m with (m ≟ᵗ n)
   ... | lt x = fst C m
   ... | eq x = fst C m
   ... | gt x = fst C n
 
+  -- Similarly for the number of cells
   subComplexCard : (n : ℕ) → ℕ → ℕ
   subComplexCard n m with (m ≟ᵗ n)
   ... | lt x = snd C .fst m
   ... | eq x = 0
   ... | gt x = 0
 
+  -- Attaching maps
   subComplexα : (n m : ℕ) → Fin (subComplexCard n m) × S⁻ m → subComplexFam n m
   subComplexα n m with (m ≟ᵗ n)
   ... | lt x = snd C .snd .fst m
@@ -61,6 +80,7 @@ module _ (C : CWskel ℓ) where
   ... | lt x = CW₀-empty C
   ... | eq x = CW₀-empty C
 
+  -- Resulting complex has CW structure
   subComplexFam≃Pushout : (n m : ℕ)
     → subComplexFam n (suc m) ≃ Pushout (subComplexα n m) fst
   subComplexFam≃Pushout n m with (m ≟ᵗ n) | ((suc m) ≟ᵗ n)
@@ -78,17 +98,19 @@ module _ (C : CWskel ℓ) where
     ⊥.rec (¬m<ᵗm (subst (n <ᵗ_) x₁ (<ᵗ-trans x <ᵗsucm)))
   ... | gt x | gt x₁ = isoToEquiv (PushoutEmptyFam (λ x → ¬Fin0 (fst x)) ¬Fin0)
 
+  -- packaging it all together
   subComplexYieldsCWskel : (n : ℕ) → yieldsCWskel (subComplexFam n)
   fst (subComplexYieldsCWskel n) = subComplexCard n
   fst (snd (subComplexYieldsCWskel n)) = subComplexα n
   fst (snd (snd (subComplexYieldsCWskel n))) = subComplex₀-empty n
   snd (snd (snd (subComplexYieldsCWskel n))) m = subComplexFam≃Pushout n m
 
+  -- main definition
   subComplex : (n : ℕ) → CWskel ℓ
   fst (subComplex n) = subComplexFam n
   snd (subComplex n) = subComplexYieldsCWskel n
 
-  -- as a finite CWskel
+  -- Let us also show that this defines a _finite_ CW complex
   subComplexFin : (m : ℕ) (n : Fin (suc m))
     → isEquiv (CW↪ (subComplexFam (fst n) , subComplexYieldsCWskel (fst n)) m)
   subComplexFin m (n , r) with (m ≟ᵗ n) | (suc m ≟ᵗ n)
@@ -128,17 +150,18 @@ module _ (C : CWskel ℓ) where
   ... | eq x = idEquiv _
   ... | gt x = ⊥.rec (¬squeeze (x , p))
 
-realiseSubComplex : (n : ℕ) (C : CWskel ℓ) → Iso (fst C n) (realise (subComplex C n))
+-- C⁽ⁿ⁾ₙ ≃ Cₙ
+realiseSubComplex : (n : ℕ) (C : CWskel ℓ)
+  → Iso (fst C n) (realise (subComplex C n))
 realiseSubComplex n C =
   compIso (equivToIso (complex≃subcomplex C n flast))
           (realiseFin n (finSubComplex C n))
 
+-- Strictifying finCWskel
 niceFinCWskel : ∀ {ℓ} (n : ℕ) → finCWskel ℓ n → finCWskel ℓ n
 fst (niceFinCWskel n (A , AC , fin)) = finSubComplex (A , AC) n .fst
 snd (niceFinCWskel n (A , AC , fin)) = finSubComplex (A , AC) n .snd
 
-open import Cubical.Foundations.HLevels
-
 makeNiceFinCWskel : ∀ {ℓ} {A : Type ℓ} → isFinCW A → isFinCW A
 makeNiceFinCWskel {A = A} (dim , cwsk , e) = better
   where
@@ -161,6 +184,7 @@ snd (makeNiceFinCW C) =
 makeNiceFinCW≡ : ∀ {ℓ} (C : finCW ℓ) → makeNiceFinCW C ≡ C
 makeNiceFinCW≡ C = Σ≡Prop (λ _ → squash₁) refl
 
+-- Elimination principles
 makeNiceFinCWElim : ∀ {ℓ ℓ'} {A : finCW ℓ → Type ℓ'}
   → ((C : finCW ℓ) → A (makeNiceFinCW C))
   → (C : _) → A C
@@ -173,7 +197,7 @@ makeNiceFinCWElim' : ∀ {ℓ ℓ'} {C : Type ℓ} {A : ∥ isFinCW C ∥₁ →
 makeNiceFinCWElim' {A = A} pr ind =
   PT.elim pr λ cw → subst A (squash₁ _ _) (ind cw)
 
--- Goal: Show that a cell complex C and its subcomplex Cₙ share
+-- Goal: Show that a cell complex C and its subcomplex C⁽ⁿ⁾ share
 -- homology in low enough dimensions
 module _ (C : CWskel ℓ) where
   ChainSubComplex : (n : ℕ) → snd C .fst n ≡ snd (subComplex C (suc n)) .fst n

Cubical/Data/Fin/Inductive/Properties.agda

@@ -145,13 +145,13 @@ DiscreteFin x y with discreteℕ (fst x) (fst y)
 ... | yes p = yes (Σ≡Prop (λ _ → isProp<ᵗ) p)
 ... | no ¬p = no λ q → ¬p (cong fst q)
 
-hasDecidableImageFin : ∀ {ℓ} {A : Type ℓ}
+inhabitedFibres?Fin : ∀ {ℓ} {A : Type ℓ}
   (da : Discrete A) (n : ℕ) (f : Fin n → A)
-  → hasDecidableImage f
-hasDecidableImageFin {A = A} da zero f y = inr λ x → ⊥.rec (¬Fin0 x)
-hasDecidableImageFin {A = A} da (suc n) f y with da (f fzero) y
+  → inhabitedFibres? f
+inhabitedFibres?Fin {A = A} da zero f y = inr λ x → ⊥.rec (¬Fin0 x)
+inhabitedFibres?Fin {A = A} da (suc n) f y with da (f fzero) y
 ... | yes p = inl (fzero , p)
-... | no ¬p with (hasDecidableImageFin da n (f ∘ fsuc) y)
+... | no ¬p with (inhabitedFibres?Fin da n (f ∘ fsuc) y)
 ... | inl q = inl ((fsuc (fst q)) , snd q)
 ... | inr q = inr (elimFin-alt ¬p q)
 

Cubical/HITs/Pushout/Properties.agda

@@ -705,7 +705,8 @@ PushoutCompEquivIso {ℓA = ℓA} {ℓA'} {ℓB} {ℓB'} {ℓC} e1 e2 f g =
                            (Pushout f g))
        λ f g → idIso)
 
--- Computation of cofibre of the quotient map B → B/A
+-- Computation of cofibre of the quotient map B → B/A (where B/A
+-- denotes the cofibre of some f : B → A)
 module _ {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
   private
     open 3x3-span

Cubical/HITs/Wedge/Properties.agda

@@ -86,7 +86,7 @@ cofibInr-⋁ {A = A} {B = B} =
           (cofibInl-⋁ {A = B} {B = A})
 
 -- A ⋁ Unit ≃ A ≃ Unit ⋁ A
-⋁-rUnitIso : {A : Pointed ℓ} → Iso (A ⋁ (Unit* {ℓ'} , tt*)) (fst A)
+⋁-rUnitIso : {A : Pointed ℓ} → Iso (A ⋁ Unit*∙ {ℓ'}) (fst A)
 Iso.fun ⋁-rUnitIso (inl x) = x
 Iso.fun (⋁-rUnitIso {A = A}) (inr x) = pt A
 Iso.fun (⋁-rUnitIso {A = A}) (push a i) = pt A
@@ -96,7 +96,7 @@ Iso.leftInv ⋁-rUnitIso (inl x) = refl
 Iso.leftInv ⋁-rUnitIso (inr x) = push tt
 Iso.leftInv ⋁-rUnitIso (push tt i) j = push tt (i ∧ j)
 
-⋁-lUnitIso : {A : Pointed ℓ} → Iso ((Unit* {ℓ'} , tt*) ⋁ A) (fst A)
+⋁-lUnitIso : {A : Pointed ℓ} → Iso (Unit*∙ {ℓ'} ⋁ A) (fst A)
 ⋁-lUnitIso = compIso ⋁-commIso ⋁-rUnitIso
 
 -- cofiber of constant function
@@ -294,6 +294,8 @@ SuspBouquet≃Bouquet : (A : Type ℓ) (B : A → Pointed ℓ')
   → Susp (⋁gen A B) ≃ ⋁gen A (λ a → Susp∙ (fst (B a)))
 SuspBouquet≃Bouquet A B = isoToEquiv (Iso-SuspBouquet-Bouquet A B)
 
+-- cofibre of f ∨→ g : A ⋁ B → C is cofibre of
+-- inr ∘ f : A → cofib g
 module _ {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
   (f : A →∙ C) (g : B →∙ C)
   where
@@ -402,6 +404,8 @@ module _ {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
                         (cofib {B = cofib (fst g)} (λ x → inr (fst f x)))
   cofib∨→compIsoᵣ = compIso cofib∨→distrIso (equivToIso (_ , isPushoutRight))
 
+-- cofibre of f ∨→ g : A ⋁ B → C is cofibre of
+-- inr ∘ g : B → cofib f
 cofib∨→compIsoₗ :
   {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
   (f : A →∙ C) (g : B →∙ C)
@@ -416,7 +420,7 @@ cofib∨→compIsoₗ f g =
               ; (push a i) j → symDistr (snd g) (sym (snd f)) (~ j) i}))
           (cofib∨→compIsoᵣ g f)
 
-
+-- (⋁ᵢ Aᵢ ∨ ⋁ⱼ Bᵢ) ≃ ⋁ᵢ₊ⱼ(Aᵢ + Bⱼ)
 module _ {A : Type ℓ} {B : Type ℓ'}
   {P : A → Pointed ℓ''} {Q : B → Pointed ℓ''}
   where
@@ -440,7 +444,7 @@ module _ {A : Type ℓ} {B : Type ℓ'}
     ⋁gen⊎← (push (inr x) i) = (push tt ∙ λ i → inr (push x i)) i
 
   ⋁gen⊎Iso : Iso (⋁gen∙ A P ⋁ ⋁gen∙ B Q)
-                   (⋁gen (A ⊎ B) (⊎.rec P Q))
+                  (⋁gen (A ⊎ B) (⊎.rec P Q))
   Iso.fun ⋁gen⊎Iso = ⋁gen⊎→
   Iso.inv ⋁gen⊎Iso = ⋁gen⊎←
   Iso.rightInv ⋁gen⊎Iso (inl tt) = refl
@@ -458,7 +462,7 @@ module _ {A : Type ℓ} {B : Type ℓ'}
     compPath-filler' (push tt) (λ i → inr (push a i)) (~ j) i
   Iso.leftInv ⋁gen⊎Iso (push a i) j = push a (i ∧ j)
 
--- computation of the cofibre of a map out of a wedge
+-- f : ⋁ₐ Bₐ → C has cofibre the pushout of cofib (f ∘ inr) ← Σₐ → A
 module _ {ℓA ℓB ℓC : Level} {A : Type ℓA} {B : A → Pointed ℓB} (C : Pointed ℓC)
          (f : (⋁gen A B , inl tt) →∙ C) where
   private

Cubical/Relation/Nullary/Properties.agda

@@ -203,12 +203,11 @@ Discrete→Separated d x y = Dec→Stable (d x y)
 Discrete→isSet : Discrete A → isSet A
 Discrete→isSet = Separated→isSet ∘ Discrete→Separated
 
--- Decidable images
-hasDecidableImage : ∀ {ℓ'} {A : Type ℓ} {B : Type ℓ'}
-  (f : A → B) → Type (ℓ-max ℓ ℓ')
-hasDecidableImage {A = A} {B = B} f =
-  (y : B) → (Σ[ x ∈ A ] f x ≡ y) ⊎ ((x : A) → ¬ f x ≡ y)
-
 ≡no : ∀ {A : Type ℓ} x y → Path (Dec A) x (no y)
 ≡no (yes p) y = ⊥.rec (y p)
 ≡no (no ¬p) y i = no (isProp¬ _ ¬p y i)
+
+inhabitedFibres? : ∀ {ℓ'} {A : Type ℓ} {B : Type ℓ'}
+  (f : A → B) → Type (ℓ-max ℓ ℓ')
+inhabitedFibres? {A = A} {B = B} f =
+  (y : B) → (Σ[ x ∈ A ] f x ≡ y) ⊎ ((x : A) → ¬ f x ≡ y)