Simplex Category

src/1Lab/Classical.lagda.md

@@ -120,7 +120,7 @@ Surjections-split =
   ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-set A → is-set B
   → (f : A → B)
   → is-surjective f
-  → ∥ (∀ b → fibre f b) ∥
+  → ∥ split-surjective f ∥
 ```
 
 We show that these two statements are logically equivalent^[they are also

src/1Lab/Equiv/Fibrewise.lagda.md

@@ -16,7 +16,7 @@ open import 1Lab.Type
 module 1Lab.Equiv.Fibrewise where
 ```
 
-# Fibrewise equivalences
+# Fibrewise equivalences {defines="fibrewise-equivalence"}
 
 In HoTT, a type family `P : A → Type` can be seen as a [_fibration_]
 with total space `Σ P`, with the fibration being the projection

src/1Lab/Function/Antiinjection.lagda.md

@@ -0,0 +1,191 @@
+---
+description: |
+  Antiinjective functions.
+---
+<!--
+```agda
+open import 1Lab.Function.Surjection
+open import 1Lab.Function.Embedding
+open import 1Lab.HLevel.Universe
+open import 1Lab.HIT.Truncation
+open import 1Lab.HLevel.Closure
+open import 1Lab.Inductive
+open import 1Lab.Equiv
+open import 1Lab.Path
+open import 1Lab.Type
+
+open import Meta.Idiom
+open import Meta.Bind
+```
+-->
+```agda
+module 1Lab.Function.Antiinjection where
+```
+
+<!--
+```
+private variable
+  ℓ ℓ₁ : Level
+  A B C : Type ℓ
+  w x : A
+```
+-->
+
+# Antiinjective functions {defines="split-antiinjective antiinjective"}
+
+A function is **split antiinjective** if it comes equipped with a choice
+of fibre that contains 2 distinct elements. Likewise, a function is
+**antiinjective** if it is merely split injective. This is constructively
+stronger than non-injective, as we actually know at least one obstruction
+to injectivity! Moreover, note that split antiinjectivity is a structure
+on a function, not a property; there may be obstructions to injectivity.
+
+```agda
+record split-antiinjective (f : A → B) : Type (level-of A ⊔ level-of B) where
+  no-eta-equality
+  field
+    pt : B
+    x₀ : A
+    x₁ : A
+    map-to₀ : f x₀ ≡ pt
+    map-to₁ : f x₁ ≡ pt
+    distinct : ¬ (x₀ ≡ x₁)
+
+is-antiinjective : (A → B) → Type _
+is-antiinjective f = ∥ split-antiinjective f ∥
+```
+
+<!--
+```agda
+open split-antiinjective
+```
+-->
+
+As the name suggests, antiinjective functions are not injective.
+
+```agda
+split-antiinj→not-injective
+  : {f : A → B}
+  → split-antiinjective f
+  → ¬ (injective f)
+split-antiinj→not-injective f-antiinj f-inj =
+  f-antiinj .distinct (f-inj (f-antiinj .map-to₀ ∙ sym (f-antiinj .map-to₁)))
+
+is-antiinj→not-injective
+  : {f : A → B}
+  → is-antiinjective f
+  → ¬ (injective f)
+is-antiinj→not-injective f-antiinj =
+  rec! split-antiinj→not-injective f-antiinj
+```
+
+<!--
+```agda
+split-antiinj→not-equiv
+  : {f : A → B}
+  → split-antiinjective f
+  → ¬ (is-equiv f)
+split-antiinj→not-equiv f-ai f-eqv =
+  split-antiinj→not-injective f-ai (Equiv.injective (_ , f-eqv))
+
+is-antiinj→not-equiv
+  : {f : A → B}
+  → is-antiinjective f
+  → ¬ (is-equiv f)
+is-antiinj→not-equiv f-ai f-eqv =
+  is-antiinj→not-injective f-ai (Equiv.injective (_ , f-eqv))
+```
+-->
+
+Precomposition by an (split) antinjective function always yields a
+(split) antiinjective function.
+
+```agda
+split-antiinj-∘r
+  : {f : B → C} {g : A → B}
+  → split-antiinjective g
+  → split-antiinjective (f ∘ g)
+split-antiinj-∘r {f = f} g-antiinj .pt = f (g-antiinj .pt)
+split-antiinj-∘r {f = f} g-antiinj .x₀ = g-antiinj .x₀
+split-antiinj-∘r {f = f} g-antiinj .x₁ = g-antiinj .x₁
+split-antiinj-∘r {f = f} g-antiinj .map-to₀ = ap f (g-antiinj .map-to₀)
+split-antiinj-∘r {f = f} g-antiinj .map-to₁ = ap f (g-antiinj .map-to₁)
+split-antiinj-∘r {f = f} g-antiinj .distinct = g-antiinj .distinct
+
+is-antiinj-∘r
+  : {f : B → C} {g : A → B}
+  → is-antiinjective g
+  → is-antiinjective (f ∘ g)
+is-antiinj-∘r {f = f} = ∥-∥-map (split-antiinj-∘r {f = f})
+```
+
+If $f : B \to C$ is split antiinjective and $g : A \to B$ can be equipped with a choice
+of fibres at the obstruction to injectivity, then $f \circ g$ is also antiinjective.
+
+```agda
+split-antiinj+in-image→split-antiinj
+  : {f : B → C} {g : A → B}
+  → (f-ai : split-antiinjective f)
+  → fibre g (f-ai .x₀) → fibre g (f-ai .x₁)
+  → split-antiinjective (f ∘ g)
+split-antiinj+in-image→split-antiinj {f = f} {g = g} f-ai (a₀ , p₀) (a₁ , p₁) = fg-ai
+  where
+    fg-ai : split-antiinjective (f ∘ g)
+    fg-ai .pt = f-ai .pt
+    fg-ai .x₀ = a₀
+    fg-ai .x₁ = a₁
+    fg-ai .map-to₀ = ap f p₀ ∙ f-ai .map-to₀
+    fg-ai .map-to₁ = ap f p₁ ∙ f-ai .map-to₁
+    fg-ai .distinct a₀=a₁ = f-ai .distinct (sym p₀ ·· ap g a₀=a₁ ·· p₁)
+```
+
+In particular, this means that composing a (split) antiinjection with a (split)
+surjection yields a (split) antiinjection.
+
+```agda
+split-antiinj+split-surj→split-antiinj
+  : {f : B → C} {g : A → B}
+  → split-antiinjective f
+  → split-surjective g
+  → split-antiinjective (f ∘ g)
+split-antiinj+split-surj→split-antiinj f-ai g-s =
+  split-antiinj+in-image→split-antiinj f-ai (g-s (f-ai .x₀)) (g-s (f-ai .x₁))
+
+is-antiinj+is-surj→is-antiinj
+  : {f : B → C} {g : A → B}
+  → is-antiinjective f
+  → is-surjective g
+  → is-antiinjective (f ∘ g)
+is-antiinj+is-surj→is-antiinj ∥f-ai∥ g-s = do
+  f-ai ← ∥f-ai∥
+  fib₀ ← g-s (f-ai .x₀)
+  fib₁ ← g-s (f-ai .x₁)
+  pure (split-antiinj+in-image→split-antiinj f-ai fib₀ fib₁)
+```
+
+```agda
+split-antiinj-cancell
+  : {f : B → C} {g : A → B}
+  → injective f
+  → split-antiinjective (f ∘ g)
+  → split-antiinjective g
+split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .pt =
+  g (fg-ai .x₀)
+split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .x₀ =
+  fg-ai .x₀
+split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .x₁ =
+  fg-ai .x₁
+split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .map-to₀ =
+ refl
+split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .map-to₁ =
+  f-inj (fg-ai .map-to₁ ∙ sym (fg-ai .map-to₀))
+split-antiinj-cancell {f = f} {g = g} f-inj fg-ai .distinct =
+  fg-ai .distinct
+
+is-antiinj-cancell
+  : {f : B → C} {g : A → B}
+  → injective f
+  → is-antiinjective (f ∘ g)
+  → is-antiinjective g
+is-antiinj-cancell f-inj = ∥-∥-map (split-antiinj-cancell f-inj)
+```

src/1Lab/Function/Antisurjection.lagda.md

@@ -0,0 +1,145 @@
+---
+description: |
+  Antisurjective functions.
+---
+<!--
+```agda
+open import 1Lab.Function.Surjection
+open import 1Lab.Function.Embedding
+open import 1Lab.HLevel.Universe
+open import 1Lab.HIT.Truncation
+open import 1Lab.HLevel.Closure
+open import 1Lab.Type.Sigma
+open import 1Lab.Inductive
+open import 1Lab.HLevel
+open import 1Lab.Equiv
+open import 1Lab.Path
+open import 1Lab.Type
+
+open import Meta.Idiom
+open import Meta.Bind
+```
+-->
+```agda
+module 1Lab.Function.Antisurjection where
+```
+
+<!--
+```
+private variable
+  ℓ ℓ₁ : Level
+  A B C : Type ℓ
+  w x : A
+```
+-->
+
+## Antisurjective functions {defines="antisurjective split-antisurjective"}
+
+A function is **antisurjective** if there merely exists some $b : B$
+with an empty fibre. This is constructively stronger than being
+non-surjective, which states that it is not the case that all fibres
+are (merely) inhabited.
+
+```agda
+is-antisurjective : (A → B) → Type _
+is-antisurjective {B = B} f = ∃[ b ∈ B ] (¬ (fibre f b))
+```
+
+Likewise, a function is **split antisurjective** if there is some
+$b : B$ with an empty fibre. Note that this is a structure on a function,
+not a property, as there may be many ways a function fails to be surjective!
+
+```agda
+split-antisurjective : (A → B) → Type _
+split-antisurjective {B = B} f = Σ[ b ∈ B ] (¬ (fibre f b))
+```
+
+As the name suggests, antisurjective functions are not surjective.
+
+```agda
+split-antisurj→not-surjective
+  : {f : A → B}
+  → split-antisurjective f
+  → ¬ (is-surjective f)
+split-antisurj→not-surjective (b , ¬fib) f-s =
+  rec! (λ a p → ¬fib (a , p)) (f-s b)
+
+is-antisurj→not-surjective
+  : {f : A → B}
+  → is-antisurjective f
+  → ¬ (is-surjective f)
+is-antisurj→not-surjective f-as =
+  rec! (λ b ¬fib → split-antisurj→not-surjective (b , ¬fib)) f-as
+```
+
+<!--
+```agda
+is-antisurj→not-equiv
+  : {f : A → B}
+  → is-antisurjective f
+  → ¬ (is-equiv f)
+is-antisurj→not-equiv f-as f-eqv =
+  is-antisurj→not-surjective f-as (λ b → inc (f-eqv .is-eqv b .centre))
+
+split-antisurj→not-equiv
+  : {f : A → B}
+  → split-antisurjective f
+  → ¬ (is-equiv f)
+split-antisurj→not-equiv f-as = is-antisurj→not-equiv (inc f-as)
+```
+-->
+
+If $f$ is antisurjective and $g$ is an arbitrary function, then $f \circ g$
+is also antisurjective.
+
+```agda
+split-antisurj-∘l
+  : {f : B → C} {g : A → B}
+  → split-antisurjective f
+  → split-antisurjective (f ∘ g)
+split-antisurj-∘l {g = g} (c , ¬fib) = c , ¬fib ∘ Σ-map g (λ p → p)
+
+is-antisurj-∘l
+  : {f : B → C} {g : A → B}
+  → is-antisurjective f
+  → is-antisurjective (f ∘ g)
+is-antisurj-∘l {f = f} {g = g} = ∥-∥-map split-antisurj-∘l
+```
+
+If $f$ is injective and $g$ is antisurjective, then $f \circ g$ is
+also antisurjective.
+
+```agda
+inj+split-antisurj→split-antisurj
+  : {f : B → C} {g : A → B}
+  → injective f
+  → split-antisurjective g
+  → split-antisurjective (f ∘ g)
+inj+split-antisurj→split-antisurj {f = f} f-inj (b , ¬fib) =
+  f b , ¬fib ∘ Σ-map₂ f-inj
+
+inj+is-antisurj→is-antisurj
+  : {f : B → C} {g : A → B}
+  → injective f
+  → is-antisurjective g
+  → is-antisurjective (f ∘ g)
+inj+is-antisurj→is-antisurj f-inj =
+  ∥-∥-map (inj+split-antisurj→split-antisurj f-inj)
+```
+
+```agda
+split-antisurj-cancelr
+  : {f : B → C} {g : A → B}
+  → is-surjective g
+  → split-antisurjective (f ∘ g)
+  → split-antisurjective f
+split-antisurj-cancelr {f = f} {g = g} surj (c , ¬fib) =
+  c , rec! λ b p → rec! (λ a q → ¬fib (a , ap f q ∙ p)) (surj b)
+
+is-antisurj-cancelr
+  : {f : B → C} {g : A → B}
+  → is-surjective g
+  → is-antisurjective (f ∘ g)
+  → is-antisurjective f
+is-antisurj-cancelr surj = ∥-∥-map (split-antisurj-cancelr surj) 
+```