From fedad73ac5390b4ec5ed706ebffbe1a39d71f1fc Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sun, 30 Jun 2024 13:43:13 -0400
Subject: [PATCH 1/9] wip: define Top

---
 src/Data/Power.lagda.md    |   7 ++
 src/Topology/Base.lagda.md | 141 +++++++++++++++++++++++++++++++++++++
 2 files changed, 148 insertions(+)
 create mode 100644 src/Topology/Base.lagda.md

diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md
index 0de45bf3b..d19d9e3cc 100644
--- a/src/Data/Power.lagda.md
+++ b/src/Data/Power.lagda.md
@@ -105,3 +105,10 @@ _∪_ : ℙ X → ℙ X → ℙ X
 infixr 32 _∩_
 infixr 31 _∪_
 ```
+
+<!--
+```agda
+⋃ : ∀ {κ : Level} {I : Type κ} → (I → ℙ X) → ℙ X
+⋃ {I = I} A x = ∃Ω[ i ∈ I ] A i x
+```
+-->
diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
new file mode 100644
index 000000000..e0e0b92bf
--- /dev/null
+++ b/src/Topology/Base.lagda.md
@@ -0,0 +1,141 @@
+---
+description: |
+  The basic theory of topological spaces.
+---
+<!--
+```agda
+open import Cat.Prelude
+
+open import Data.Power
+
+open import 1Lab.Reflection hiding (absurd)
+```
+-->
+```agda
+module Topology.Base where
+```
+
+```agda
+record is-topology {o ℓ} (X : Type o) (is-open : (X → Ω) → Type ℓ) : Type (lsuc o ⊔ ℓ) where
+  field
+    ∩-open : ∀ {U V : X → Ω} → is-open U → is-open V → is-open (U ∩ V)
+    ⋃-open : {I : Type o} → (Uᵢ : I → X → Ω) → (∀ i → is-open (Uᵢ i)) → is-open (⋃ Uᵢ)
+    maximal-open : is-open maximal
+    has-is-set : is-set X
+    is-open-is-prop : ∀ {U} → is-prop (is-open U)
+
+  minimal-open : is-open minimal
+  minimal-open =
+    subst is-open
+      (ext (λ _ → Ω-ua (rec! (λ ff tt → ff)) λ ff → inc (lift ff , tt)))
+      (⋃-open {I = Lift _ ⊥} (λ _ _ → ⊤Ω) (λ ff → absurd (Lift.lower ff)))
+
+record Topological-space (o ℓ : Level) : Type (lsuc o ⊔ lsuc ℓ) where
+  field
+    Ob : Type o
+    is-open : (Ob → Ω) → Type ℓ
+    has-is-topology : is-topology Ob is-open
+
+  open is-topology has-is-topology public
+```
+
+<!--
+```agda
+private variable
+  o ℓ o' ℓ' : Level
+  X Y Z : Topological-space o ℓ
+
+instance
+  Underlying-Topological-space : ∀ {o ℓ} → Underlying (Topological-space o ℓ)
+  Underlying-Topological-space .Underlying.ℓ-underlying = _
+  Underlying-Topological-space .Underlying.⌞_⌟ = Topological-space.Ob
+
+  open hlevel-projection
+
+  Topological-space-ob-hlevel-proj : hlevel-projection (quote Topological-space.Ob)
+  Topological-space-ob-hlevel-proj .has-level   = quote Topological-space.has-is-set
+  Topological-space-ob-hlevel-proj .get-level _ = pure (lit (nat 2))
+  Topological-space-ob-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
+  Topological-space-ob-hlevel-proj .get-argument _                     = typeError []
+
+  Topological-space-open-hlevel-proj : hlevel-projection (quote Topological-space.is-open)
+  Topological-space-open-hlevel-proj .has-level   = quote Topological-space.is-open-is-prop
+  Topological-space-open-hlevel-proj .get-level _ = pure (lit (nat 1))
+  Topological-space-open-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
+  Topological-space-open-hlevel-proj .get-argument _                     = typeError []
+
+```
+-->
+
+```agda
+record Continuous
+  {o ℓ o' ℓ'}
+  (X : Topological-space o ℓ) (Y : Topological-space o' ℓ')
+  : Type (o ⊔ o' ⊔ ℓ ⊔ ℓ') where
+  no-eta-equality
+  private
+    module X = Topological-space X
+    module Y = Topological-space Y
+  field
+    hom : X.Ob → Y.Ob
+    reflect-open : ∀ {U} → Y.is-open U → X.is-open (λ x → U (hom x))
+
+open Continuous
+```
+
+<!--
+```agda
+unquoteDecl H-Level-Continuous = declare-record-hlevel 2 H-Level-Continuous (quote Continuous)
+
+instance
+  Funlike-Continuous : Funlike (Continuous X Y) ⌞ X ⌟ λ _ → ⌞ Y ⌟
+  Funlike-Continuous = record { _#_ = hom }
+
+Continuous-pathp
+  : ∀ {o ℓ o' ℓ'} {P : I → Topological-space o ℓ} {Q : I → Topological-space o' ℓ'}
+  → {f : Continuous (P i0) (Q i0)} {g : Continuous (P i1) (Q i1)}
+  → PathP (λ i → ⌞ P i ⌟ → ⌞ Q i ⌟) (apply f) (apply g)
+  → PathP (λ i → Continuous (P i) (Q i)) f g
+Continuous-pathp q i .hom a = q i a
+Continuous-pathp {P = P} {Q} {f} {g} q i .Continuous.reflect-open {U} U-open =
+  is-prop→pathp
+    (λ i →
+      Π-is-hlevel' {A = ⌞ Q i ⌟ → Ω} {B = λ U → Q.is-open i U → P.is-open i λ x → U (q i x)} 1 λ _ →
+      Π-is-hlevel 1 λ _ → P.is-open-is-prop i)
+    (λ U-open → f .reflect-open U-open)
+    (λ U-open → g .reflect-open U-open)
+    i U-open
+  where
+    module P i = Topological-space (P i)
+    module Q i = Topological-space (Q i)
+
+instance
+  Extensional-Continuous
+    : ∀ {o ℓ o' ℓ' ℓr} {P : Topological-space o ℓ} {Q : Topological-space o' ℓ'}
+    → ⦃ sa : Extensional (⌞ P ⌟ → ⌞ Q ⌟) ℓr ⦄
+    → Extensional (Continuous P Q) ℓr
+  Extensional-Continuous {Q = Q} ⦃ sa ⦄ =
+    injection→extensional! Continuous-pathp sa
+
+```
+-->
+
+```agda
+idᶜ : Continuous X X
+idᶜ .hom x = x
+idᶜ .reflect-open U-open = U-open
+
+_∘ᶜ_ : Continuous Y Z → Continuous X Y → Continuous X Z
+(f ∘ᶜ g) .hom x = f # (g # x)
+(f ∘ᶜ g) .reflect-open U-open = g .reflect-open (f .reflect-open U-open)
+
+Top : ∀ (o ℓ : Level) → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ)
+Top o ℓ .Precategory.Ob = Topological-space o ℓ
+Top o ℓ .Precategory.Hom = Continuous
+Top o ℓ .Precategory.Hom-set _ _ = hlevel 2
+Top o ℓ .Precategory.id = idᶜ
+Top o ℓ .Precategory._∘_ = _∘ᶜ_
+Top o ℓ .Precategory.idr _ = trivial!
+Top o ℓ .Precategory.idl _ = trivial!
+Top o ℓ .Precategory.assoc _ _ _ = trivial!
+```

From 4ee860eb29c86daf2d8f163b8f84a0bd84636fee Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sun, 30 Jun 2024 19:23:24 -0400
Subject: [PATCH 2/9] wip: some junk

---
 src/1Lab/Function/Embedding.lagda.md |  8 +++
 src/Data/Power.lagda.md              |  6 ++
 src/Topology/Base.lagda.md           | 97 ++++++++++++++++++++++++++--
 3 files changed, 107 insertions(+), 4 deletions(-)

diff --git a/src/1Lab/Function/Embedding.lagda.md b/src/1Lab/Function/Embedding.lagda.md
index a7a19a19d..831dc6006 100644
--- a/src/1Lab/Function/Embedding.lagda.md
+++ b/src/1Lab/Function/Embedding.lagda.md
@@ -173,6 +173,14 @@ 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)
+
 right-inverse→injective
   : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
   → {f : A → B} (g : B → A)
diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md
index d19d9e3cc..5404e84bb 100644
--- a/src/Data/Power.lagda.md
+++ b/src/Data/Power.lagda.md
@@ -110,5 +110,11 @@ infixr 31 _∪_
 ```agda
 ⋃ : ∀ {κ : Level} {I : Type κ} → (I → ℙ X) → ℙ X
 ⋃ {I = I} A x = ∃Ω[ i ∈ I ] A i x
+
+⋂ : ∀ {κ : Level} {I : Type κ} → (I → ℙ X) → ℙ X
+⋂ {I = I} A x = ∀Ω[ i ∈ I ] A i x
+
+_ᶜ : ℙ X → ℙ X
+(A ᶜ) x = ¬Ω (A x)
 ```
 -->
diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
index e0e0b92bf..6b168bcd5 100644
--- a/src/Topology/Base.lagda.md
+++ b/src/Topology/Base.lagda.md
@@ -4,19 +4,33 @@ description: |
 ---
 <!--
 ```agda
+open import Cat.Functor.Properties
+open import Cat.Functor.Morphism
 open import Cat.Prelude
 
+open import Data.Set.Surjection
+open import Data.Sum
 open import Data.Power
 
-open import 1Lab.Reflection hiding (absurd)
+import Cat.Reasoning
+
+open import 1Lab.Reflection hiding (absurd; [_])
 ```
 -->
 ```agda
 module Topology.Base where
 ```
 
+# Topological spaces {defines="topology topological-space open-set"}
+
+
 ```agda
-record is-topology {o ℓ} (X : Type o) (is-open : (X → Ω) → Type ℓ) : Type (lsuc o ⊔ ℓ) where
+record is-topology
+  {o ℓ}
+  (X : Type o)
+  (is-open : (X → Ω) → Type ℓ)
+  : Type (lsuc o ⊔ ℓ) where
+  no-eta-equality
   field
     ∩-open : ∀ {U V : X → Ω} → is-open U → is-open V → is-open (U ∩ V)
     ⋃-open : {I : Type o} → (Uᵢ : I → X → Ω) → (∀ i → is-open (Uᵢ i)) → is-open (⋃ Uᵢ)
@@ -24,10 +38,20 @@ record is-topology {o ℓ} (X : Type o) (is-open : (X → Ω) → Type ℓ) : Ty
     has-is-set : is-set X
     is-open-is-prop : ∀ {U} → is-prop (is-open U)
 
+  open-ext
+    : ∀ {U V : X → Ω}
+    → (∀ x → x ∈ U → x ∈ V)
+    → (∀ x → x ∈ V → x ∈ U)
+    → is-open U
+    → is-open V
+  open-ext to from U-open =
+    subst is-open (ext λ x → Ω-ua (to x) (from x)) U-open
+
   minimal-open : is-open minimal
   minimal-open =
-    subst is-open
-      (ext (λ _ → Ω-ua (rec! (λ ff tt → ff)) λ ff → inc (lift ff , tt)))
+    open-ext
+      (rec! (λ x ff tt → ff))
+      (λ x ff → inc (lift ff , tt))
       (⋃-open {I = Lift _ ⊥} (λ _ _ → ⊤Ω) (λ ff → absurd (Lift.lower ff)))
 
 record Topological-space (o ℓ : Level) : Type (lsuc o ⊔ lsuc ℓ) where
@@ -37,8 +61,39 @@ record Topological-space (o ℓ : Level) : Type (lsuc o ⊔ lsuc ℓ) where
     has-is-topology : is-topology Ob is-open
 
   open is-topology has-is-topology public
+
+  is-closed : ℙ Ob → Type _
+  is-closed U = is-open (U ᶜ)
+
+  ∪-closed : ∀ {U V} → is-closed U → is-closed V → is-closed (U ∪ V)
+  ∪-closed U-closed V-closed =
+    open-ext
+      (λ x (¬U , ¬V) → rec! [ ¬U , ¬V ])
+      (λ x ¬U+V → (λ u → ¬U+V (inc (inl u))) , (λ v → ¬U+V (inc (inr v))))
+      (∩-open U-closed V-closed)
+
+  minimal-closed : is-closed minimal
+  minimal-closed =
+    open-ext
+      (λ x tt ff → ff)
+      (λ x ff→ff → tt)
+      maximal-open
+
+  maximal-closed : is-closed maximal
+  maximal-closed =
+    open-ext
+      (λ x ff tt → ff)
+      (λ x tt→ff → tt→ff tt)
+      minimal-open
 ```
 
+<!--
+```agda
+  is-neighborhood : (x : Ob) → (U : Ob → Ω) → Type _
+  is-neighborhood x U = ∃[ O ∈ (Ob → Ω) ] (O ⊆ U × is-open O)
+```
+-->
+
 <!--
 ```agda
 private variable
@@ -139,3 +194,37 @@ Top o ℓ .Precategory.idr _ = trivial!
 Top o ℓ .Precategory.idl _ = trivial!
 Top o ℓ .Precategory.assoc _ _ _ = trivial!
 ```
+
+```agda
+Top↪Sets : Functor (Top o ℓ) (Sets o)
+Top↪Sets .Functor.F₀ X .∣_∣ = ⌞ X ⌟
+Top↪Sets .Functor.F₀ X .is-tr = hlevel 2
+Top↪Sets .Functor.F₁ = hom
+Top↪Sets .Functor.F-id = refl
+Top↪Sets .Functor.F-∘ _ _ = refl
+
+Top↪Sets-is-faithful : is-faithful (Top↪Sets {o} {ℓ})
+Top↪Sets-is-faithful p = ext (apply p)
+
+module Top {o ℓ} = Cat.Reasoning (Top o ℓ)
+```
+
+```agda
+continuous-injection→monic
+  : {X Y : Topological-space o ℓ}
+  → (f : Continuous X Y)
+  → injective (f .hom)
+  → Top.is-monic f
+continuous-injection→monic f f-inj =
+  faithful→reflects-mono Top↪Sets Top↪Sets-is-faithful $ λ {Z} →
+  injective→monic (hlevel 2) f-inj {Z}
+
+continuous-surjection→epic
+  : {X Y : Topological-space o ℓ}
+  → (f : Continuous X Y)
+  → is-surjective (f .hom)
+  → Top.is-epic f
+continuous-surjection→epic {X = X} {Y = Y} f f-surj =
+  faithful→reflects-epi Top↪Sets Top↪Sets-is-faithful $ λ {Z} →
+  surjective→epi (el! ⌞ X ⌟) (el! ⌞ Y ⌟) (f .hom) f-surj {Z}
+```

From 486544f7ac3c684be8720bd25c72794551980213 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sun, 30 Jun 2024 19:24:01 -0400
Subject: [PATCH 3/9] wip: hausdorff spaces

---
 src/Topology/Hausdorff.lagda.md | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 src/Topology/Hausdorff.lagda.md

diff --git a/src/Topology/Hausdorff.lagda.md b/src/Topology/Hausdorff.lagda.md
new file mode 100644
index 000000000..b460b6af6
--- /dev/null
+++ b/src/Topology/Hausdorff.lagda.md
@@ -0,0 +1,24 @@
+---
+description: |
+  Hausdorff spaces.
+---
+<!--
+```agda
+open import Cat.Prelude
+
+open import Topology.Base
+```
+-->
+```agda
+module Topology.Hausdorff where
+```
+
+```agda
+record is-hausdorff {o ℓ} (X : Topological-space o ℓ) : Type (o ⊔ ℓ) where
+  open Topological-space X
+  field
+    cool
+      : ∀ (x y : ⌞ X ⌟)
+      → (∀ (U V : ⌞ X ⌟ → Ω) → is-neighborhood x U → is-neighborhood y V → ∃[ z ∈ ⌞ X ⌟ ] (z ∈ U × z ∈ V))
+      → x ≡ y
+```

From 652466a14b9ee8d43f23f2e66e6f3e0661444bb6 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sat, 3 Aug 2024 12:09:06 -0700
Subject: [PATCH 4/9] wip: rework how topologies are defined

---
 src/Data/Power.lagda.md    |  55 ++++++-
 src/Topology/Base.lagda.md | 314 ++++++++++++++++++++-----------------
 2 files changed, 219 insertions(+), 150 deletions(-)

diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md
index 5404e84bb..9cd70a3e8 100644
--- a/src/Data/Power.lagda.md
+++ b/src/Data/Power.lagda.md
@@ -14,7 +14,7 @@ module Data.Power where
 ```agda
 private variable
   ℓ : Level
-  X : Type ℓ
+  X Y : Type ℓ
 ```
 -->
 
@@ -106,15 +106,66 @@ 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
+```
+
+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ᵢ =
+  funext λ x →
+  Ω-ua
+    (rec! λ A i Aᵢ=A x∈A → pure (i , (subst (λ A → ∣ A x ∣) (sym Aᵢ=A) x∈A)))
+    (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 _ =
+  funext λ x →
+    Ω-ua
+      (rec! λ ff x∈A → ff)
+      (λ ff → absurd ff)
+```
+
+
+<!--
+```agda
 ⋂ : ∀ {κ : Level} {I : Type κ} → (I → ℙ X) → ℙ X
 ⋂ {I = I} A x = ∀Ω[ i ∈ I ] A i x
 
 _ᶜ : ℙ X → ℙ X
 (A ᶜ) x = ¬Ω (A x)
+
+Preimage : (X → Y) → ℙ Y → ℙ X
+Preimage f A = A ∘ f
+
+Direct-image : (X → Y) → ℙ X → ℙ Y
+Direct-image {X = X} f A y = elΩ (Σ[ x ∈ X ] (x ∈ A × (f x ≡ y)))
+
+direct-preimage
+  : ∀ {f : X → Y}
+  → ∀ (U : ℙ Y)
+  → Direct-image f (Preimage f U) ⊆ U
+direct-preimage {f = f} U y =
+  rec! λ x fx∈U p → subst (λ x → ∣ U x ∣) p fx∈U
 ```
 -->
diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
index 6b168bcd5..67f39131b 100644
--- a/src/Topology/Base.lagda.md
+++ b/src/Topology/Base.lagda.md
@@ -4,6 +4,7 @@ description: |
 ---
 <!--
 ```agda
+open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Properties
 open import Cat.Functor.Morphism
 open import Cat.Prelude
@@ -23,208 +24,225 @@ module Topology.Base where
 
 # Topological spaces {defines="topology topological-space open-set"}
 
+A **topology** on a type $X$ consists of a subset $\mathcal{O}$ of the [[power set]]
+of $X$ that is closed under finite intersections and infinitary unions.
+The elements of $\mathcal{O}$ are known as **open sets**,
+and a set equipped with a topology is called a **topological space**
 
-```agda
-record is-topology
-  {o ℓ}
-  (X : Type o)
-  (is-open : (X → Ω) → Type ℓ)
-  : Type (lsuc o ⊔ ℓ) where
-  no-eta-equality
-  field
-    ∩-open : ∀ {U V : X → Ω} → is-open U → is-open V → is-open (U ∩ V)
-    ⋃-open : {I : Type o} → (Uᵢ : I → X → Ω) → (∀ i → is-open (Uᵢ i)) → is-open (⋃ Uᵢ)
-    maximal-open : is-open maximal
-    has-is-set : is-set X
-    is-open-is-prop : ∀ {U} → is-prop (is-open U)
-
-  open-ext
-    : ∀ {U V : X → Ω}
-    → (∀ x → x ∈ U → x ∈ V)
-    → (∀ x → x ∈ V → x ∈ U)
-    → is-open U
-    → is-open V
-  open-ext to from U-open =
-    subst is-open (ext λ x → Ω-ua (to x) (from x)) U-open
+Topological spaces allow us to study geometric ideas like continuity,
+convergence, etc. within a relatively abstract framework, and are a
+pillar of modern classical mathematics. However, they tend to be rather
+ill-behaved constructively, and provide a rich source of constructive
+taboos.
 
-  minimal-open : is-open minimal
-  minimal-open =
-    open-ext
-      (rec! (λ x ff tt → ff))
-      (λ x ff → inc (lift ff , tt))
-      (⋃-open {I = Lift _ ⊥} (λ _ _ → ⊤Ω) (λ ff → absurd (Lift.lower ff)))
+With that small bit of motivation out of the way, we can proceed to
+give a formal definition of a topology.
 
-record Topological-space (o ℓ : Level) : Type (lsuc o ⊔ lsuc ℓ) where
+```agda
+record Topology-on {ℓ} (X : Type ℓ) : Type ℓ where
+  no-eta-equality
   field
-    Ob : Type o
-    is-open : (Ob → Ω) → Type ℓ
-    has-is-topology : is-topology Ob is-open
-
-  open is-topology has-is-topology public
+    Opens : ℙ (ℙ X)
+```
 
-  is-closed : ℙ Ob → Type _
-  is-closed U = is-open (U ᶜ)
+We ensure that the set of opens is closed under finite intersections
+by requiring that the entirety of $X$ is open, along with closure
+under binary intersections.
 
-  ∪-closed : ∀ {U V} → is-closed U → is-closed V → is-closed (U ∪ V)
-  ∪-closed U-closed V-closed =
-    open-ext
-      (λ x (¬U , ¬V) → rec! [ ¬U , ¬V ])
-      (λ x ¬U+V → (λ u → ¬U+V (inc (inl u))) , (λ v → ¬U+V (inc (inr v))))
-      (∩-open U-closed V-closed)
+```agda
+    maximal-open : maximal ∈ Opens
+    ∩-open : ∀ {U V : ℙ X} → U ∈ Opens → V ∈ Opens → (U ∩ V) ∈ Opens
+```
 
-  minimal-closed : is-closed minimal
-  minimal-closed =
-    open-ext
-      (λ x tt ff → ff)
-      (λ x ff→ff → tt)
-      maximal-open
+Instead of closure under infinitary unions $\bigcup_{i : I} U_i$, we
+require that the set of opens is closed under unions of subsets. This
+allows us to avoid a bump in universe level, as we do not need to quantify
+over any types!
 
-  maximal-closed : is-closed maximal
-  maximal-closed =
-    open-ext
-      (λ x ff tt → ff)
-      (λ x tt→ff → tt→ff tt)
-      minimal-open
+```agda
+    ⋃ˢ-open : ∀ (S : ℙ (ℙ X)) → S ⊆ Opens → ⋃ˢ S ∈ Opens
 ```
 
 <!--
 ```agda
-  is-neighborhood : (x : Ob) → (U : Ob → Ω) → Type _
-  is-neighborhood x U = ∃[ O ∈ (Ob → Ω) ] (O ⊆ U × is-open O)
+  is-open : ℙ X → Type
+  is-open X = ∣ Opens X ∣
+
+  open-ext
+    : ∀ {U V : ℙ X}
+    → (∀ (x : X) → x ∈ U → x ∈ V)
+    → (∀ (x : X) → x ∈ V → x ∈ U)
+    → U ∈ Opens
+    → V ∈ Opens
+  open-ext to from U-open =
+    subst is-open (ext λ x → Ω-ua (to x) (from x)) U-open
 ```
 -->
 
-<!--
+Next, we will show that open sets are closed under indexed unions.
+Let $U_i$ be a family of open sets indexed by an arbitrary type $I$.
+Note that if $U$ is in the fibre of $U_i$, then $U$ is open. Moreover,
+the set of fibres of $U_i$ forms a subset of the powerset, so its
+union is also open. Finally, the union of the fibres of $U_i$ is equal
+to the union of $U_i$, so $\bigcup_{I} U_i$ is open.
+
 ```agda
-private variable
-  o ℓ o' ℓ' : Level
-  X Y Z : Topological-space o ℓ
+  fibre-open
+    : ∀ {κ} {I : Type κ}
+    → (Uᵢ : I → ℙ X) → (∀ i → Uᵢ i ∈ Opens)
+    → ∀ (U : ℙ X) → □ (fibre Uᵢ U) → U ∈ Opens
+  fibre-open Uᵢ Uᵢ-open U = rec! λ i Uᵢ=U →
+    subst is-open Uᵢ=U (Uᵢ-open i)
+
+  ⋃-open
+    : ∀ {κ} {I : Type κ}
+    → (Uᵢ : I → ℙ X) → (∀ i → Uᵢ i ∈ Opens)
+    → ⋃ Uᵢ ∈ Opens
+  ⋃-open {I = I} Uᵢ Uᵢ-open =
+    subst is-open
+      (⋃-fibre Uᵢ)
+      (⋃ˢ-open (λ U → elΩ (fibre Uᵢ U)) (fibre-open Uᵢ Uᵢ-open))
+```
 
-instance
-  Underlying-Topological-space : ∀ {o ℓ} → Underlying (Topological-space o ℓ)
-  Underlying-Topological-space .Underlying.ℓ-underlying = _
-  Underlying-Topological-space .Underlying.⌞_⌟ = Topological-space.Ob
+As an easy corollary, the empty set is also open.
 
-  open hlevel-projection
+```agda
+  minimal-open : minimal ∈ Opens
+  minimal-open =
+    subst is-open
+      (⋃-minimal (λ _ → maximal))
+      (⋃-open (λ _ → maximal) (λ _ → maximal-open))
+```
 
-  Topological-space-ob-hlevel-proj : hlevel-projection (quote Topological-space.Ob)
-  Topological-space-ob-hlevel-proj .has-level   = quote Topological-space.has-is-set
-  Topological-space-ob-hlevel-proj .get-level _ = pure (lit (nat 2))
-  Topological-space-ob-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
-  Topological-space-ob-hlevel-proj .get-argument _                     = typeError []
+We pause to note that paths between topologies are relatively easy to
+characterise: if two topologies on $X$ have the same sets of opens, then
+the two topologies are equal!
 
-  Topological-space-open-hlevel-proj : hlevel-projection (quote Topological-space.is-open)
-  Topological-space-open-hlevel-proj .has-level   = quote Topological-space.is-open-is-prop
-  Topological-space-open-hlevel-proj .get-level _ = pure (lit (nat 1))
-  Topological-space-open-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
-  Topological-space-open-hlevel-proj .get-argument _                     = typeError []
+```agda
+Topology-on-path
+  : ∀ {ℓ} {X : Type ℓ}
+  → {S T : Topology-on X}
+  → (Topology-on.Opens S ⊆ Topology-on.Opens T)
+  → (Topology-on.Opens T ⊆ Topology-on.Opens S)
+  → S ≡ T
+```
 
+<details>
+<summary>The proof is somewhat tedious, but the key observation is that
+the sets of opens are the only non-propositional piece of data in a
+topology.
+</summary>
+```agda
+Topology-on-path {X = X} {S = S} {T = T} to from = path where
+  module S = Topology-on S
+  module T = Topology-on T
+
+
+  opens : S.Opens ≡ T.Opens
+  opens = funext λ U → Ω-ua (to U) (from U)
+
+  path : S ≡ T
+  path i .Topology-on.Opens = opens i
+  path i .Topology-on.maximal-open =
+    is-prop→pathp (λ i → opens i maximal .is-tr)
+      S.maximal-open
+      T.maximal-open i
+  path i .Topology-on.∩-open {U} {V} =
+    is-prop→pathp
+      (λ i →
+        Π-is-hlevel² {A = U ∈ opens i} {B = λ _ → V ∈ opens i} 1 λ _ _ →
+        opens i (U ∩ V) .is-tr)
+      S.∩-open
+      T.∩-open i
+  path i .Topology-on.⋃ˢ-open S =
+    is-prop→pathp
+      (λ i →
+        Π-is-hlevel {A = S ⊆ opens i} 1 λ _ →
+        opens i (⋃ˢ S) .is-tr)
+      (S.⋃ˢ-open S)
+      (T.⋃ˢ-open S) i
 ```
--->
+</details>
+
+
+# Continuous Maps
 
 ```agda
-record Continuous
-  {o ℓ o' ℓ'}
-  (X : Topological-space o ℓ) (Y : Topological-space o' ℓ')
-  : Type (o ⊔ o' ⊔ ℓ ⊔ ℓ') where
+record is-continuous
+  {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'}
+  (f : X → Y)
+  (X-top : Topology-on X) (Y-top : Topology-on Y)
+  : Type ℓ'
+  where
   no-eta-equality
   private
-    module X = Topological-space X
-    module Y = Topological-space Y
+    module X = Topology-on X-top
+    module Y = Topology-on Y-top
   field
-    hom : X.Ob → Y.Ob
-    reflect-open : ∀ {U} → Y.is-open U → X.is-open (λ x → U (hom x))
+      reflect-open : ∀ {U : ℙ Y} → U ∈ Y.Opens → Preimage f U ∈ X.Opens
 
-open Continuous
 ```
 
 <!--
 ```agda
-unquoteDecl H-Level-Continuous = declare-record-hlevel 2 H-Level-Continuous (quote Continuous)
-
-instance
-  Funlike-Continuous : Funlike (Continuous X Y) ⌞ X ⌟ λ _ → ⌞ Y ⌟
-  Funlike-Continuous = record { _#_ = hom }
-
-Continuous-pathp
-  : ∀ {o ℓ o' ℓ'} {P : I → Topological-space o ℓ} {Q : I → Topological-space o' ℓ'}
-  → {f : Continuous (P i0) (Q i0)} {g : Continuous (P i1) (Q i1)}
-  → PathP (λ i → ⌞ P i ⌟ → ⌞ Q i ⌟) (apply f) (apply g)
-  → PathP (λ i → Continuous (P i) (Q i)) f g
-Continuous-pathp q i .hom a = q i a
-Continuous-pathp {P = P} {Q} {f} {g} q i .Continuous.reflect-open {U} U-open =
-  is-prop→pathp
-    (λ i →
-      Π-is-hlevel' {A = ⌞ Q i ⌟ → Ω} {B = λ U → Q.is-open i U → P.is-open i λ x → U (q i x)} 1 λ _ →
-      Π-is-hlevel 1 λ _ → P.is-open-is-prop i)
-    (λ U-open → f .reflect-open U-open)
-    (λ U-open → g .reflect-open U-open)
-    i U-open
-  where
-    module P i = Topological-space (P i)
-    module Q i = Topological-space (Q i)
-
-instance
-  Extensional-Continuous
-    : ∀ {o ℓ o' ℓ' ℓr} {P : Topological-space o ℓ} {Q : Topological-space o' ℓ'}
-    → ⦃ sa : Extensional (⌞ P ⌟ → ⌞ Q ⌟) ℓr ⦄
-    → Extensional (Continuous P Q) ℓr
-  Extensional-Continuous {Q = Q} ⦃ sa ⦄ =
-    injection→extensional! Continuous-pathp sa
+open is-continuous
 
+unquoteDecl H-Level-is-continuous = declare-record-hlevel 1 H-Level-is-continuous (quote is-continuous)
 ```
 -->
 
+# The category of topological spaces
+
 ```agda
-idᶜ : Continuous X X
-idᶜ .hom x = x
-idᶜ .reflect-open U-open = U-open
+Topology-structure : ∀ ℓ → Thin-structure ℓ (Topology-on {ℓ})
+Topology-structure ℓ .is-hom f X-top Y-top =
+  el! (is-continuous f X-top Y-top)
+Topology-structure ℓ .id-is-hom .reflect-open U-open = U-open
+Topology-structure ℓ .∘-is-hom f g f-cont g-cont .reflect-open =
+  g-cont .reflect-open ⊙ f-cont .reflect-open
+Topology-structure ℓ .id-hom-unique p q =
+  Topology-on-path (λ U → q .reflect-open) (λ U → p .reflect-open)
+```
+
+```agda
+Topologies : ∀ ℓ → Precategory (lsuc ℓ) (ℓ ⊔ ℓ)
+Topologies ℓ = Structured-objects (Topology-structure ℓ)
 
-_∘ᶜ_ : Continuous Y Z → Continuous X Y → Continuous X Z
-(f ∘ᶜ g) .hom x = f # (g # x)
-(f ∘ᶜ g) .reflect-open U-open = g .reflect-open (f .reflect-open U-open)
+module Topologies {ℓ} = Cat.Reasoning (Topologies ℓ)
 
-Top : ∀ (o ℓ : Level) → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ)
-Top o ℓ .Precategory.Ob = Topological-space o ℓ
-Top o ℓ .Precategory.Hom = Continuous
-Top o ℓ .Precategory.Hom-set _ _ = hlevel 2
-Top o ℓ .Precategory.id = idᶜ
-Top o ℓ .Precategory._∘_ = _∘ᶜ_
-Top o ℓ .Precategory.idr _ = trivial!
-Top o ℓ .Precategory.idl _ = trivial!
-Top o ℓ .Precategory.assoc _ _ _ = trivial!
+Topological-space : ∀ ℓ → Type (lsuc ℓ)
+Topological-space ℓ = Topologies.Ob {ℓ}
 ```
 
 ```agda
-Top↪Sets : Functor (Top o ℓ) (Sets o)
-Top↪Sets .Functor.F₀ X .∣_∣ = ⌞ X ⌟
-Top↪Sets .Functor.F₀ X .is-tr = hlevel 2
-Top↪Sets .Functor.F₁ = hom
-Top↪Sets .Functor.F-id = refl
-Top↪Sets .Functor.F-∘ _ _ = refl
+Topologies↪Sets : ∀ {ℓ} → Functor (Topologies ℓ) (Sets ℓ)
+Topologies↪Sets = Forget-structure (Topology-structure _)
 
-Top↪Sets-is-faithful : is-faithful (Top↪Sets {o} {ℓ})
-Top↪Sets-is-faithful p = ext (apply p)
+Topologies↪Sets-faithful : ∀ {ℓ} → is-faithful (Topologies↪Sets {ℓ})
+Topologies↪Sets-faithful = Structured-hom-path (Topology-structure _)
+```
 
-module Top {o ℓ} = Cat.Reasoning (Top o ℓ)
+```agda
+Topologies-is-category : ∀ {ℓ} → is-category (Topologies ℓ)
+Topologies-is-category = Structured-objects-is-category (Topology-structure _)
 ```
 
 ```agda
 continuous-injection→monic
-  : {X Y : Topological-space o ℓ}
-  → (f : Continuous X Y)
+  : ∀ {ℓ} {X Y : Topological-space ℓ}
+  → (f : Topologies.Hom X Y)
   → injective (f .hom)
-  → Top.is-monic f
+  → Topologies.is-monic f
 continuous-injection→monic f f-inj =
-  faithful→reflects-mono Top↪Sets Top↪Sets-is-faithful $ λ {Z} →
+  faithful→reflects-mono Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
   injective→monic (hlevel 2) f-inj {Z}
 
 continuous-surjection→epic
-  : {X Y : Topological-space o ℓ}
-  → (f : Continuous X Y)
+  : ∀ {ℓ} {X Y : Topological-space ℓ}
+  → (f : Topologies.Hom X Y)
   → is-surjective (f .hom)
-  → Top.is-epic f
+  → Topologies.is-epic f
 continuous-surjection→epic {X = X} {Y = Y} f f-surj =
-  faithful→reflects-epi Top↪Sets Top↪Sets-is-faithful $ λ {Z} →
+  faithful→reflects-epi Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
   surjective→epi (el! ⌞ X ⌟) (el! ⌞ Y ⌟) (f .hom) f-surj {Z}
 ```

From d434e0ffb2bf77f8a76c43c286353b39a6d82f9d Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Mon, 5 Aug 2024 11:42:19 -0700
Subject: [PATCH 5/9] wip: induced topologies

---
 src/Data/Power.lagda.md                 | 127 ++++++++++++++++++++----
 src/Topology/Base.lagda.md              |  13 ++-
 src/Topology/Instances/Induced.lagda.md |  99 ++++++++++++++++++
 src/Topology/Instances/Product.lagda.md |  23 +++++
 src/preamble.tex                        |   1 +
 5 files changed, 240 insertions(+), 23 deletions(-)
 create mode 100644 src/Topology/Instances/Induced.lagda.md
 create mode 100644 src/Topology/Instances/Product.lagda.md

diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md
index 9cd70a3e8..5ffd284ab 100644
--- a/src/Data/Power.lagda.md
+++ b/src/Data/Power.lagda.md
@@ -13,7 +13,7 @@ module Data.Power where
 <!--
 ```agda
 private variable
-  ℓ : Level
+  ℓ ℓ' : Level
   X Y : Type ℓ
 ```
 -->
@@ -82,6 +82,17 @@ _∩_ : ℙ 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)
+```
+-->
+
 <!--
 ```agda
 _ = ∥_∥
@@ -117,6 +128,48 @@ as unions of subsets of the power set.
 ⋃ˢ {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$.
 
@@ -126,10 +179,9 @@ of the fibres of $A_i$.
   → (Aᵢ : I → ℙ X)
   → ⋃ˢ (λ A → elΩ (fibre Aᵢ A)) ≡ ⋃ Aᵢ
 ⋃-fibre Aᵢ =
-  funext λ x →
-  Ω-ua
-    (rec! λ A i Aᵢ=A x∈A → pure (i , (subst (λ A → ∣ A x ∣) (sym Aᵢ=A) x∈A)))
-    (rec! λ i x∈Aᵢ → pure ((Aᵢ i , pure (i , refl)) , x∈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
@@ -140,12 +192,49 @@ set.
   : (A : ⊥ → ℙ X)
   → ⋃ {I = ⊥} A ≡ minimal
 ⋃-minimal _ =
-  funext λ x →
-    Ω-ua
-      (rec! λ ff x∈A → ff)
-      (λ ff → absurd ff)
+  ℙ-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
@@ -155,17 +244,15 @@ set.
 _ᶜ : ℙ X → ℙ X
 (A ᶜ) x = ¬Ω (A x)
 
-Preimage : (X → Y) → ℙ Y → ℙ X
-Preimage f A = A ∘ f
+≡→⊆
+  : ∀ {U V : ℙ X}
+  → U ≡ V → U ⊆ V
+≡→⊆ {V = V} p x x∈U =
+  subst (λ U → ∣ U x ∣) p x∈U
 
-Direct-image : (X → Y) → ℙ X → ℙ Y
-Direct-image {X = X} f A y = elΩ (Σ[ x ∈ X ] (x ∈ A × (f x ≡ y)))
-
-direct-preimage
-  : ∀ {f : X → Y}
-  → ∀ (U : ℙ Y)
-  → Direct-image f (Preimage f U) ⊆ U
-direct-preimage {f = f} U y =
-  rec! λ x fx∈U p → subst (λ x → ∣ U x ∣) p fx∈U
+≡→⊇
+  : ∀ {U V : ℙ X}
+  → U ≡ V → V ⊆ U
+≡→⊇ p = ≡→⊆ (sym p)
 ```
 -->
diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
index 67f39131b..748d759ce 100644
--- a/src/Topology/Base.lagda.md
+++ b/src/Topology/Base.lagda.md
@@ -165,7 +165,12 @@ Topology-on-path {X = X} {S = S} {T = T} to from = path where
 </details>
 
 
-# Continuous Maps
+# Continuous functions {defines="continuous-function"}
+
+A function $f : X \to Y$ between two topological spaces is **continuous**
+if it reflects open sets. Explicitly, $f$ is continuous if, for every
+open set $U : \power{Y}$, the preimage $f^{-1}(U) : \power{X}$ is open
+in $X$.
 
 ```agda
 record is-continuous
@@ -179,8 +184,7 @@ record is-continuous
     module X = Topology-on X-top
     module Y = Topology-on Y-top
   field
-      reflect-open : ∀ {U : ℙ Y} → U ∈ Y.Opens → Preimage f U ∈ X.Opens
-
+    reflect-open : ∀ {U : ℙ Y} → U ∈ Y.Opens → Preimage f U ∈ X.Opens
 ```
 
 <!--
@@ -208,6 +212,9 @@ Topology-structure ℓ .id-hom-unique p q =
 Topologies : ∀ ℓ → Precategory (lsuc ℓ) (ℓ ⊔ ℓ)
 Topologies ℓ = Structured-objects (Topology-structure ℓ)
 
+Topologies-on : ∀ ℓ → Displayed (Sets ℓ) ℓ ℓ
+Topologies-on ℓ = Thin-structure-over (Topology-structure ℓ)
+
 module Topologies {ℓ} = Cat.Reasoning (Topologies ℓ)
 
 Topological-space : ∀ ℓ → Type (lsuc ℓ)
diff --git a/src/Topology/Instances/Induced.lagda.md b/src/Topology/Instances/Induced.lagda.md
new file mode 100644
index 000000000..c5322cb76
--- /dev/null
+++ b/src/Topology/Instances/Induced.lagda.md
@@ -0,0 +1,99 @@
+---
+description: |
+  Induced topologies
+---
+<!--
+```agda
+open import Cat.Displayed.Cartesian
+open import Cat.Prelude
+
+open import Data.Power
+
+open import Topology.Base
+```
+-->
+```agda
+module Topology.Instances.Induced where
+```
+
+# Induced topologies
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+
+open Topology-on
+open is-continuous
+```
+-->
+
+```agda
+Induced
+  : ∀ {X : Type ℓ} {Y : Type ℓ'}
+  → (f : X → Y)
+  → Topology-on Y
+  → Topology-on X
+Induced {X = X} {Y = Y} f Y-top = X-top where
+  module Y = Topology-on Y-top
+
+  X-top : Topology-on X
+  X-top .Opens = Direct-image (Preimage f) Y.Opens
+  X-top .∩-open =
+    rec! λ U U-open U∈f⁻¹ V V-open V∈f⁻¹ →
+      pure $
+        U ∩ V ,
+        Y.∩-open U-open V-open ,
+        ap₂ _∩_ U∈f⁻¹ V∈f⁻¹
+  X-top .⋃ˢ-open S S⊆Opens =
+    pure $
+      ⋃ˢ S* ,
+      Y.⋃ˢ-open S* (λ V V-open → V-open .fst) ,
+      ℙ-ext S*-⊆ S*-⊇
+    where
+      S* : ℙ (ℙ Y)
+      S* = Y.Opens ∩ Preimage (Preimage f) S
+
+      S*-⊆ : Preimage f (⋃ˢ S*) ⊆ ⋃ˢ S
+      S*-⊆ =
+        ⋃-⊆ (λ U → Preimage f (U .fst)) (⋃ˢ S) λ (V , V∈S*) →
+        ⋃ˢ-inc S (Preimage f V) (V∈S* .snd)
+
+      S*-⊇ : ⋃ˢ S ⊆ Preimage f (⋃ˢ S*)
+      S*-⊇ =
+        ⋃ˢ-⊆ S (Preimage f (⋃ˢ S*)) λ U U∈S →
+        rec! (λ V V-open f[V]=U x x∈U →
+          pure $
+            (V , (V-open , subst (λ A → ∣ S A ∣) (sym f[V]=U) U∈S)) ,
+            subst (λ A → ∣ A x ∣) (sym f[V]=U) x∈U)
+          (S⊆Opens U U∈S)
+  X-top .maximal-open =
+    pure (maximal , Y.maximal-open , refl)
+```
+
+```agda
+induced-continuous
+  : ∀ {X : Type ℓ} {Y : Type ℓ'} {f : X → Y}
+  → {Y-top : Topology-on Y}
+  → is-continuous f (Induced f Y-top) Y-top
+induced-continuous .reflect-open {U = U} U-open =
+  pure (U , U-open , refl)
+```
+
+```agda
+Topologies-fibration : ∀ {ℓ} → Cartesian-fibration (Topologies-on ℓ)
+Topologies-fibration {ℓ} .Cartesian-fibration.has-lift f Y-top = cart where
+  open Cartesian-lift
+  open is-cartesian
+
+  cart : Cartesian-lift (Topologies-on ℓ) f Y-top
+  cart .x' = Induced f Y-top
+  cart .lifting = induced-continuous
+  cart .cartesian .universal {u = Z} {u' = Z-top} g fg-cont .reflect-open {U = U} =
+    rec! λ V V-open f[V]=U →
+      subst (is-open Z-top)
+        (funext λ z → f[V]=U $ₚ g z)
+        (fg-cont .reflect-open V-open)
+  cart .cartesian .commutes _ _ = prop!
+  cart .cartesian .unique _ _ = prop!
+```
diff --git a/src/Topology/Instances/Product.lagda.md b/src/Topology/Instances/Product.lagda.md
new file mode 100644
index 000000000..62c18f911
--- /dev/null
+++ b/src/Topology/Instances/Product.lagda.md
@@ -0,0 +1,23 @@
+---
+description: |
+  Products of topological spaces.
+---
+<!--
+```agda
+open import Cat.Prelude
+
+open import Topology.Base
+```
+-->
+```agda
+module Topology.Instances.Product where
+```
+
+<!--
+```agda
+private variable
+  o ℓ o' ℓ' : Level
+
+open Topological-space
+```
+-->
diff --git a/src/preamble.tex b/src/preamble.tex
index 318c08561..754d26ad6 100644
--- a/src/preamble.tex
+++ b/src/preamble.tex
@@ -62,6 +62,7 @@
 \newcommand{\set}{\rm{Set}}
 \newcommand{\prop}{\rm{Prop}}
 \newcommand{\psh}{\rm{PSh}}
+\newcommand{\power}[1]{\mathcal{P}(#1)}
 
 \DeclareMathOperator{\Sh}{Sh}
 

From 6d27c355f55729207315ea7cce08df3f53267649 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 8 Aug 2024 11:14:40 -0700
Subject: [PATCH 6/9] wip: more stuff on topologies

---
 src/Cat/Displayed/Univalence/Thin.lagda.md |  2 +-
 src/Data/Power.lagda.md                    | 10 +++
 src/Topology/Base.lagda.md                 | 84 +++++++++++++++-------
 src/Topology/Instances/Discrete.lagda.md   | 80 +++++++++++++++++++++
 src/preamble.tex                           |  1 +
 5 files changed, 152 insertions(+), 25 deletions(-)
 create mode 100644 src/Topology/Instances/Discrete.lagda.md

diff --git a/src/Cat/Displayed/Univalence/Thin.lagda.md b/src/Cat/Displayed/Univalence/Thin.lagda.md
index bfa44ca44..1762af68a 100644
--- a/src/Cat/Displayed/Univalence/Thin.lagda.md
+++ b/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
diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md
index 5ffd284ab..7cf7a2592 100644
--- a/src/Data/Power.lagda.md
+++ b/src/Data/Power.lagda.md
@@ -90,6 +90,16 @@ _∩_ : ℙ X → ℙ X → ℙ X
   → 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
 ```
 -->
 
diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
index 748d759ce..4ba702a7e 100644
--- a/src/Topology/Base.lagda.md
+++ b/src/Topology/Base.lagda.md
@@ -168,8 +168,8 @@ Topology-on-path {X = X} {S = S} {T = T} to from = path where
 # Continuous functions {defines="continuous-function"}
 
 A function $f : X \to Y$ between two topological spaces is **continuous**
-if it reflects open sets. Explicitly, $f$ is continuous if, for every
-open set $U : \power{Y}$, the preimage $f^{-1}(U) : \power{X}$ is open
+if it reflects open sets. Explicitly, $f$ is continuous if for every
+open set $U : \power{Y}$, the [[preimage]] $f^{-1}(U) : \power{X}$ is open
 in $X$.
 
 ```agda
@@ -197,6 +197,9 @@ unquoteDecl H-Level-is-continuous = declare-record-hlevel 1 H-Level-is-continuou
 
 # The category of topological spaces
 
+Topological spaces and continuous maps form a category, which we will
+denote $\Top$.
+
 ```agda
 Topology-structure : ∀ ℓ → Thin-structure ℓ (Topology-on {ℓ})
 Topology-structure ℓ .is-hom f X-top Y-top =
@@ -206,20 +209,22 @@ Topology-structure ℓ .∘-is-hom f g f-cont g-cont .reflect-open =
   g-cont .reflect-open ⊙ f-cont .reflect-open
 Topology-structure ℓ .id-hom-unique p q =
   Topology-on-path (λ U → q .reflect-open) (λ U → p .reflect-open)
-```
 
-```agda
 Topologies : ∀ ℓ → Precategory (lsuc ℓ) (ℓ ⊔ ℓ)
 Topologies ℓ = Structured-objects (Topology-structure ℓ)
+```
 
-Topologies-on : ∀ ℓ → Displayed (Sets ℓ) ℓ ℓ
-Topologies-on ℓ = Thin-structure-over (Topology-structure ℓ)
-
+<!--
+```agda
 module Topologies {ℓ} = Cat.Reasoning (Topologies ℓ)
 
 Topological-space : ∀ ℓ → Type (lsuc ℓ)
 Topological-space ℓ = Topologies.Ob {ℓ}
 ```
+-->
+
+As $\Top$ is a category of [[thin structures]], it comes equipped with
+a forgetful functor into sets.
 
 ```agda
 Topologies↪Sets : ∀ {ℓ} → Functor (Topologies ℓ) (Sets ℓ)
@@ -229,27 +234,58 @@ Topologies↪Sets-faithful : ∀ {ℓ} → is-faithful (Topologies↪Sets {ℓ})
 Topologies↪Sets-faithful = Structured-hom-path (Topology-structure _)
 ```
 
+Additionally, $\Top$ is a [[univalent category]].
+
 ```agda
 Topologies-is-category : ∀ {ℓ} → is-category (Topologies ℓ)
 Topologies-is-category = Structured-objects-is-category (Topology-structure _)
 ```
 
+<!--
 ```agda
-continuous-injection→monic
-  : ∀ {ℓ} {X Y : Topological-space ℓ}
-  → (f : Topologies.Hom X Y)
-  → injective (f .hom)
-  → Topologies.is-monic f
-continuous-injection→monic f f-inj =
-  faithful→reflects-mono Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
-  injective→monic (hlevel 2) f-inj {Z}
-
-continuous-surjection→epic
-  : ∀ {ℓ} {X Y : Topological-space ℓ}
-  → (f : Topologies.Hom X Y)
-  → is-surjective (f .hom)
-  → Topologies.is-epic f
-continuous-surjection→epic {X = X} {Y = Y} f f-surj =
-  faithful→reflects-epi Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
-  surjective→epi (el! ⌞ X ⌟) (el! ⌞ Y ⌟) (f .hom) f-surj {Z}
+instance
+  Extensional-Topology-hom
+    : ∀ {ℓ} {X Y : Topological-space ℓ} {ℓr}
+    → ⦃ _ : Extensional (⌞ X ⌟ → ⌞ Y ⌟) ℓr ⦄
+    → Extensional (Topologies.Hom X Y) ℓr
+  Extensional-Topology-hom ⦃ e ⦄ =
+    injection→extensional! (λ p → total-hom-path _ p prop!) e
 ```
+-->
+
+-- ## Morphisms
+
+-- ```agda
+-- continuous-injection→monic
+--   : ∀ {ℓ} {X Y : Topological-space ℓ}
+--   → (f : Topologies.Hom X Y)
+--   → injective (f .hom)
+--   → Topologies.is-monic f
+-- continuous-injection→monic f f-inj =
+--   faithful→reflects-mono Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
+--   injective→monic (hlevel 2) f-inj {Z}
+
+-- monic→continuous-injection
+--   : ∀ {ℓ} {X Y : Topological-space ℓ}
+--   → (f : Topologies.Hom X Y)
+--   → Topologies.is-monic f
+--   → injective (f .hom)
+-- monic→continuous-injection f f-monic =
+--   {!!}
+--   -- monic→injective (hlevel 2) $
+--   -- λ g h p → ap hom (f-monic (total-hom g {!!}) (total-hom h {!!}) (total-hom-path _ p prop!))
+
+-- continuous-surjection→epic
+--   : ∀ {ℓ} {X Y : Topological-space ℓ}
+--   → (f : Topologies.Hom X Y)
+--   → is-surjective (f .hom)
+--   → Topologies.is-epic f
+-- continuous-surjection→epic {X = X} {Y = Y} f f-surj =
+--   faithful→reflects-epi Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
+--   surjective→epi (el! ⌞ X ⌟) (el! ⌞ Y ⌟) (f .hom) f-surj {Z}
+-- ```
+
+-- ```agda
+-- Topologies-on : ∀ ℓ → Displayed (Sets ℓ) ℓ ℓ
+-- Topologies-on ℓ = Thin-structure-over (Topology-structure ℓ)
+-- ```
diff --git a/src/Topology/Instances/Discrete.lagda.md b/src/Topology/Instances/Discrete.lagda.md
new file mode 100644
index 000000000..a3c9178a7
--- /dev/null
+++ b/src/Topology/Instances/Discrete.lagda.md
@@ -0,0 +1,80 @@
+---
+description: |
+  The discrete topology on a type.
+---
+<!--
+```agda
+open import Cat.Displayed.Total
+open import Cat.Functor.Adjoint
+open import Cat.Prelude
+
+open import Data.Power
+
+open import Topology.Base
+```
+-->
+```agda
+module Topology.Instances.Discrete where
+```
+
+# The discrete topology
+
+:::{.definition #discrete-topology}
+The **discrete topology** on a type $X$ is the topology where every
+subset $U : \power{\power{X}}$ is open.
+:::
+
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  X Y : Type ℓ
+
+open Topology-on
+open is-continuous
+open Total-hom
+```
+-->
+
+```agda
+Discrete-topology : ∀ {ℓ} (X : Type ℓ) → Topology-on X
+Discrete-topology X .Opens = maximal
+Discrete-topology X .maximal-open = tt
+Discrete-topology X .∩-open _ _ = tt
+Discrete-topology X .⋃ˢ-open _ _ = tt
+```
+
+Note that every function out of the discrete topology on $X$ is continuous.
+
+```agda
+discrete-continuous
+  : ∀ {T : Topology-on Y}
+  → (f : X → Y)
+  → is-continuous f (Discrete-topology X) T
+discrete-continuous f .reflect-open _ = tt
+```
+
+This means that discrete topologies are [[free objects]] relative to
+the forgetful functor $\Top \to \Sets$.
+
+```agda
+Discrete-topology-free : ∀ (X : Set ℓ) → Free-object Topologies↪Sets X
+Discrete-topology-free X .Free-object.free = X , Discrete-topology ⌞ X ⌟
+Discrete-topology-free X .Free-object.unit x = x
+Discrete-topology-free X .Free-object.fold f .hom = f
+Discrete-topology-free X .Free-object.fold f .preserves = discrete-continuous f
+Discrete-topology-free X .Free-object.commute = refl
+Discrete-topology-free X .Free-object.unique g p = ext (apply p)
+```
+
+We can assemble these free objects together to form a left adjoint
+to the aforementioned forgetful functor.
+
+```agda
+Discrete-topologies : Functor (Sets ℓ) (Topologies ℓ)
+Discrete-topologies = free-objects→functor Discrete-topology-free
+
+Discrete-topologies⊣Topologies↪Sets : Discrete-topologies {ℓ} ⊣ Topologies↪Sets
+Discrete-topologies⊣Topologies↪Sets = free-objects→left-adjoint Discrete-topology-free
+```
diff --git a/src/preamble.tex b/src/preamble.tex
index 754d26ad6..39dcc6762 100644
--- a/src/preamble.tex
+++ b/src/preamble.tex
@@ -78,6 +78,7 @@
 \knowncat{Rel}
 \knowncat{Par}
 \knowncat{Pos}
+\knowncat{Top}
 \knownbicat{Cat}
 \knownbicat{Topos}
 \knownbicat{Grpd}

From f7e7367a19aee28f9ee9510eae625d03287a0544 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 8 Aug 2024 15:37:15 -0700
Subject: [PATCH 7/9] def: cofree objects

---
 src/Cat/Functor/Adjoint.lagda.md  | 66 +++++++++++++++++++++++++++++++
 src/Cat/Functor/Morphism.lagda.md |  2 +-
 2 files changed, 67 insertions(+), 1 deletion(-)

diff --git a/src/Cat/Functor/Adjoint.lagda.md b/src/Cat/Functor/Adjoint.lagda.md
index d22e4b06d..1a02c887a 100644
--- a/src/Cat/Functor/Adjoint.lagda.md
+++ b/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
diff --git a/src/Cat/Functor/Morphism.lagda.md b/src/Cat/Functor/Morphism.lagda.md
index e2b023082..eacfde8c7 100644
--- a/src/Cat/Functor/Morphism.lagda.md
+++ b/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 :

From 6d28e62bf4b41b77ec9805bb80afdba084282c30 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 8 Aug 2024 15:37:45 -0700
Subject: [PATCH 8/9] def: (co)discrete topologies, epis/monos in Top

---
 src/1Lab/Function/Embedding.lagda.md       |   9 ++
 src/Topology/Base.lagda.md                 |   1 -
 src/Topology/Cat.lagda.md                  | 111 ++++++++++++++++++++
 src/Topology/Instances/Codiscrete.lagda.md |  94 +++++++++++++++++
 src/Topology/Instances/Cofree.lagda.md     | 114 +++++++++++++++++++++
 src/Topology/Instances/Discrete.lagda.md   |  22 ++--
 6 files changed, 340 insertions(+), 11 deletions(-)
 create mode 100644 src/Topology/Cat.lagda.md
 create mode 100644 src/Topology/Instances/Codiscrete.lagda.md
 create mode 100644 src/Topology/Instances/Cofree.lagda.md

diff --git a/src/1Lab/Function/Embedding.lagda.md b/src/1Lab/Function/Embedding.lagda.md
index 831dc6006..32e1ad7c4 100644
--- a/src/1Lab/Function/Embedding.lagda.md
+++ b/src/1Lab/Function/Embedding.lagda.md
@@ -181,6 +181,15 @@ injective→monic
 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)
diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
index 4ba702a7e..5bd3fe2a4 100644
--- a/src/Topology/Base.lagda.md
+++ b/src/Topology/Base.lagda.md
@@ -6,7 +6,6 @@ description: |
 ```agda
 open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Properties
-open import Cat.Functor.Morphism
 open import Cat.Prelude
 
 open import Data.Set.Surjection
diff --git a/src/Topology/Cat.lagda.md b/src/Topology/Cat.lagda.md
new file mode 100644
index 000000000..3cf0cfac8
--- /dev/null
+++ b/src/Topology/Cat.lagda.md
@@ -0,0 +1,111 @@
+---
+description: |
+  Basic facts about the category of topological spaces.
+---
+<!--
+```agda
+open import Cat.Functor.Morphism
+open import Cat.Displayed.Total
+open import Cat.Prelude
+
+open import Data.Set.Surjection
+open import Data.Power
+
+open import Topology.Instances.Codiscrete
+open import Topology.Instances.Discrete
+open import Topology.Base
+```
+-->
+```agda
+module Topology.Cat where
+```
+
+<!--
+```agda
+open Total-hom
+```
+-->
+
+# Basic facts about the category of topological spaces
+
+This file collects a bunch of basic facts about the category of
+topological spaces into a single place.
+
+## Morphisms
+
+If $f : X \to Y$ is an injective [[continuous function]], then $f$
+is [[monic]].
+
+```agda
+continuous-injection→monic
+  : ∀ {ℓ} {X Y : Topological-space ℓ}
+  → (f : Topologies.Hom X Y)
+  → injective (f .hom)
+  → Topologies.is-monic f
+```
+
+To see this, note that the forgetful functor $U : \Top \to \Sets$ is
+[[faithful]], and recall that faithful functors reflect monos.
+
+```agda
+continuous-injection→monic f f-inj =
+  faithful→reflects-mono Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
+  injective→monic (hlevel 2) f-inj {Z}
+```
+
+Moreover, continuous injections are *precisely* the monos in $\Top$.
+
+```agda
+monic→continuous-injection
+  : ∀ {ℓ} {X Y : Topological-space ℓ}
+  → (f : Topologies.Hom X Y)
+  → Topologies.is-monic f
+  → injective (f .hom)
+```
+
+This follows via some general abstract nonsense: the forgetful
+functor $U : \Top \to \Sets$ is [[right adjoint]] to the functor
+that sends every set $X$ to the [[discrete topology]] on $X$, and
+[[right adjoints preserve monos]].
+
+```agda
+monic→continuous-injection f f-monic =
+  monic→injective (hlevel 2) $ λ {C} →
+  right-adjoint→preserves-monos
+    Topologies↪Sets
+    Discrete-topologies⊣Topologies↪Sets
+    f-monic {C}
+```
+
+Similarly characterise the [[epis]] in $\Top$ as continuous surjections.
+
+```agda
+continuous-surjection→epic
+  : ∀ {ℓ} {X Y : Topological-space ℓ}
+  → (f : Topologies.Hom X Y)
+  → is-surjective (f .hom)
+  → Topologies.is-epic f
+
+epic→continuous-surjection
+  : ∀ {ℓ} {X Y : Topological-space ℓ}
+  → (f : Topologies.Hom X Y)
+  → Topologies.is-epic f
+  → is-surjective (f .hom)
+```
+
+The proof is essentially dual to the one for monos: faithful functors
+reflect epis, and the forgetful functor $U : \Top \to \Sets$ is [[left adjoint]]
+to the [[codiscrete topology]] functor.
+
+```agda
+continuous-surjection→epic {X = X} {Y = Y} f f-surj =
+  faithful→reflects-epi Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
+  surjective→epi (el! ⌞ X ⌟) (el! ⌞ Y ⌟) (f .hom) f-surj {Z}
+
+epic→continuous-surjection {X = X} {Y = Y} f f-epic =
+  epi→surjective (X .fst) (Y .fst) (f .hom) $ λ {C} →
+  left-adjoint→preserves-epis
+    Topologies↪Sets
+    Topologies↪Sets⊣Codiscrete-topologies
+    f-epic {C}
+```
diff --git a/src/Topology/Instances/Codiscrete.lagda.md b/src/Topology/Instances/Codiscrete.lagda.md
new file mode 100644
index 000000000..d4b5ec96c
--- /dev/null
+++ b/src/Topology/Instances/Codiscrete.lagda.md
@@ -0,0 +1,94 @@
+---
+description: |
+  The codiscrete topology on a type.
+---
+<!--
+```agda
+open import Cat.Displayed.Total
+open import Cat.Functor.Adjoint
+open import Cat.Prelude
+
+open import Data.Power
+open import Data.Sum
+
+open import Topology.Instances.Cofree
+open import Topology.Base
+
+```
+-->
+```agda
+module Topology.Instances.Codiscrete where
+```
+
+# The codiscrete topology {defines="codiscrete-topology"}
+
+For motivation, recall that the [[discrete topology]] is the finest
+topology one can impose on a set $X$. The **codiscrete topology** is dual
+to the discrete topology: it is the *coarsest* topology possible on $X$.
+
+Classically, this topology can be constructed by taking only the empty
+set and the entirety of $X$ as open sets. Unfortunately, this does not
+work constructively, as cannot show that this set is closed under infinitary
+unions!
+
+Instead, we opt to define the codiscrete topology on $X$ as the [[cofree topology]]
+generated by the empty set.
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  X Y : Type ℓ
+
+open Cofree-object
+open is-continuous
+open Topology-on
+open Total-hom
+```
+-->
+
+```agda
+Codiscrete-topology : (X : Type ℓ) → Topology-on X
+Codiscrete-topology X = Cofree-topology λ _ → ⊥Ω
+```
+
+Though less conceptually clear, this definition gives us the right
+universal property: every function $f : X \to Y$ is continuous with
+respect to the codiscrete topology on $Y$, regardless of the topology
+on $X$!
+
+```agda
+codiscrete-continuous
+  : ∀ {T : Topology-on X}
+  → {f : X → Y}
+  → is-continuous f T (Codiscrete-topology Y)
+codiscrete-continuous {T = T} {f = f} =
+  cofree-continuous $
+  elim! (λ U ff → absurd ff)
+```
+
+Put another way, codiscrete topologies are cofree objects relative to
+the forgetful functor $U : \Top \to \Sets$.
+
+```agda
+Codiscrete-topology-cofree : ∀ (X : Set ℓ) → Cofree-object Topologies↪Sets X
+Codiscrete-topology-cofree X .cofree = X , Codiscrete-topology ⌞ X ⌟
+Codiscrete-topology-cofree X .counit x = x
+Codiscrete-topology-cofree X .unfold f .hom = f
+Codiscrete-topology-cofree X .unfold f .preserves = codiscrete-continuous
+Codiscrete-topology-cofree X .commute = refl
+Codiscrete-topology-cofree X .unique g p = ext (apply p)
+```
+
+We can assemble these cofree objects together to form a right adjoint
+to the aforementioned forgetful functor.
+
+```agda
+Codiscrete-topologies : Functor (Sets ℓ) (Topologies ℓ)
+Codiscrete-topologies =
+  cofree-objects→functor Codiscrete-topology-cofree
+
+Topologies↪Sets⊣Codiscrete-topologies : Topologies↪Sets ⊣ Codiscrete-topologies {ℓ}
+Topologies↪Sets⊣Codiscrete-topologies =
+  cofree-objects→right-adjoint Codiscrete-topology-cofree
+```
diff --git a/src/Topology/Instances/Cofree.lagda.md b/src/Topology/Instances/Cofree.lagda.md
new file mode 100644
index 000000000..b61ffa145
--- /dev/null
+++ b/src/Topology/Instances/Cofree.lagda.md
@@ -0,0 +1,114 @@
+---
+description: |
+  The cofree topology on a collection of subsets.
+---
+<!--
+```agda
+open import 1Lab.Reflection.Induction
+
+open import Cat.Prelude
+
+open import Data.Power
+
+open import Topology.Base
+```
+-->
+
+```agda
+module Topology.Instances.Cofree where
+```
+
+# The cofree topology
+
+:::{.definition #cofree-topology}
+Let $O : \power{\power{X}}$ by a set of subsets of $X$.
+The **cofree topology** generated by $O$ is the coarsest
+topology on $X$ such that every element of $O$ is open.
+:::
+
+
+<!--
+```agda
+private variable
+  ℓ : Level
+  X Y : Type ℓ
+
+open Topology-on
+open is-continuous
+```
+-->
+
+We can construct this topology in Agda by freely closing $O$ under
+finite intersections and infinitary unions.
+
+```agda
+data Cofree-opens {X : Type ℓ} (O : ℙ (ℙ X)) : ℙ X → Type ℓ where
+  basic     : ∀ (U : ℙ X) → U ∈ O → Cofree-opens O U
+  top       : Cofree-opens O maximal
+  intersect : ∀ {U V : ℙ X} → Cofree-opens O U → Cofree-opens O V → Cofree-opens O (U ∩ V)
+  union     : ∀ (S : ℙ (ℙ X)) → (∀ (U : ℙ X) → U ∈ S → Cofree-opens O U) → Cofree-opens O (⋃ˢ S)
+  trunc     : ∀ {U : ℙ X} → is-prop (Cofree-opens O U)
+```
+
+<!--
+```agda
+unquoteDecl Cofree-opens-elim-prop = make-elim-n 1 Cofree-opens-elim-prop (quote Cofree-opens)
+
+instance
+  HLevel-Cofree-opens
+    : ∀ {O : ℙ (ℙ X)} {U : ℙ X}
+    → H-Level (Cofree-opens O U) 1
+  HLevel-Cofree-opens = prop-instance trunc
+```
+-->
+
+```agda
+Cofree-topology : ℙ (ℙ X) → Topology-on X
+Cofree-topology O .Opens U = elΩ (Cofree-opens O U)
+Cofree-topology O .maximal-open = pure top
+Cofree-topology O .∩-open U-open V-open = ⦇ intersect U-open V-open ⦈
+Cofree-topology O .⋃ˢ-open S S⊆Opens = pure (union S λ U U∈S → □-out! (S⊆Opens U U∈S))
+```
+
+Like all good constructions, the cofree topology generated by
+$O : \power{\power{Y}}$ has a universal property: for every
+$f : X \to Y$ and every topology $T$ on $X$, $\forall U,\, U \in O \Rightarrow f^{-1}(U) \in T$
+if and only if $f$ is continuous with respect to the codiscrete topology.
+
+```agda
+cofree-⊆
+  : ∀ {T : Topology-on X} {O : ℙ (ℙ Y)}
+  → {f : X → Y}
+  → is-continuous f T (Cofree-topology O)
+  → O ⊆ Preimage (Preimage f) (T .Opens)
+
+cofree-continuous
+  : ∀ {T : Topology-on X} {O : ℙ (ℙ Y)}
+  → {f : X → Y}
+  → O ⊆ Preimage (Preimage f) (T .Opens)
+  → is-continuous f T (Cofree-topology O)
+```
+
+The forward direction is almost by definition: if $f$ is continuous, then
+it reflects every open in the codiscrete topology, and every element of $O$
+is open.
+
+```agda
+cofree-⊆ {f = f} f-cont U U∈O =
+  f-cont .reflect-open (pure (basic U U∈O))
+```
+
+The reverse direction requires a bit more thought, but only marginally so.
+Suppose that some $U : \power{Y}$ is open in the cofree topology. We can
+then invoke the elimination principle of `Cofree-open` to show that
+$f^{-1}(U)$ is open in $T$: all of the closure conditions hold as $T$
+is a topology, so it suffices to know that $U \in O \Rightarrow f^{-1}(U) \in T$.
+```agda
+cofree-continuous {T = T} {f = f} O⊆f[T] .reflect-open =
+  elim! $
+  Cofree-opens-elim-prop {P = λ {U} _ → Preimage f U ∈ T .Opens} (λ _ → hlevel 1)
+    O⊆f[T]
+    (T .maximal-open)
+    (λ _ U∈T _ V∈T → T .∩-open U∈T V∈T)
+    (λ S _ S⊆T → ⋃-open T (Preimage f ⊙ fst) λ V → S⊆T (V .fst) (V .snd))
+```
diff --git a/src/Topology/Instances/Discrete.lagda.md b/src/Topology/Instances/Discrete.lagda.md
index a3c9178a7..7792dc8bb 100644
--- a/src/Topology/Instances/Discrete.lagda.md
+++ b/src/Topology/Instances/Discrete.lagda.md
@@ -13,6 +13,7 @@ open import Data.Power
 open import Topology.Base
 ```
 -->
+
 ```agda
 module Topology.Instances.Discrete where
 ```
@@ -31,14 +32,15 @@ private variable
   ℓ ℓ' : Level
   X Y : Type ℓ
 
-open Topology-on
+open Free-object
 open is-continuous
+open Topology-on
 open Total-hom
 ```
 -->
 
 ```agda
-Discrete-topology : ∀ {ℓ} (X : Type ℓ) → Topology-on X
+Discrete-topology : (X : Type ℓ) → Topology-on X
 Discrete-topology X .Opens = maximal
 Discrete-topology X .maximal-open = tt
 Discrete-topology X .∩-open _ _ = tt
@@ -50,9 +52,9 @@ Note that every function out of the discrete topology on $X$ is continuous.
 ```agda
 discrete-continuous
   : ∀ {T : Topology-on Y}
-  → (f : X → Y)
+  → {f : X → Y}
   → is-continuous f (Discrete-topology X) T
-discrete-continuous f .reflect-open _ = tt
+discrete-continuous .reflect-open _ = tt
 ```
 
 This means that discrete topologies are [[free objects]] relative to
@@ -60,12 +62,12 @@ the forgetful functor $\Top \to \Sets$.
 
 ```agda
 Discrete-topology-free : ∀ (X : Set ℓ) → Free-object Topologies↪Sets X
-Discrete-topology-free X .Free-object.free = X , Discrete-topology ⌞ X ⌟
-Discrete-topology-free X .Free-object.unit x = x
-Discrete-topology-free X .Free-object.fold f .hom = f
-Discrete-topology-free X .Free-object.fold f .preserves = discrete-continuous f
-Discrete-topology-free X .Free-object.commute = refl
-Discrete-topology-free X .Free-object.unique g p = ext (apply p)
+Discrete-topology-free X .free = X , Discrete-topology ⌞ X ⌟
+Discrete-topology-free X .unit x = x
+Discrete-topology-free X .fold f .hom = f
+Discrete-topology-free X .fold f .preserves = discrete-continuous
+Discrete-topology-free X .commute = refl
+Discrete-topology-free X .unique g p = ext (apply p)
 ```
 
 We can assemble these free objects together to form a left adjoint

From 013302a67dcde4bbd517c12d8f4d176a73bf7c72 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Fri, 9 Aug 2024 10:18:54 -0700
Subject: [PATCH 9/9] def: product topologies

---
 src/Topology/Base.lagda.md              | 42 ++----------
 src/Topology/Instances/Induced.lagda.md | 18 +++--
 src/Topology/Instances/Product.lagda.md | 89 ++++++++++++++++++++++++-
 src/Topology/Instances/Union.lagda.md   | 88 ++++++++++++++++++++++++
 4 files changed, 194 insertions(+), 43 deletions(-)
 create mode 100644 src/Topology/Instances/Union.lagda.md

diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
index 5bd3fe2a4..29799c3fe 100644
--- a/src/Topology/Base.lagda.md
+++ b/src/Topology/Base.lagda.md
@@ -252,39 +252,9 @@ instance
 ```
 -->
 
--- ## Morphisms
-
--- ```agda
--- continuous-injection→monic
---   : ∀ {ℓ} {X Y : Topological-space ℓ}
---   → (f : Topologies.Hom X Y)
---   → injective (f .hom)
---   → Topologies.is-monic f
--- continuous-injection→monic f f-inj =
---   faithful→reflects-mono Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
---   injective→monic (hlevel 2) f-inj {Z}
-
--- monic→continuous-injection
---   : ∀ {ℓ} {X Y : Topological-space ℓ}
---   → (f : Topologies.Hom X Y)
---   → Topologies.is-monic f
---   → injective (f .hom)
--- monic→continuous-injection f f-monic =
---   {!!}
---   -- monic→injective (hlevel 2) $
---   -- λ g h p → ap hom (f-monic (total-hom g {!!}) (total-hom h {!!}) (total-hom-path _ p prop!))
-
--- continuous-surjection→epic
---   : ∀ {ℓ} {X Y : Topological-space ℓ}
---   → (f : Topologies.Hom X Y)
---   → is-surjective (f .hom)
---   → Topologies.is-epic f
--- continuous-surjection→epic {X = X} {Y = Y} f f-surj =
---   faithful→reflects-epi Topologies↪Sets Topologies↪Sets-faithful $ λ {Z} →
---   surjective→epi (el! ⌞ X ⌟) (el! ⌞ Y ⌟) (f .hom) f-surj {Z}
--- ```
-
--- ```agda
--- Topologies-on : ∀ ℓ → Displayed (Sets ℓ) ℓ ℓ
--- Topologies-on ℓ = Thin-structure-over (Topology-structure ℓ)
--- ```
+# As a displayed category
+
+```agda
+Topologies-on : ∀ ℓ → Displayed (Sets ℓ) ℓ ℓ
+Topologies-on ℓ = Thin-structure-over (Topology-structure ℓ)
+```
diff --git a/src/Topology/Instances/Induced.lagda.md b/src/Topology/Instances/Induced.lagda.md
index c5322cb76..bfb82e758 100644
--- a/src/Topology/Instances/Induced.lagda.md
+++ b/src/Topology/Instances/Induced.lagda.md
@@ -22,6 +22,7 @@ module Topology.Instances.Induced where
 ```agda
 private variable
   ℓ ℓ' : Level
+  X Y Z : Type ℓ
 
 open Topology-on
 open is-continuous
@@ -78,6 +79,17 @@ induced-continuous
   → is-continuous f (Induced f Y-top) Y-top
 induced-continuous .reflect-open {U = U} U-open =
   pure (U , U-open , refl)
+
+induced-universal
+  : ∀ {S : Topology-on X} {T : Topology-on Z}
+  → {f : Y → Z} {g : X → Y}
+  → is-continuous (f ⊙ g) S T
+  → is-continuous g S (Induced f T)
+induced-universal {S = S} {T = T} {g = g} fg-cont .reflect-open {U} =
+  rec! λ V V-open f[V]=U →
+    subst (is-open S)
+      (funext λ z → f[V]=U $ₚ g z)
+      (fg-cont .reflect-open V-open)
 ```
 
 ```agda
@@ -89,11 +101,7 @@ Topologies-fibration {ℓ} .Cartesian-fibration.has-lift f Y-top = cart where
   cart : Cartesian-lift (Topologies-on ℓ) f Y-top
   cart .x' = Induced f Y-top
   cart .lifting = induced-continuous
-  cart .cartesian .universal {u = Z} {u' = Z-top} g fg-cont .reflect-open {U = U} =
-    rec! λ V V-open f[V]=U →
-      subst (is-open Z-top)
-        (funext λ z → f[V]=U $ₚ g z)
-        (fg-cont .reflect-open V-open)
+  cart .cartesian .universal g fg-cont = induced-universal fg-cont
   cart .cartesian .commutes _ _ = prop!
   cart .cartesian .unique _ _ = prop!
 ```
diff --git a/src/Topology/Instances/Product.lagda.md b/src/Topology/Instances/Product.lagda.md
index 62c18f911..7053b4bba 100644
--- a/src/Topology/Instances/Product.lagda.md
+++ b/src/Topology/Instances/Product.lagda.md
@@ -4,8 +4,13 @@ description: |
 ---
 <!--
 ```agda
+open import Cat.Diagram.Product.Indexed
+open import Cat.Displayed.Total
+open import Cat.Diagram.Product
 open import Cat.Prelude
 
+open import Topology.Instances.Induced
+open import Topology.Instances.Union
 open import Topology.Base
 ```
 -->
@@ -13,11 +18,91 @@ open import Topology.Base
 module Topology.Instances.Product where
 ```
 
+# Products of topological spaces
+
 <!--
 ```agda
 private variable
-  o ℓ o' ℓ' : Level
+  ℓ ℓ' : Level
+  X Y : Type ℓ
+  S T : Topology-on X
 
-open Topological-space
+open Topology-on
+open Total-hom
+open is-continuous
+open Product
+open Indexed-product
 ```
 -->
+
+```agda
+_×ᵗ_
+  : ∀ {X : Type ℓ} {Y : Type ℓ'}
+  → Topology-on X → Topology-on Y
+  → Topology-on (X × Y)
+S ×ᵗ T = Induced fst S ∪ᵗ Induced snd T
+```
+
+```agda
+fst-continuous : is-continuous fst (S ×ᵗ T) S
+fst-continuous {T = T} =
+  ∪-continuousl {S' = Induced snd T} induced-continuous
+
+snd-continuous : is-continuous snd (S ×ᵗ T) T
+snd-continuous {S = S} =
+  ∪-continuousr {S = Induced fst S} induced-continuous
+```
+
+```agda
+Topologies-product
+  : ∀ (X Y : Topological-space ℓ)
+  → Product (Topologies ℓ) X Y
+Topologies-product X Y .apex =
+  el! (⌞ X ⌟ × ⌞ Y ⌟) , X .snd ×ᵗ Y .snd
+Topologies-product X Y .π₁ .hom = fst
+Topologies-product X Y .π₁ .preserves = fst-continuous {T = Y .snd}
+Topologies-product X Y .π₂ .hom = snd
+Topologies-product X Y .π₂ .preserves = snd-continuous {S = X .snd}
+Topologies-product X Y .has-is-product .is-product.⟨_,_⟩ f g .hom x = f # x , g # x
+Topologies-product X Y .has-is-product .is-product.⟨_,_⟩ f g .preserves =
+  ∪-continuous {T = Induced fst (X .snd)} {T' = Induced snd (Y .snd)}
+    (induced-universal (f .preserves))
+    (induced-universal (g .preserves))
+Topologies-product X Y .has-is-product .is-product.π₁∘⟨⟩ = trivial!
+Topologies-product X Y .has-is-product .is-product.π₂∘⟨⟩ = trivial!
+Topologies-product X Y .has-is-product .is-product.unique p q =
+  ext λ x → p #ₚ x , q #ₚ x
+```
+
+# Indexed products
+
+```agda
+Πᵗ
+  : ∀ {κ} {I : Type κ} {Xᵢ : I → Type ℓ}
+  → (∀ i → Topology-on (Xᵢ i)) → Topology-on (∀ i → Xᵢ i)
+Πᵗ Tᵢ = ⋃ᵗ λ i → Induced (_$ i) (Tᵢ i)
+
+proj-continuous
+  : ∀ {κ} {I : Type κ} {Xᵢ : I → Type ℓ}
+  → (Tᵢ : ∀ i → Topology-on (Xᵢ i))
+  → ∀ (i : I) → is-continuous (_$ i) (Πᵗ Tᵢ) (Tᵢ i)
+proj-continuous Tᵢ i =
+  ⋃-continuous {Sᵢ = λ i → Induced (_$ i) (Tᵢ i)} i induced-continuous
+
+Topologies-indexed-product
+  : ∀ {I : Type ℓ}
+  → (Xᵢ : I → Topological-space ℓ)
+  → Indexed-product (Topologies ℓ) Xᵢ
+Topologies-indexed-product {I = I} Xᵢ .ΠF =
+  el! (∀ (i : I) → ⌞ Xᵢ i ⌟) , Πᵗ (λ i → Xᵢ i .snd)
+Topologies-indexed-product {I = I} Xᵢ .π i .hom f = f i
+Topologies-indexed-product {I = I} Xᵢ .π i .preserves =
+  proj-continuous (λ i → Xᵢ i .snd) i
+Topologies-indexed-product {I = I} Xᵢ .has-is-ip .is-indexed-product.tuple fᵢ .hom y i = fᵢ i # y
+Topologies-indexed-product {I = I} Xᵢ .has-is-ip .is-indexed-product.tuple fᵢ .preserves =
+  ⋃-universal λ i → induced-universal (fᵢ i .preserves)
+Topologies-indexed-product {I = I} Xᵢ .has-is-ip .is-indexed-product.commute =
+  trivial!
+Topologies-indexed-product {I = I} Xᵢ .has-is-ip .is-indexed-product.unique fᵢ p =
+  ext (λ y i → p i #ₚ y)
+```
diff --git a/src/Topology/Instances/Union.lagda.md b/src/Topology/Instances/Union.lagda.md
new file mode 100644
index 000000000..9dd5b2f4a
--- /dev/null
+++ b/src/Topology/Instances/Union.lagda.md
@@ -0,0 +1,88 @@
+---
+description: |
+  The union of topologies.
+---
+<!--
+```agda
+open import Cat.Prelude
+
+open import Data.Power
+open import Data.Sum
+
+open import Topology.Instances.Cofree
+open import Topology.Base
+```
+-->
+```agda
+module Topology.Instances.Union where
+```
+
+# Unions of topologies
+
+<!--
+```agda
+private variable
+  ℓ : Level
+  X Y : Type ℓ
+
+open is-continuous
+open Topology-on
+```
+-->
+
+```agda
+_∪ᵗ_ : Topology-on X → Topology-on X → Topology-on X
+S ∪ᵗ T = Cofree-topology (S .Opens ∪ T .Opens)
+
+∪-continuousl
+  : {S S' : Topology-on X} {T : Topology-on Y}
+  → {f : X → Y}
+  → is-continuous f S T
+  → is-continuous f (S ∪ᵗ S') T
+∪-continuousl {f = f} f-cont .reflect-open {U} U∈T =
+  pure (basic (Preimage f U) (pure (inl (f-cont .reflect-open U∈T))))
+
+∪-continuousr
+  : {S S' : Topology-on X} {T : Topology-on Y}
+  → {f : X → Y}
+  → is-continuous f S' T
+  → is-continuous f (S ∪ᵗ S') T
+∪-continuousr {f = f} f-cont .reflect-open {U} U∈T =
+  pure (basic (Preimage f U) (pure (inr (f-cont .reflect-open U∈T))))
+
+∪-continuous
+  : ∀ {S : Topology-on X} {T T' : Topology-on Y}
+  → {f : X → Y}
+  → is-continuous f S T
+  → is-continuous f S T'
+  → is-continuous f S (T ∪ᵗ T')
+∪-continuous T-cont T'-cont =
+  cofree-continuous λ U → rec! λ where
+    (inl U∈T) → T-cont .reflect-open U∈T
+    (inr U∈T') → T'-cont .reflect-open U∈T'
+
+```
+
+```agda
+⋃ᵗ : ∀ {κ} {I : Type κ} → (I → Topology-on X) → Topology-on X
+⋃ᵗ Tᵢ = Cofree-topology (⋃ (λ i → Tᵢ i .Opens))
+
+⋃-continuous
+  : ∀ {κ} {I : Type κ}
+  → {Sᵢ : I → Topology-on X} {T : Topology-on Y}
+  → {f : X → Y}
+  → (i : I) → is-continuous f (Sᵢ i) T
+  → is-continuous f (⋃ᵗ Sᵢ) T
+⋃-continuous {f = f} i f-cont .reflect-open {U} U∈T =
+  pure (basic (Preimage f U) (pure (i , f-cont .reflect-open U∈T)))
+
+⋃-universal
+  : ∀ {κ} {I : Type κ}
+  → {S : Topology-on X} {Tᵢ : I → Topology-on Y}
+  → {f : X → Y}
+  → (∀ i → is-continuous f S (Tᵢ i))
+  → is-continuous f S (⋃ᵗ Tᵢ)
+⋃-universal f-cont =
+  cofree-continuous λ U → rec! λ i U∈Tᵢ →
+    f-cont i .reflect-open U∈Tᵢ
+```