Point-set topology

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

@@ -173,6 +173,23 @@ monic→is-embedding {f = f} bset monic =
   injective→is-embedding bset _ λ {x} {y} p →
     happly (monic {C = el (Lift _ ⊤) (λ _ _ _ _ i j → lift tt)} (λ _ → x) (λ _ → y) (funext (λ _ → p))) _
 
+injective→monic
+  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {f : A → B}
+  → is-set B
+  → injective f
+  → (∀ {C : Set ℓ''} (g h : ∣ C ∣ → A) → f ∘ g ≡ f ∘ h → g ≡ h)
+injective→monic B-set inj =
+  embedding→monic (injective→is-embedding B-set _ inj)
+
+monic→injective
+  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {f : A → B}
+  → is-set B
+  → (∀ {C : Set ℓ''} (g h : ∣ C ∣ → A) → f ∘ g ≡ f ∘ h → g ≡ h)
+  → injective f
+monic→injective {f = f} B-set monic =
+  has-prop-fibres→injective f $
+  monic→is-embedding B-set (λ {C} → monic {C})
+
 right-inverse→injective
   : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
   → {f : A → B} (g : B → A)

src/Cat/Displayed/Univalence/Thin.lagda.md

@@ -32,7 +32,7 @@ open _≅[_]_
 ```
 -->
 
-# Thinly displayed structures
+# Thinly displayed structures {defines="thin-structure"}
 
 The HoTT Book's version of the structure identity principle can be seen
 as a very early example of [[displayed category]] theory. Their

src/Cat/Functor/Adjoint.lagda.md

@@ -714,6 +714,72 @@ $\cD$, regardless of how many free objects there are. Put syntactically,
 a notion of "syntax without generators" does not imply that there is an
 object of 0 generators!
 
+
+<!--
+```agda
+module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} (F : Functor D C) where
+  private
+    module C = Cat.Reasoning C
+    module D = Cat.Reasoning D
+    module F = Func F
+
+  record Cofree-object (X : C.Ob) : Type (adj-level C D) where
+    field
+      {cofree} : D.Ob
+      counit   : C.Hom (F.₀ cofree) X
+
+      unfold : ∀ {A} (f : C.Hom (F.₀ A) X) → D.Hom A cofree
+      commute : ∀ {A} {f : C.Hom (F.₀ A) X} → counit C.∘ F.₁ (unfold f) ≡ f
+      unique
+        : ∀ {A} {f : C.Hom (F.₀ A) X} (g : D.Hom A cofree)
+        → counit C.∘ F.₁ g ≡ f
+        → g ≡ unfold f
+
+    abstract
+      unfold-natural
+        : ∀ {A B} (f : D.Hom A B) (g : C.Hom (F.₀ B) X)
+        → unfold (g C.∘ F.₁ f) ≡ unfold g D.∘ f
+      unfold-natural f g = sym (unique (unfold g D.∘ f) (F.popl commute))
+
+      unfold-counit : unfold counit ≡ D.id
+      unfold-counit = sym (unique D.id (C.elimr F.F-id))
+
+
+module _ {F : Functor D C} where
+  private
+    module C = Cat.Reasoning C
+    module D = Cat.Reasoning D
+    module F = Func F
+
+  module _ (cofree-objects : ∀ X → Cofree-object F X) where
+    private module U {X} where open Cofree-object (cofree-objects X) public
+    open Functor
+    open _=>_
+    open _⊣_
+
+    cofree-objects→functor : Functor C D
+    cofree-objects→functor .F₀ X = U.cofree {X}
+    cofree-objects→functor .F₁ f = U.unfold (f C.∘ U.counit)
+    cofree-objects→functor .F-id = ap U.unfold (C.idl _) ∙ U.unfold-counit
+    cofree-objects→functor .F-∘ f g = ap U.unfold (C.extendr (sym U.commute)) ∙ U.unfold-natural _ _
+
+    cofree-objects→right-adjoint : F ⊣ cofree-objects→functor
+    cofree-objects→right-adjoint .unit .η X = U.unfold C.id
+    cofree-objects→right-adjoint .unit .is-natural X Y f =
+      sym (U.unfold-natural _ _)
+      ∙ ap U.unfold (C.idl _ ∙ C.insertr U.commute)
+      ∙ U.unfold-natural _ _
+    cofree-objects→right-adjoint .counit .η X = U.counit
+    cofree-objects→right-adjoint .counit .is-natural X Y f = U.commute
+    cofree-objects→right-adjoint .zig = U.commute
+    cofree-objects→right-adjoint .zag =
+      sym (U.unfold-natural _ _)
+      ∙ ap U.unfold (C.cancelr U.commute)
+      ∙ U.unfold-counit
+
+```
+-->
+
 ## Induced adjunctions
 
 Any adjunction $L \dashv R$ induces, in a very boring way, an *opposite* adjunction

src/Cat/Functor/Morphism.lagda.md

@@ -193,7 +193,7 @@ formally dual to the case above, we will not dwell on it.
 
 </details>
 
-## Left and right adjoints
+## Left and right adjoints {defines="right-adjoints-preserve-monos"}
 
 If we are given an [[adjunction]] $L \dashv F$, then the right adjoint
 $F$ preserves monomorphisms. Fix a mono $a : \cC(A,B)$, and let $f, g :

src/Data/Power.lagda.md

@@ -13,8 +13,8 @@ module Data.Power where
 <!--
 ```agda
 private variable
-  ℓ : Level
-  X : Type ℓ
+  ℓ ℓ' : Level
+  X Y : Type ℓ
 ```
 -->
 
@@ -82,6 +82,27 @@ _∩_ : ℙ X → ℙ X → ℙ X
 (A ∩ B) x = A x ∧Ω B x
 ```
 
+<!--
+```agda
+∩-⊆
+  : ∀ {U V W : ℙ X}
+  → U ⊆ V → U ⊆ W
+  → U ⊆ V ∩ W
+∩-⊆ U⊆V V⊆W x x∈U =
+  (U⊆V x x∈U) , (V⊆W x x∈U)
+
+∩-⊆l
+  : ∀ (U V : ℙ X)
+  → U ∩ V ⊆ U
+∩-⊆l _ _ x (x∈U , x∈V) = x∈U
+
+∩-⊆r
+  : ∀ (U V : ℙ X)
+  → U ∩ V ⊆ V
+∩-⊆r _ _ x (x∈U , x∈V) = x∈V
+```
+-->
+
 <!--
 ```agda
 _ = ∥_∥
@@ -105,3 +126,143 @@ _∪_ : ℙ X → ℙ X → ℙ X
 infixr 32 _∩_
 infixr 31 _∪_
 ```
+
+We can also take unions of $I$-indexed families of sets $A_i$, as well
+as unions of subsets of the power set.
+
+```agda
+⋃ : ∀ {κ : Level} {I : Type κ} → (I → ℙ X) → ℙ X
+⋃ {I = I} A x = ∃Ω[ i ∈ I ] A i x
+
+⋃ˢ : ℙ (ℙ X) → ℙ X
+⋃ˢ {X = X} P = ⋃ {I = Σ[ U ∈ ℙ X ] U ∈ P} fst
+```
+
+<!--
+```agda
+⋃-⊆
+  : ∀ {κ} {I : Type κ}
+  → (Uᵢ : I → ℙ X) (V : ℙ X)
+  → (∀ i → Uᵢ i ⊆ V)
+  → ⋃ Uᵢ ⊆ V
+⋃-⊆ Uᵢ V Uᵢ⊆V x =
+  rec! (λ i → Uᵢ⊆V i x)
+
+⋃ˢ-⊆
+  : (S : ℙ (ℙ X)) (V : ℙ X)
+  → (∀ (U : ℙ X) → U ∈ S → U ⊆ V)
+  → ⋃ˢ S ⊆ V
+⋃ˢ-⊆ S V U⊆V x =
+  rec! λ U U∈S → U⊆V U U∈S x
+
+⋃-inc
+  : ∀ {κ} {I : Type κ}
+  → (Uᵢ : I → ℙ X)
+  → ∀ i → Uᵢ i ⊆ ⋃ Uᵢ
+⋃-inc Uᵢ i x x∈Uᵢ =
+  pure (i , x∈Uᵢ)
+
+⋃ˢ-inc
+  : (S : ℙ (ℙ X)) (U : ℙ X)
+  → U ∈ S
+  → U ⊆ ⋃ˢ S
+⋃ˢ-inc S U U∈S x x∈U =
+  pure ((U , U∈S) , x∈U)
+
+⋃-Σ
+  : ∀ {κ κ'} {I : Type κ} {J : I → Type κ'}
+  → (Aᵢⱼ : Σ[ i ∈ I ] (J i) → ℙ X)
+  → ⋃ Aᵢⱼ ≡ ⋃ λ i → ⋃ λ j → Aᵢⱼ (i , j)
+⋃-Σ Aᵢⱼ =
+  ℙ-ext
+    (λ x → rec! λ i j x∈Aᵢⱼ → pure (i , (pure (j , x∈Aᵢⱼ))))
+    (λ x → rec! λ i j x∈Aᵢⱼ → pure ((i , j) , x∈Aᵢⱼ))
+```
+-->
+
+Note that the union of a family of sets $A_i$ is equal to the union
+of the fibres of $A_i$.
+
+```agda
+⋃-fibre
+  : ∀ {κ} {I : Type κ}
+  → (Aᵢ : I → ℙ X)
+  → ⋃ˢ (λ A → elΩ (fibre Aᵢ A)) ≡ ⋃ Aᵢ
+⋃-fibre Aᵢ =
+  ℙ-ext
+    (λ x → rec! λ A i Aᵢ=A x∈A → pure (i , (subst (λ A → ∣ A x ∣) (sym Aᵢ=A) x∈A)))
+    (λ x → rec! λ i x∈Aᵢ → pure ((Aᵢ i , pure (i , refl)) , x∈Aᵢ))
+```
+
+Moreover, the union of an empty family of sets is equal to the empty
+set.
+
+```agda
+⋃-minimal
+  : (A : ⊥ → ℙ X)
+  → ⋃ {I = ⊥} A ≡ minimal
+⋃-minimal _ =
+  ℙ-ext (λ _ → rec! λ ff x∈A → ff) (λ _ ff → absurd ff)
+```
+
+# Images of subsets {defines="preimage direct-image"}
+
+Let $f : X \to Y$ be a function. the **preimage** of a subset $U : \power{Y}$
+is the subset $f^{-1}(U) : \power{X}$ of all $x : X$ such that $f(x) \in U$.
+
+```agda
+Preimage : (X → Y) → ℙ Y → ℙ X
+Preimage f A = A ∘ f
+```
+
+Conversely, the **direct image** of a subset $U : \power{X}$ is the
+subset $f(U) : \power{X}$ of all $y : Y$ such that there exists an
+$x \in U$ with $f(x) = y$.
+
+```agda
+Direct-image : (X → Y) → ℙ X → ℙ Y
+Direct-image {X = X} f A y = elΩ (Σ[ x ∈ X ] (x ∈ A × (f x ≡ y)))
+```
+
+We can relate preimages and direct images by observing that for every
+$U : \power{X}$ and $V : \power{Y}$, $f(U) \subseteq V$ if and only if
+$U \subseteq f^{-1}(V)$. In more categorical terms, preimages and
+direct images form and [[adjunction]] between $\power{X}$ and $\power{Y}$.
+
+```agda
+direct-image-⊆→preimage-⊆
+  : ∀ {f : X → Y}
+  → (U : ℙ X) (V : ℙ Y)
+  → Direct-image f U ⊆ V → U ⊆ Preimage f V
+direct-image-⊆→preimage-⊆ {f = f} U V f[U]⊆V x x∈U =
+  f[U]⊆V (f x) (pure (x , x∈U , refl))
+
+preimage-⊆→direct-image-⊆
+  : ∀ {f : X → Y}
+  → (U : ℙ X) (V : ℙ Y)
+  → U ⊆ Preimage f V → Direct-image f U ⊆ V
+preimage-⊆→direct-image-⊆ U V U⊆f⁻¹[V] y =
+  rec! λ x x∈U f[x]=y →
+    subst (λ y → ∣ V y ∣) f[x]=y (U⊆f⁻¹[V] x x∈U)
+```
+
+<!--
+```agda
+⋂ : ∀ {κ : Level} {I : Type κ} → (I → ℙ X) → ℙ X
+⋂ {I = I} A x = ∀Ω[ i ∈ I ] A i x
+
+_ᶜ : ℙ X → ℙ X
+(A ᶜ) x = ¬Ω (A x)
+
+≡→⊆
+  : ∀ {U V : ℙ X}
+  → U ≡ V → U ⊆ V
+≡→⊆ {V = V} p x x∈U =
+  subst (λ U → ∣ U x ∣) p x∈U
+
+≡→⊇
+  : ∀ {U V : ℙ X}
+  → U ≡ V → V ⊆ U
+≡→⊇ p = ≡→⊆ (sym p)
+```
+-->