diff --git a/src/1Lab/Function/Embedding.lagda.md b/src/1Lab/Function/Embedding.lagda.md
index a7a19a19d..32e1ad7c4 100644
--- a/src/1Lab/Function/Embedding.lagda.md
+++ b/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)
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/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 :
diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md
index 0de45bf3b..7cf7a2592 100644
--- a/src/Data/Power.lagda.md
+++ b/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)
+```
+-->
diff --git a/src/Topology/Base.lagda.md b/src/Topology/Base.lagda.md
new file mode 100644
index 000000000..29799c3fe
--- /dev/null
+++ b/src/Topology/Base.lagda.md
@@ -0,0 +1,260 @@
+---
+description: |
+  The basic theory of topological spaces.
+---
+<!--
+```agda
+open import Cat.Displayed.Univalence.Thin
+open import Cat.Functor.Properties
+open import Cat.Prelude
+
+open import Data.Set.Surjection
+open import Data.Sum
+open import Data.Power
+
+import Cat.Reasoning
+
+open import 1Lab.Reflection hiding (absurd; [_])
+```
+-->
+```agda
+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**
+
+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.
+
+With that small bit of motivation out of the way, we can proceed to
+give a formal definition of a topology.
+
+```agda
+record Topology-on {ℓ} (X : Type ℓ) : Type ℓ where
+  no-eta-equality
+  field
+    Opens : ℙ (ℙ X)
+```
+
+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.
+
+```agda
+    maximal-open : maximal ∈ Opens
+    ∩-open : ∀ {U V : ℙ X} → U ∈ Opens → V ∈ Opens → (U ∩ V) ∈ Opens
+```
+
+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!
+
+```agda
+    ⋃ˢ-open : ∀ (S : ℙ (ℙ X)) → S ⊆ Opens → ⋃ˢ S ∈ Opens
+```
+
+<!--
+```agda
+  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
+  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))
+```
+
+As an easy corollary, the empty set is also open.
+
+```agda
+  minimal-open : minimal ∈ Opens
+  minimal-open =
+    subst is-open
+      (⋃-minimal (λ _ → maximal))
+      (⋃-open (λ _ → maximal) (λ _ → maximal-open))
+```
+
+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!
+
+```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 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
+  {ℓ ℓ'} {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 = Topology-on X-top
+    module Y = Topology-on Y-top
+  field
+    reflect-open : ∀ {U : ℙ Y} → U ∈ Y.Opens → Preimage f U ∈ X.Opens
+```
+
+<!--
+```agda
+open is-continuous
+
+unquoteDecl H-Level-is-continuous = declare-record-hlevel 1 H-Level-is-continuous (quote is-continuous)
+```
+-->
+
+# 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 =
+  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)
+
+Topologies : ∀ ℓ → Precategory (lsuc ℓ) (ℓ ⊔ ℓ)
+Topologies ℓ = Structured-objects (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 ℓ)
+Topologies↪Sets = Forget-structure (Topology-structure _)
+
+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
+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
+```
+-->
+
+# As a displayed category
+
+```agda
+Topologies-on : ∀ ℓ → Displayed (Sets ℓ) ℓ ℓ
+Topologies-on ℓ = Thin-structure-over (Topology-structure ℓ)
+```
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/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
+```
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
new file mode 100644
index 000000000..7792dc8bb
--- /dev/null
+++ b/src/Topology/Instances/Discrete.lagda.md
@@ -0,0 +1,82 @@
+---
+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 Free-object
+open is-continuous
+open Topology-on
+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 .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 = 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
+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/Topology/Instances/Induced.lagda.md b/src/Topology/Instances/Induced.lagda.md
new file mode 100644
index 000000000..bfb82e758
--- /dev/null
+++ b/src/Topology/Instances/Induced.lagda.md
@@ -0,0 +1,107 @@
+---
+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
+  X Y Z : Type ℓ
+
+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)
+
+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
+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 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
new file mode 100644
index 000000000..7053b4bba
--- /dev/null
+++ b/src/Topology/Instances/Product.lagda.md
@@ -0,0 +1,108 @@
+---
+description: |
+  Products of topological spaces.
+---
+<!--
+```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
+```
+-->
+```agda
+module Topology.Instances.Product where
+```
+
+# Products of topological spaces
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  X Y : Type ℓ
+  S T : Topology-on X
+
+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ᵢ
+```
diff --git a/src/preamble.tex b/src/preamble.tex
index 318c08561..39dcc6762 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}
 
@@ -77,6 +78,7 @@
 \knowncat{Rel}
 \knowncat{Par}
 \knowncat{Pos}
+\knowncat{Top}
 \knownbicat{Cat}
 \knownbicat{Topos}
 \knownbicat{Grpd}