Adjunctions between large precategories
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.
Created on 2022-03-11.
Last modified on 2023-09-27.
module category-theory.adjunctions-large-precategories where
Imports
open import category-theory.functors-large-precategories open import category-theory.large-precategories open import category-theory.natural-transformations-functors-large-precategories open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-maps open import foundation.equivalences open import foundation.identity-types open import foundation.universe-levels
Idea
Let C
and D
be two
large precategories. Two
functors F : C → D
and
G : D → C
constitute an adjoint pair if
- for each pair of objects
X
inC
andY
inD
, there is an equivalenceϕ X Y : hom X (G Y) ≃ hom (F X) Y
such that - for every pair of morhpisms
f : X₂ → X₁
andg : Y₁ → Y₂
the following square commutes:
ϕ X₁ Y₁
hom X₁ (G Y₁) --------> hom (F X₁) Y₁
| |
G g ∘ _ ∘ f | | g ∘ _ ∘ F f
| |
v v
hom X₂ (G Y₂) --------> hom (F X₂) Y₂
ϕ X₂ Y₂
In this case we say that F
is left adjoint to G
and G
is right
adjoint to F
and write this as F ⊣ G
.
Definition
module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} (F : functor-Large-Precategory C D γF) (G : functor-Large-Precategory D C γG) where record is-adjoint-pair-Large-Precategory : UUω where field equiv-is-adjoint-pair-Large-Precategory : {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → ( hom-Large-Precategory C ( X) ( obj-functor-Large-Precategory G Y)) ≃ ( hom-Large-Precategory D ( obj-functor-Large-Precategory F X) ( Y)) naturality-equiv-is-adjoint-pair-Large-Precategory : { l1 l2 l3 l4 : Level} { X1 : obj-Large-Precategory C l1} { X2 : obj-Large-Precategory C l2} { Y1 : obj-Large-Precategory D l3} { Y2 : obj-Large-Precategory D l4} ( f : hom-Large-Precategory C X2 X1) ( g : hom-Large-Precategory D Y1 Y2) → coherence-square-maps ( map-equiv (equiv-is-adjoint-pair-Large-Precategory X1 Y1)) ( λ h → comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C ( hom-functor-Large-Precategory G g) ( h)) ( f)) ( λ h → comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D g h) ( hom-functor-Large-Precategory F f)) ( map-equiv (equiv-is-adjoint-pair-Large-Precategory X2 Y2)) open is-adjoint-pair-Large-Precategory public map-equiv-is-adjoint-pair-Large-Precategory : (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → ( hom-Large-Precategory C X (obj-functor-Large-Precategory G Y)) → ( hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y) map-equiv-is-adjoint-pair-Large-Precategory H X Y = map-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y) inv-equiv-is-adjoint-pair-Large-Precategory : (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y ≃ hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) inv-equiv-is-adjoint-pair-Large-Precategory H X Y = inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y) map-inv-equiv-is-adjoint-pair-Large-Precategory : (H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y → hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) map-inv-equiv-is-adjoint-pair-Large-Precategory H X Y = map-inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y) naturality-inv-equiv-is-adjoint-pair-Large-Precategory : ( H : is-adjoint-pair-Large-Precategory) { l1 l2 l3 l4 : Level} { X1 : obj-Large-Precategory C l1} { X2 : obj-Large-Precategory C l2} { Y1 : obj-Large-Precategory D l3} { Y2 : obj-Large-Precategory D l4} ( f : hom-Large-Precategory C X2 X1) ( g : hom-Large-Precategory D Y1 Y2) → coherence-square-maps ( map-inv-equiv-is-adjoint-pair-Large-Precategory H X1 Y1) ( λ h → comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D g h) ( hom-functor-Large-Precategory F f)) ( λ h → comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C (hom-functor-Large-Precategory G g) h) ( f)) ( map-inv-equiv-is-adjoint-pair-Large-Precategory H X2 Y2) naturality-inv-equiv-is-adjoint-pair-Large-Precategory H {X1 = X1} {X2} {Y1} {Y2} f g = coherence-square-inv-horizontal ( equiv-is-adjoint-pair-Large-Precategory H X1 Y1) ( λ h → comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C ( hom-functor-Large-Precategory G g) ( h)) ( f)) ( λ h → comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D g h) ( hom-functor-Large-Precategory F f)) ( equiv-is-adjoint-pair-Large-Precategory H X2 Y2) ( naturality-equiv-is-adjoint-pair-Large-Precategory H f g) module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} (G : functor-Large-Precategory D C γG) (F : functor-Large-Precategory C D γF) where is-left-adjoint-functor-Large-Precategory : UUω is-left-adjoint-functor-Large-Precategory = is-adjoint-pair-Large-Precategory F G module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} (F : functor-Large-Precategory C D γF) (G : functor-Large-Precategory D C γG) where is-right-adjoint-functor-Large-Precategory : UUω is-right-adjoint-functor-Large-Precategory = is-adjoint-pair-Large-Precategory F G module _ {αC αD : Level → Level} {βC βD : Level → Level → Level} (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) where record Adjunction-Large-Precategory : UUω where field level-left-adjoint-Adjunction-Large-Precategory : Level → Level left-adjoint-Adjunction-Large-Precategory : functor-Large-Precategory C D level-left-adjoint-Adjunction-Large-Precategory level-right-adjoint-Adjunction-Large-Precategory : Level → Level right-adjoint-Adjunction-Large-Precategory : functor-Large-Precategory D C level-right-adjoint-Adjunction-Large-Precategory is-adjoint-pair-Adjunction-Large-Precategory : is-adjoint-pair-Large-Precategory left-adjoint-Adjunction-Large-Precategory right-adjoint-Adjunction-Large-Precategory open Adjunction-Large-Precategory public obj-left-adjoint-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l : Level} → obj-Large-Precategory C l → obj-Large-Precategory D ( level-left-adjoint-Adjunction-Large-Precategory FG l) obj-left-adjoint-Adjunction-Large-Precategory FG = obj-functor-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) hom-left-adjoint-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 : Level} {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} → hom-Large-Precategory C X Y → hom-Large-Precategory D ( obj-left-adjoint-Adjunction-Large-Precategory FG X) ( obj-left-adjoint-Adjunction-Large-Precategory FG Y) hom-left-adjoint-Adjunction-Large-Precategory FG = hom-functor-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) preserves-id-left-adjoint-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 : Level} (X : obj-Large-Precategory C l1) → hom-left-adjoint-Adjunction-Large-Precategory FG ( id-hom-Large-Precategory C {X = X}) = id-hom-Large-Precategory D preserves-id-left-adjoint-Adjunction-Large-Precategory FG X = preserves-id-functor-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) obj-right-adjoint-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 : Level} → obj-Large-Precategory D l1 → obj-Large-Precategory C ( level-right-adjoint-Adjunction-Large-Precategory FG l1) obj-right-adjoint-Adjunction-Large-Precategory FG = obj-functor-Large-Precategory ( right-adjoint-Adjunction-Large-Precategory FG) hom-right-adjoint-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 : Level} {X : obj-Large-Precategory D l1} {Y : obj-Large-Precategory D l2} → hom-Large-Precategory D X Y → hom-Large-Precategory C ( obj-right-adjoint-Adjunction-Large-Precategory FG X) ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) hom-right-adjoint-Adjunction-Large-Precategory FG = hom-functor-Large-Precategory ( right-adjoint-Adjunction-Large-Precategory FG) preserves-id-right-adjoint-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l : Level} (Y : obj-Large-Precategory D l) → hom-right-adjoint-Adjunction-Large-Precategory FG ( id-hom-Large-Precategory D {X = Y}) = id-hom-Large-Precategory C preserves-id-right-adjoint-Adjunction-Large-Precategory FG Y = preserves-id-functor-Large-Precategory ( right-adjoint-Adjunction-Large-Precategory FG) equiv-is-adjoint-pair-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory C ( X) ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) ≃ hom-Large-Precategory D ( obj-left-adjoint-Adjunction-Large-Precategory FG X) ( Y) equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = equiv-is-adjoint-pair-Large-Precategory ( is-adjoint-pair-Adjunction-Large-Precategory FG) map-equiv-is-adjoint-pair-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory C ( X) ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) → hom-Large-Precategory D ( obj-left-adjoint-Adjunction-Large-Precategory FG X) ( Y) map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = map-equiv-is-adjoint-pair-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) ( right-adjoint-Adjunction-Large-Precategory FG) ( is-adjoint-pair-Adjunction-Large-Precategory FG) naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 l3 l4 : Level} {X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2} {Y1 : obj-Large-Precategory D l3} {Y2 : obj-Large-Precategory D l4} (f : hom-Large-Precategory C X2 X1) (g : hom-Large-Precategory D Y1 Y2) → coherence-square-maps ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1) ( λ h → comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory FG g) ( h)) ( f)) ( λ h → comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D g h) ( hom-left-adjoint-Adjunction-Large-Precategory FG f)) ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X2 Y2) naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = naturality-equiv-is-adjoint-pair-Large-Precategory ( is-adjoint-pair-Adjunction-Large-Precategory FG) inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D ( obj-left-adjoint-Adjunction-Large-Precategory FG X) ( Y) ≃ hom-Large-Precategory C ( X) ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y = inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y) map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) → hom-Large-Precategory D ( obj-left-adjoint-Adjunction-Large-Precategory FG X) ( Y) → hom-Large-Precategory C ( X) ( obj-right-adjoint-Adjunction-Large-Precategory FG Y) map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y = map-inv-equiv (equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X Y) naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory) {l1 l2 l3 l4 : Level} {X1 : obj-Large-Precategory C l1} {X2 : obj-Large-Precategory C l2} {Y1 : obj-Large-Precategory D l3} {Y2 : obj-Large-Precategory D l4} (f : hom-Large-Precategory C X2 X1) (g : hom-Large-Precategory D Y1 Y2) → coherence-square-maps ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X1 Y1) ( λ h → comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D g h) ( hom-left-adjoint-Adjunction-Large-Precategory FG f)) ( λ h → comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory FG g) ( h)) ( f)) ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG X2 Y2) naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory FG = naturality-inv-equiv-is-adjoint-pair-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) ( right-adjoint-Adjunction-Large-Precategory FG) ( is-adjoint-pair-Adjunction-Large-Precategory FG)
Properties
Unit of adjunction
Given an adjoint pair F ⊣ G
, we can construct a natural transformation
η : id → G ∘ F
called the unit of the adjunction.
module _ {αC αD : Level → Level} {βC βD : Level → Level → Level} (C : Large-Precategory αC βC) (D : Large-Precategory αD βD) where unit-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory C D) → natural-transformation-Large-Precategory ( id-functor-Large-Precategory) ( comp-functor-Large-Precategory ( right-adjoint-Adjunction-Large-Precategory FG) ( left-adjoint-Adjunction-Large-Precategory FG)) hom-family-natural-transformation-Large-Precategory ( unit-Adjunction-Large-Precategory FG) ( X) = map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG X ( obj-left-adjoint-Adjunction-Large-Precategory C D FG X) ( id-hom-Large-Precategory D) coherence-square-natural-transformation-Large-Precategory ( unit-Adjunction-Large-Precategory FG) {X = X} {Y} f = inv ( ( inv ( left-unit-law-comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C (η Y) f))) ∙ ( ap ( comp-hom-Large-Precategory' C ( comp-hom-Large-Precategory C (η Y) f)) ( inv ( preserves-id-right-adjoint-Adjunction-Large-Precategory C D FG ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y)))) ∙ ( inv ( associative-comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG ( id-hom-Large-Precategory D)) ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG Y ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y) ( id-hom-Large-Precategory D)) ( f))) ∙ ( inv ( naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG f ( id-hom-Large-Precategory D) ( id-hom-Large-Precategory D))) ∙ ( ap ( map-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG X ( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y)) ( ( associative-comp-hom-Large-Precategory D ( id-hom-Large-Precategory D) ( id-hom-Large-Precategory D) ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙ ( left-unit-law-comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D ( id-hom-Large-Precategory D) ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙ ( left-unit-law-comp-hom-Large-Precategory D ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙ ( inv ( right-unit-law-comp-hom-Large-Precategory D ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙ ( inv ( right-unit-law-comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f) ( id-hom-Large-Precategory D)))) ∙ ( ap ( comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f) ( id-hom-Large-Precategory D))) ( inv ( preserves-id-left-adjoint-Adjunction-Large-Precategory C D FG X)))) ∙ ( naturality-inv-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG ( id-hom-Large-Precategory C) ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f) ( id-hom-Large-Precategory D)) ∙ ( right-unit-law-comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG ( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ( η X))))) where η : {l : Level} (X : obj-Large-Precategory C l) → hom-Large-Precategory C X ( obj-right-adjoint-Adjunction-Large-Precategory C D FG ( obj-left-adjoint-Adjunction-Large-Precategory C D FG X)) η = hom-family-natural-transformation-Large-Precategory ( unit-Adjunction-Large-Precategory FG)
Counit of adjunction
Given an adjoint pair F ⊣ G
, we can construct a natural transformation
ε : F ∘ G → id
called the counit of the adjunction.
counit-Adjunction-Large-Precategory : (FG : Adjunction-Large-Precategory C D) → natural-transformation-Large-Precategory ( comp-functor-Large-Precategory ( left-adjoint-Adjunction-Large-Precategory FG) ( right-adjoint-Adjunction-Large-Precategory FG)) ( id-functor-Large-Precategory) hom-family-natural-transformation-Large-Precategory ( counit-Adjunction-Large-Precategory FG) Y = map-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y) ( Y) ( id-hom-Large-Precategory C) coherence-square-natural-transformation-Large-Precategory (counit-Adjunction-Large-Precategory FG) {X = X} {Y = Y} f = inv ( ( inv ( left-unit-law-comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D ( ε Y) ( hom-left-adjoint-Adjunction-Large-Precategory C D FG ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))))) ∙ ( inv ( associative-comp-hom-Large-Precategory D ( id-hom-Large-Precategory D) ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y) ( Y) ( id-hom-Large-Precategory C)) ( hom-left-adjoint-Adjunction-Large-Precategory C D FG ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)))) ∙ ( inv ( naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f) ( id-hom-Large-Precategory D) ( id-hom-Large-Precategory C))) ∙ ( ap ( map-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG ( obj-right-adjoint-Adjunction-Large-Precategory C D FG X) ( Y)) ( ( ap ( comp-hom-Large-Precategory' C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)) ( ( right-unit-law-comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG ( id-hom-Large-Precategory D))) ∙ ( preserves-id-right-adjoint-Adjunction-Large-Precategory C D FG Y))) ∙ ( left-unit-law-comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)) ∙ ( ( inv ( right-unit-law-comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))) ∙ ( inv ( right-unit-law-comp-hom-Large-Precategory C ( comp-hom-Large-Precategory C ( hom-right-adjoint-Adjunction-Large-Precategory C D FG f) ( id-hom-Large-Precategory C)))))) ∙ ( naturality-equiv-is-adjoint-pair-Adjunction-Large-Precategory C D FG ( id-hom-Large-Precategory C) ( f) ( id-hom-Large-Precategory C)) ∙ ( ap ( comp-hom-Large-Precategory ( D) ( comp-hom-Large-Precategory D f (ε X))) ( preserves-id-left-adjoint-Adjunction-Large-Precategory C D FG ( obj-right-adjoint-Adjunction-Large-Precategory C D FG X))) ∙ ( right-unit-law-comp-hom-Large-Precategory D ( comp-hom-Large-Precategory D f (ε X))))) where ε : {l : Level} (Y : obj-Large-Precategory D l) → hom-Large-Precategory D ( obj-left-adjoint-Adjunction-Large-Precategory C D FG ( obj-right-adjoint-Adjunction-Large-Precategory C D FG Y)) ( Y) ε = hom-family-natural-transformation-Large-Precategory ( counit-Adjunction-Large-Precategory FG)
Recent changes
- 2023-09-27. Fredrik Bakke. Presheaf categories (#801).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622). - 2023-05-06. Egbert Rijke. Big cleanup continued (#597).