diff --git a/src/1Lab/Reflection/Subst.agda b/src/1Lab/Reflection/Subst.agda
index fd1b84c4e..0d3c18c83 100644
--- a/src/1Lab/Reflection/Subst.agda
+++ b/src/1Lab/Reflection/Subst.agda
@@ -89,6 +89,9 @@ instance
Has-subst-Telescope : Has-subst Telescope
Has-subst-Telescope = record { applyS = subst-tel }
+ Has-subst-Abs : ∀ {ℓ} {A : Type ℓ} ⦃ _ : Has-subst A ⦄ → Has-subst (Abs A)
+ Has-subst-Abs = record { applyS = λ rho (abs nm a) → abs nm (applyS (liftS 1 rho) a) }
+
subst-tm* ρ [] = []
subst-tm* ρ (arg ι x ∷ ls) = arg ι (subst-tm ρ x) ∷ subst-tm* ρ ls
@@ -128,7 +131,7 @@ subst-tm ρ (def f args) = def f $ subst-tm* ρ args
subst-tm ρ (meta x args) = meta x $ subst-tm* ρ args
subst-tm ρ (pat-lam cs args) = pat-lam (map (subst-clause ρ) cs) (subst-tm* ρ args)
subst-tm ρ (lam v (abs n b)) = lam v (abs n (subst-tm (liftS 1 ρ) b))
-subst-tm ρ (pi (arg ι a) (abs n b)) = pi (arg ι (subst-tm ρ a)) (abs n (subst-tm (liftS 1 ρ) b))
+subst-tm ρ (pi (arg ι a) (abs n b)) = pi (arg ι (subst-tm ρ a)) (abs n (subst-tm (liftS 1 ρ) b))
subst-tm ρ (lit l) = (lit l)
subst-tm ρ unknown = unknown
subst-tm ρ (agda-sort s) with s
@@ -145,6 +148,9 @@ subst-tel ρ ((x , arg ai t) ∷ xs) = (x , arg ai (subst-tm ρ t)) ∷ subst-te
subst-clause σ (clause tel ps t) = clause (subst-tel σ tel) ps (subst-tm (liftS (length tel) σ) t)
subst-clause σ (absurd-clause tel ps) = absurd-clause (subst-tel σ tel) ps
+apply-abs : ∀ {ℓ} {A : Type ℓ} ⦃ _ : Has-subst A ⦄ → Abs A → Term → A
+apply-abs (abs _ x) a = applyS (a ∷ ids) x
+
_<#>_ : Term → Arg Term → Term
f <#> x = apply-tm f x
diff --git a/src/Cat/Functor/Amnestic.lagda.md b/src/Cat/Functor/Amnestic.lagda.md
index 579f88d7f..b4e1b444b 100644
--- a/src/Cat/Functor/Amnestic.lagda.md
+++ b/src/Cat/Functor/Amnestic.lagda.md
@@ -29,7 +29,7 @@ private variable
```
-->
-# Amnestic functors
+# Amnestic functors {defines="amnestic"}
The notion of **amnestic functor** was introduced by Adámek, Herrlich
and Strecker in their book "The Joy of Cats"^[Cats are, indeed, very
diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md
index bc82ad9d7..042813375 100644
--- a/src/Data/Set/Coequaliser.lagda.md
+++ b/src/Data/Set/Coequaliser.lagda.md
@@ -1,8 +1,10 @@
+
+## The 1Lab
+
+Open source, combination wiki (à la nLab) + Agda library.
+
+* Reimplementations of everything we need, e.g.
+
+```agda
+ open import 1Lab.Path
+```
+
+contains basic results about identity.
+
+* Lots of category theory (e.g. [Elephant](Elephant.html),
+ [Borceux](Borceux.html))
+
+* Very basic results in algebra + synthetic homotopy theory (e.g. [HoTT ch. 8](HoTT.html#chapter-8-homotopy-theory))
+
+This talk is a module in the 1Lab!
+
+## The 1Lab as a library
+
+* Constructive but *im*predicative (propositional resizing); homotopical
+ features used freely
+
+* Type classes for automation, but only of *properties*; equipping a
+ type with *structure* (e.g. algebraic) is always explicit.
+
+* Playground for new Agda features, e.g. `opaque`{.kw}, `OVERLAPPING`{.kw} instances
+
+## This talk
+
+
+
+* HoTT simplifies Martin-Löf type theory by giving universes a nice
+ universal property ([[univalence]])
+
+* Cubical type theory *complicates* type theory to make this compute
+ (`uaβ`{.Agda})
+
+Lots of work has gone into usability of traditional proof assistants;
+but what about *higher dimensional* proof assistants?
+
+# Extensional equality
+
+When are functions $f, g : A \to B$ identical?
+
+* Expected answer: whenever $f(x) \is g(x)$ for all $x$;
+* Actual answer: 🤷♀️!
+
+ Extensionality is *independent of* MLTT. E.g. [antifunext](https://github.com/AndrasKovacs/antifunext).
+
+. . .
+
+But it's for doing maths. Our solution: [the interval](1Lab.Path.html),
+[[paths]].
+
+
+
+A type `I`{.Agda}, with *endpoints* `i0`{.Agda}, `i1`{.Agda}, which
+(co)represents identifications.
+
+An identification $p : x \is_A y$ is an element $i : \bI, p(i) : A$ that
+satisfies $p(i0) = x$ and $p(i1) = y$.
+
+In Agda: path lambdas and path application.
+
+```agda
+_ : {A : Type} (x : A) → x ≡ x
+_ = λ x → λ i → x
+```
+
+## Working with the interval
+
+
+
+```agda
+ cong : (f : A → B) (x y : A) → x ≡ y → f x ≡ f y
+ cong f x y p = λ i → f (p i)
+```
+
+
+
+. . .
+
+```agda
+ sym : (x y : A) → x ≡ y → y ≡ x
+ sym x y p = λ i → p (~ i)
+```
+
+
+
+. . .
+
+```agda
+ funext : (f g : A → B) (h : ∀ x → f x ≡ g x) → f ≡ g
+ funext f g h = λ i → λ x → h x i
+```
+
+
+
+. . .
+
+```agda
+ subst : (P : A → Type) {x y : A} (p : x ≡ y) → P x → P y
+ subst P p x = transport (λ i → P (p i)) x
+```
+
+---
+
+
+
+```agda
+_ : {f : A → B} → funext {f = f} (λ x → refl) ≡ refl
+_ = refl
+
+_ : {f g : A → B} {h : ∀ x → f x ≡ g x}
+ → funext (λ x → sym (h x)) ≡ sym (funext h)
+_ = refl
+
+_ : {f g h : A → B} {α : ∀ x → f x ≡ g x} {β : ∀ x → g x ≡ h x}
+ → funext (λ x → α x ∙ β x) ≡ funext α ∙ funext β
+_ = refl
+```
+
+---
+
+We can even explain things like pattern matching on HITs:
+
+
+
+```agda
+ example : (p : S¹) → S¹
+ example base = base
+ example (loop i) = {! !}
+ -- Goal: S¹
+ -- i = i0 ⊢ base
+ -- i = i1 ⊢ base
+```
+
+
+
+. . .
+
+```agda
+ example' : (p : S¹) → P p → S¹
+ example' base x = base
+ example' (loop i) x = {! !}
+```
+
+## It's not all perfect
+
+Introducing path abstractions does a number on inference:
+
+
+
+```agda
+ what : ((x y : A) → x ≡ y) → (x y : A) → x ≡ y
+ what h x y i = h _ _ i
+```
+
+Agda generates constraints:
+
+
+ _x h x y (i = i0) = x
+ _y h x y (i = i1) = y
+
+
+Neither of these is fully determined!
+Both metas go unsolved.
+
+. . .
+
+Need a nice *interface* for extensional equality.
+
+# A nice interface
+
+Ideally: the identity type $x \is_A y$ *computes* to something simpler,
+based on the structure of $A$.
+
+* Observational type theory with strict propositions...
+
+ + Pro: computed identity type is basically always right;
+ + Con: doesn't scale to homotopy.
+
+* Higher observational type theory...
+
+ + Pro: scales to homotopy;
+ + Con: computed identity system will in many cases be overcomplicated.
+
+Key example: group homomorphisms $f, g : G \to H$. These are pairs, so
+$f \is g$ computes to a pair type.
+But the second component --- the proof that $f$ is a homomorphism --- is
+irrelevant!
+
+Without a sort of strict propositions, the system can't "see" this.
+So "primitive higher-OTT" will still need a helper, to fill in the
+trivial second component.
+
+---
+
+Surprisingly, we can use type classes!
+
+
+
+```agda
+ record Extensional (A : Type) : Type (lsuc lzero) where
+ field
+ _≈_ : A → A → Type
+ to-path : ∀ {x y : A} → x ≈ y → x ≡ y
+```
+
+
+
+. . .
+
+We have an instance for each type former we want to compute:
+
+```agda
+ instance
+ ext-fun : ⦃ Extensional B ⦄ → Extensional (A → B)
+ ext-fun ⦃ e ⦄ = record
+ { _≈_ = λ f g → ∀ x → e ._≈_ (f x) (g x)
+ ; to-path = λ h → funext λ x → e .to-path (h x)
+ }
+```
+
+. . .
+
+And an *overlappable* instance for the base case:
+
+```agda
+ ext-base : Extensional A
+ ext-base = record { to-path = λ x → x }
+ {-# OVERLAPPABLE ext-base #-}
+```
+
+---
+
+We can test that this works by asking Agda to check `ext`{.Agda} at
+various types:
+
+```agda
+ _ : {A B : Type} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
+ _ = ext
+
+ _ : {A B C : Type} {f g : A → B → C} → (∀ x y → f x y ≡ g x y) → f ≡ g
+ _ = ext
+
+ _ : {A : Type} {x y : A} → x ≡ y → x ≡ y
+ _ = ext
+```
+
+. . .
+
+A benefit: type class solving *isn't a real function*. Can be unstable
+under substitution!
+
+```agda
+ instance
+ ext-uncurry : ⦃ Extensional (A → B → C) ⦄ → Extensional (A × B → C)
+ ext-uncurry ⦃ e ⦄ = record
+ { _≈_ = λ f g → e ._≈_ (curry f) (curry g)
+ ; to-path = λ h i (x , y) → e .to-path h i x y
+ }
+ {-# OVERLAPPING ext-uncurry #-}
+```
+
+The resulting relation has three arguments, rather than two:
+
+```agda
+ _ : {A B C D : Type} {f g : A × B → C → D}
+ → (∀ a b c → f (a , b) c ≡ g (a , b) c)
+ → f ≡ g
+ _ = ext
+```
+
+---
+
+
+
+The real implementation handles maps of algebraic structures, e.g.
+groups,
+
+```agda
+ _ : {G H : Group lzero} {f g : Groups.Hom G H}
+ → ((x : ⌞ G ⌟) → f # x ≡ g # x) → f ≡ g
+ _ = ext
+```
+
+maps *from* certain higher inductive types, e.g. generic set-quotients,
+or abelian group homomorphisms from a tensor product,
+
+```agda
+ _ : {A B C : Abelian-group lzero} {f g : Ab.Hom (A ⊗ B) C}
+ → ((x : ⌞ A ⌟) (y : ⌞ B ⌟) → f # (x , y) ≡ g # (x , y))
+ → f ≡ g
+ _ = ext
+```
+
+and also: natural transformations, maps in slice categories, in comma
+categories, in categories of elements, in wide and full subcategories,
+in categories of monad algebras, type-theoretic equivalences and
+embeddings, monotone maps, &c., &c.
+
+# Structure (and) identity
+
+Same setup: when are types $A, B : \ty$ identical?
+Ideal answer: when they are *indistinguishable*.
+What distinguishes types?
+
+Take e.g. $\bN \times \mathtt{String}$ vs. $\mathtt{String} \times \bN$:
+
+* In base MLTT (or even e.g. Lean): no proof that they're distinct
+
+* ... because if you give me any property that holds of one, I can
+ modify your proof to show it holds of the other (by hand)
+
+* ... so these types should be identical!
+
+. . .
+
+The actual answer: 🤷♀️
+Univalence (and equality reflection!) says they're the same; (set-level)
+OTT says they're different; everyone else is undecided
+
+---
+
+Univalence says $(A \is B)$ is equivalent to $(A \simeq B)$:
+
+* Just as much control over $p : A \is B$ as we would have over $f : A \simeq B$;
+
+ + E.g. *exactly* two inhabitants $\ua(\id)$, $\ua(\operatorname{not})$ in $\{0, 1\} \is \{0, 1\}$
+
+Funny *looking* consequences: e.g. $\bZ \simeq \bN$, and "$\bZ$ is a
+group", so transport lets us conclude "$\bN$ is a group."
+
+Implications for library design?
+
+## Stuff vs. structure vs. property
+
+The traditional approach for doing algebra in a proof assistant is by
+letting the elaborator fill in the structure
+
++ E.g. mathlib4 (Lean): extensive use of type classes
++ E.g. mathcomp (Rocq): canonical structures
+
+Technically different approaches, but, in effect, you can say $x, y :
+\bZ$ and write "$x + y$" to mean "*the* addition on $\bZ$"
+
+From a user's POV, great! Can write maths "as on paper" and the system
+does "the right thing".
+
+---
+
+But it's actually pretty funny if you think about it:
+
++ "Additive" monoid vs "multiplicative" monoid; the same algebraic
+ structure, but the entire hierarchy is duplicated
+
++ Type synonyms like `OrderDual`: $P^{\mathrm{od}}$ is definitionally
+ $P$, but type class search doesn't respect that
+
++ Requires careful setup to avoid diamonds
+
++ Mostly sensible for concrete types, but "the" order on $X \times Y$
+ is a choice!
+
+In effect, mathematical vernacular makes explicit the *stuff*, leaves
+the *structure* implicit, and hardly ever mentions the *properties*.
+
+---
+
+Our approach is to always *bundle* types with the structure under
+consideration. Three-layered approach:
+
+```agda
+record is-ring {A : Type} (1r : A) (_*_ _+_ : A → A → A) : Type where
+ -- _*_ is a monoid, _+_ is an abelian group, distributivity
+
+record Ring-on (A : Type) : Type where
+ field
+ 1r : A
+ _*_ _+_ : A → A → A
+
+ has-is-ring : is-ring 1r _*_ _+_
+
+Ring : Type₁
+Ring = Σ[ T ∈ Type ] Ring-on T -- almost
+```
+
+
+
+Similarly `is-group`{.Agda}/`Group-on`{.Agda}/`Group`{.Agda},
+`is-monoid`{.Agda}/`Monoid-on`{.Agda}/`Monoid`{.Agda}, etc.
+
+---
+
+This layered approach still requires a bit of choosing. Categorically,
+the guidelines are:
+
+* Forgetting the *properties* should be fully faithful
+* Forgetting the *structure* should be faithful
+
+Type-theoretically, we can say:
+
+* The *properties* should be a family of [[propositions]]
+* The *structure* should preserve h-level
+
+These sometimes conflict: once we fix the multiplication, a monoid has...
+
+* exactly one identity element (so we could put it in the properties), but
+* multiplication-preserving maps of monoids don't necessarily preserve
+ the identity (so it's actually a structure).
+
+## Identity of structures
+
+Simplifying a bit, a monoid $M$ is a tuple $(M_0, *, 1, \lambda, \rho, \alpha)$ consisting of
+
+* The *stuff*: $M_0$;
+* The *structure*: the binary operator and the identity;
+* The *property*: the proofs of identity on the left, on the right, and
+ of associativity.
+
+When are two monoids the same?
+
+---
+
+Let's make it a bit more formal: we define the property, parametrised
+over the stuff and the structure;
+
+```agda
+is-monoid : (M : Type) → (M → M → M) → M → Type
+is-monoid M m u =
+ is-set M -- required so is-monoid is a property
+ × (∀ x → m u x ≡ x) -- left identity
+ × (∀ x → m x u ≡ x) -- right identity
+ × (∀ x y z → m x (m y z) ≡ m (m x y) z) -- associativity
+```
+
+We'll need that it's an actual property:
+
+```agda
+is-monoid-is-prop : ∀ M m u → is-prop (is-monoid M m u)
+```
+
+
+
+Then we sum it all:
+
+```agda
+Monoid : Type₁
+Monoid =
+ Σ[ M ∈ Type ] -- stuff
+ Σ[ m ∈ (M → M → M) ] Σ[ u ∈ M ] -- structure
+ (is-monoid M m u) -- property
+```
+
+Completely formally, a `Monoid`{.Agda} has 7 fields, but we've shown
+that 4 don't matter.
+
+---
+
+Then we can compute the identity type: If we have monoids $M = (M_0, m, u,
+\alpha)$ and $N = (N_0, n, v, \beta)$, what is $M \is N$?
+
+```agda
+module _ (M@(M₀ , m , u , α) N@(N₀ , n , v , β) : Monoid) where
+```
+
+. . .
+
+Step 1: an identity of tuples is a tuple of identities, and identity in
+`is-monoid`{.Agda} is trivial;
+
+```agda
+ Step₁ : Type₁
+ Step₁ = Σ[ p ∈ M₀ ≡ N₀ ]
+ ( PathP (λ i → p i → p i → p i) m n
+ × PathP (λ i → p i) u v
+ )
+
+ step₁ : Step₁ → M ≡ N
+ step₁ (p , q , r) i = p i , q i , r i ,
+ is-prop→pathp (λ i → is-monoid-is-prop (p i) (q i) (r i)) α β i
+```
+
+---
+
+Step 2: we can simplify the `PathP`{.Agda}s to talk about transport instead:
+
+```agda
+ Step₂ : Type₁
+ Step₂ = Σ[ p ∈ M₀ ≡ N₀ ]
+ ( (∀ x y → transport p (m x y) ≡ n (transport p x) (transport p y))
+ × transport p u ≡ v
+ )
+
+ step₂ : Step₂ → Step₁
+ step₂ (p , q , r) = p , q' , to-pathp r where
+ -- q' actually pretty complicated...
+ q' = funext-dep λ α → funext-dep λ β →
+ to-pathp (q _ _ ∙ ap₂ n (from-pathp α) (from-pathp β))
+```
+
+---
+
+Step 3: we know what identity of types is!
+
+```agda
+ Step₃ : Type
+ Step₃ = Σ[ p ∈ M₀ ≃ N₀ ] -- equivalence!
+ ( (∀ x y → p .fst (m x y) ≡ n (p .fst x) (p .fst y))
+ × p .fst u ≡ v
+ )
+```
+
+Takes a bit of massaging...
+
+```agda
+ step₃ : Step₃ → Step₂
+ step₃ (p , q , r) = ua p , q' , r' where
+ r' = transport (ua p) u ≡⟨ uaβ p u ⟩
+ p .fst u ≡⟨ r ⟩
+ v ∎
+
+ q' : ∀ x y → _
+ q' x y =
+ transport (ua p) (m x y) ≡⟨ uaβ p (m x y) ⟩
+ p .fst (m x y) ≡⟨ q x y ⟩
+ n (p .fst x) (p .fst y) ≡⟨ ap₂ n (sym (uaβ p x)) (sym (uaβ p y)) ⟩
+ n (transport (ua p) x) (transport (ua p) y) ∎
+```
+
+The conclusion: identity in the type `Monoid`{.Agda} is *exactly¹*
+monoid isomorphism!
+
+# Designing for structure identity
+
+While it's great that the theory works, the proofs are pretty annoying.
+But they're very mechanical --- incremental!
+
+Our solution: we can make the three-layer approach from before into an
+actual theorem, using *displayed categories*.
+
+An alternative presentation of the data of a category $\cD$ equipped
+with a "projection" functor $\pi : \cD \to \cC$; just more "native" to
+type theory.
+
+
+
+---
+
+The idea: turn fibers into families.
+
+```agda
+ record Displayed o' ℓ' : Type (o ⊔ ℓ ⊔ lsuc (o' ⊔ ℓ')) where
+ field
+ Ob[_] : ⌞ C ⌟ → Type o'
+ Hom[_] : (f : Hom x y) → Ob[ x ] → Ob[ y ] → Type ℓ'
+```
+
+. . .
+
+Stuff over stuff, structure over structure:
+
+```agda
+ id' : {x' : Ob[ x ]} → Hom[ id ] x' x'
+ _∘'_
+ : {x' : Ob[ x ]} {y' : Ob[ y ]} {z' : Ob[ z ]}
+ → {f : Hom y z} (f' : Hom[ f ] y' z')
+ → {g : Hom x y} (g' : Hom[ g ] x' y')
+ → Hom[ f ∘ g ] x' z'
+```
+
+... also need property over property; check the formalisation.
+
+---
+
+If we start with a displayed category $\cE \liesover \cC$, we can
+put together a category with objects $\sum_{x : \cC}
+\operatorname{Ob}[x]$ --- the [[total category]] $\int \cE$.
+
+Similarly, each $x : \cC$ gives a category $\cE^*(x)$ with objects
+$\operatorname{Ob}[x]$ and maps $\operatorname{Hom}[\id](-,-)$ --- the
+[[fibre|fibre category]] over $x$.
+
+Properties of the functor $\pi : \int \cE \to \cC$ map very nicely to
+properties of $\cE$!
+
++--------------------+------------------------------------------------------------------------------+
+| $\pi$ is... | $\cE$ satisfies... |
++====================+==============================================================================+
+| [[faithful]] | each $\operatorname{Hom}[-](-,-)$ is a [[proposition]] |
++--------------------+------------------------------------------------------------------------------+
+| [[full]] | each $\operatorname{Hom}[-](-,-)$ is [[inhabited\|propositional truncation]] |
++--------------------+------------------------------------------------------------------------------+
+| [[fully faithful]] | each $\operatorname{Hom}[-](-,-)$ is [[contractible]] |
++--------------------+------------------------------------------------------------------------------+
+| [[amnestic]] | each $\cE^*(x)$ univalent, and so is $\cC$ |
++--------------------+------------------------------------------------------------------------------+
+
+That last row is important!
+
+---
+
+If we start with a functor, then $\operatorname{Ob}[x]$ is the type
+$\sum_{y : \cD} \pi(y) \cong x$; the "fibre" of $\pi$ over $x$.
+
+
+
+```agda
+ Street : Displayed C _ _
+ Street .Ob[_] x = Σ[ y ∈ D ] (π.₀ y ≅ x)
+```
+
+The maps over are more complicated:
+
+```agda
+ Street .Hom[_] f (x' , i) (y' , j) = Σ[ g ∈ D.Hom x' y' ]
+ (π.₁ g ≡ j .from ∘ f ∘ i .to)
+```
+
+Accordingly, the structure is pretty annoying:
+
+```agda
+ Street .id' {x} {x' , i} = record { snd =
+ π.₁ D.id ≡⟨ π.F-id ⟩
+ id ≡˘⟨ i .invr ⟩
+ i .from ∘ i .to ≡˘⟨ ap₂ _∘_ refl (C.idl _) ⟩
+ i .from ∘ id C.∘ i .to ∎ }
+ Street ._∘'_ = _ -- even worse!
+```
+
+---
+
+We can present a concrete, univalent category as a displayed category.
+
+* Concrete: the base is $\Sets$ and each $\operatorname{Hom}[-](-,-)$ is a proposition.
+* Univalent: each $\cE^*(x)$ is a partial order.
+
+. . .
+
+These data amount to:
+
+1. A type family of *structures* $F : \ty \to \ty$;
+
+2. A proposition $\operatorname{Hom}[f](S, T)$, given $f : A \to B$, $S : F(A)$, $T : F(B)$.
+
+ This type defines what it means for $f$ to be a
+ "$F$-structure-preserving map from $S$ to $T$"
+
+3. Proofs that (2) contains the identities and is closed under
+ composition;
+
+4. For univalence: a proof that if $\id$ is a structure preserving map
+ $S \to T$ (and also $T \to S$), then $S = T$.
+
+# Concrete example
+
+We start by defining the property, parametrised by the structure:
+
+```agda
+record is-semigroup {A : Type ℓ} (_⋆_ : A → A → A) : Type ℓ where
+ field
+ has-is-set : is-set A
+ assoc : ∀ {x y z} → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z
+```
+
+. . .
+
+We can derive that this *is* a property pretty mechanically:
+
+```agda
+module _ where
+ private unquoteDecl eqv = declare-record-iso eqv (quote is-semigroup)
+
+ is-semigroup-is-prop : {A : Type ℓ} {s : A → A → A} → is-prop (is-semigroup s)
+ is-semigroup-is-prop = Iso→is-hlevel 1 eqv $ Σ-is-hlevel 1 (hlevel 1) λ x →
+ let instance _ = hlevel-instance {n = 2} x in hlevel 1
+```
+
+---
+
+Then we define the structure:
+
+```agda
+record Semigroup-on (A : Type ℓ) : Type ℓ where
+ field
+ _⋆_ : A → A → A
+ has-is-semigroup : is-semigroup _⋆_
+ open is-semigroup has-is-semigroup public
+```
+
+... and what it means for functions to preserve it:
+
+```agda
+record is-semigroup-hom (f : A → B) (S : Semigroup-on A) (T : Semigroup-on B)
+ : Type (level-of A ⊔ level-of B) where
+
+ private
+ module S = Semigroup-on S
+ module T = Semigroup-on T
+
+ field
+ pres-⋆ : ∀ x y → f (x S.⋆ y) ≡ f x T.⋆ f y
+```
+
+
+
+---
+
+We can then fill in the four bullet points. $F$ is
+`Semigroup-on`{.Agda}, $\operatorname{Hom}[-](-,-)$ is
+`is-semigroup-hom`{.Agda},
+
+```agda
+Semigroup-structure : ∀ {ℓ} → Thin-structure ℓ Semigroup-on
+Semigroup-structure .is-hom f S T = el! (is-semigroup-hom f S T)
+```
+
+... identities and composites are respected ...
+
+```agda
+Semigroup-structure .id-is-hom .pres-⋆ x y = refl
+Semigroup-structure .∘-is-hom f g α β .pres-⋆ x y =
+ ap f (β .pres-⋆ x y) ∙ α .pres-⋆ _ _
+```
+
+and, finally, the univalence condition:
+
+```agda
+Semigroup-structure .id-hom-unique p q = Iso.injective eqv $ Σ-prop-path! $
+ ext λ a b → p .pres-⋆ a b
+```
+
+# Conclusion
+
+* Cubical type theory works in practice, but handling the raw primitives bites
+
+ + ... but it is possible to do better
+
+* Univalence challenges us to reconsider the notion of structure
+
+ + ... but provides insights on how to organise mathematical libraries
diff --git a/src/preamble.tex b/src/preamble.tex
index ccc3716b7..115eec02e 100644
--- a/src/preamble.tex
+++ b/src/preamble.tex
@@ -23,6 +23,9 @@
\newcommand{\Square}[4]{\rm{Square}~ {#1}~ {#2}~ {#3}~ {#4}}
\newcommand{\ap}[2]{\rm{ap}~ {#1}~ {#2}}
+\newcommand{\subst}{\operatorname{subst}}
+\newcommand{\ua}{\operatorname{ua}}
+
\newcommand{\iZ}{\rm{i0}}
\newcommand{\iO}{\rm{i1}}
diff --git a/support/shake/app/Main.hs b/support/shake/app/Main.hs
index fd2f3c153..bce65c9e5 100755
--- a/support/shake/app/Main.hs
+++ b/support/shake/app/Main.hs
@@ -164,6 +164,7 @@ rules = do
, "_build/html/static/links.json"
, "_build/html/static/search.json"
, "_build/html/css/default.css"
+ , "_build/html/css/talk.css"
, "_build/html/main.js"
, "_build/html/start.js"
, "_build/html/code-only.js"
diff --git a/support/shake/app/Shake/Markdown.hs b/support/shake/app/Shake/Markdown.hs
index 849801fc4..b673140ba 100644
--- a/support/shake/app/Shake/Markdown.hs
+++ b/support/shake/app/Shake/Markdown.hs
@@ -179,7 +179,7 @@ buildMarkdown modname input output = do
gitCommit <- gitCommit
skipAgda <- getSkipAgda
- need [templateName, bibliographyName, input]
+ need [bibliographyName, input]
modulePath <- findModule modname
authors <- gitAuthors modulePath
@@ -209,12 +209,14 @@ buildMarkdown modname input output = do
let refMap = Map.fromList $ map (\x -> (Cite.unItemId . Cite.referenceId $ x, x)) references
- Pandoc meta blocks <-
+ Pandoc meta@(Meta metamap) blocks <-
walkM (patchInline refMap)
. (if skipAgda then id else linkReferences modname)
. walk uncommentAgda
$ markdown
+ need [ if isJust (Map.lookup "talk" metamap) then talkTemplateName else pageTemplateName ]
+
-- Rendering the search data has to be done *here*, after running the
-- maths through KaTeX but before adding the emoji to headers.
let search = query (getHeaders (Text.pack modname)) markdown
@@ -387,14 +389,23 @@ patchBlock _ h = pure h
-- | Render our Pandoc document using the given template variables.
-renderMarkdown :: PandocMonad m
- => [Text] -- ^ List of authors
- -> [Val Text] -- ^ List of references
- -> String -- ^ Name of the current module
- -> String -- ^ Base URL
- -> Context Text -- ^ Digests of the various files.
- -> Pandoc -> m Text
-renderMarkdown authors references modname baseUrl digest markdown = do
+renderMarkdown
+ :: PandocMonad m
+ => [Text] -- ^ List of authors
+ -> [Val Text] -- ^ List of references
+ -> String -- ^ Name of the current module
+ -> String -- ^ Base URL
+ -> Context Text -- ^ Digests of the various files.
+ -> Pandoc
+ -> m Text
+renderMarkdown authors references modname baseUrl digest markdown@(Pandoc (Meta meta) _) = do
+ let
+ isTalk = isJust $ Map.lookup "talk" meta
+
+ templateName
+ | isTalk = talkTemplateName
+ | otherwise = pageTemplateName
+
template <- getTemplate templateName >>= runWithPartials . compileTemplate templateName
>>= either (throwError . PandocTemplateError . Text.pack) pure
let
@@ -411,13 +422,18 @@ renderMarkdown authors references modname baseUrl digest markdown = do
, ("digest", toVal digest)
]
- options = def { writerTemplate = Just template
- , writerTableOfContents = True
- , writerVariables = context
- , writerExtensions = getDefaultExtensions "html"
- }
+ opts = def
+ { writerTemplate = Just template
+ , writerTableOfContents = not isTalk
+ , writerVariables = context
+ , writerExtensions = getDefaultExtensions "html"
+ , writerSlideLevel = Just 2
+ }
+
setTranslations (Lang "en" Nothing Nothing [] [] [])
- writeHtml5String options markdown
+ if isTalk
+ then writeRevealJs opts markdown
+ else writeHtml5String opts markdown
-- | Simple textual list of starting identifiers not to fold
don'tFold :: Set.Set Text
@@ -510,6 +526,7 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) =
htmlInl :: Text -> Inline
htmlInl = RawInline "html"
-templateName, bibliographyName :: FilePath
-templateName = "support/web/template.html"
+pageTemplateName, talkTemplateName, bibliographyName :: FilePath
+pageTemplateName = "support/web/template.html"
+talkTemplateName = "support/web/template.reveal.html"
bibliographyName = "src/bibliography.bibtex"
diff --git a/support/web/css/code.scss b/support/web/css/code.scss
index 64d9326f3..8b85703ad 100644
--- a/support/web/css/code.scss
+++ b/support/web/css/code.scss
@@ -105,8 +105,8 @@ a[href].hover-highlight {
.Record { color: theme(--primary) !important; }
/* OtherAspects. */
- .UnsolvedMeta { color: theme(--code-fg); background: yellow }
- .UnsolvedConstraint { color: theme(--code-fg); background: yellow }
+ .UnsolvedMeta { color: theme(--code-fg); background: #806b00 }
+ .UnsolvedConstraint { color: theme(--code-fg); background: #806b00 }
.TerminationProblem { color: theme(--code-fg); background: #FFA07A }
.IncompletePattern { color: theme(--code-fg); background: #F5DEB3 }
.Error { color: red; text-decoration: underline }
@@ -132,7 +132,7 @@ a[href].hover-highlight {
font-weight: 400;
font-size: initial;
- body.text-page & {
+ body.text-page &, .reveal & {
font-size: var(--code-font-size);
}
}
diff --git a/support/web/css/components/search.scss b/support/web/css/components/search.scss
index 10c9aed0e..2749d34e7 100644
--- a/support/web/css/components/search.scss
+++ b/support/web/css/components/search.scss
@@ -1,4 +1,4 @@
-#search-wrapper > .modal-contents {
+#search-wrapper .modal-contents {
align-items: stretch;
text-align: left;
@@ -31,6 +31,7 @@ input#search-box {
font-size: 100%;
border: none;
+ color: theme(--text-fg);
caret-color: theme(--search-selected);
background-color: theme(--text-bg);
diff --git a/support/web/css/default.scss b/support/web/css/default.scss
index 53e12e39e..f5a5e29e3 100644
--- a/support/web/css/default.scss
+++ b/support/web/css/default.scss
@@ -25,41 +25,6 @@ html, body, main, div#post-toc-container {
max-width: 100vw;
}
-:root {
- --serif: "EB Garamond", "Times New Roman", "serif";
- --sans-serif: "Inria Sans", -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif;
- --font-size: 1.4rem;
- --code-font-size: calc(0.85 * var(--font-size));
-
- --sidenote-separation: 2em;
-
- &.sans-serif {
- --serif: "";
- --font-size: 1.3rem;
- --code-font-size: calc(0.92 * var(--font-size));
- }
-
- &.show-equations span.reasoning-step {
- .as-written {
- display: inline;
- }
- .alternate {
- display: none;
- }
- }
-
- &.show-hidden-code .commented-out {
- display: revert;
- }
-
- &.justified article {
- p, li, summary, blockquote {
- text-align: justify;
- hyphens: auto;
- }
- }
-}
-
body {
font-family: var(--serif), var(--sans-serif);
font-size: var(--font-size);
diff --git a/support/web/css/talk.scss b/support/web/css/talk.scss
new file mode 100644
index 000000000..254f6e196
--- /dev/null
+++ b/support/web/css/talk.scss
@@ -0,0 +1,147 @@
+@import "vars.scss";
+@import "mixins.scss";
+@import "theme.scss";
+
+@import "code.scss";
+
+@import "components/search.scss";
+@import "components/modal.scss";
+
+body, .reveal-viewport {
+ font-family: var(--serif), var(--sans-serif);
+ font-size: var(--font-size);
+
+ background-color: theme(--text-bg);
+ color: theme(--text-fg);
+
+ line-height: 1.25;
+}
+
+#search-wrapper {
+ font-size: 24px;
+}
+
+#author {
+ font-size: 28px;
+}
+
+.reveal-viewport {
+ --font-size: 24px;
+ --code-font-size: 22px;
+ --code-margin: 0;
+
+ pre.Agda {
+ --code-font-size: 18px;
+ }
+}
+
+.reveal {
+ .controls {
+ color: theme(--primary);
+ }
+
+ section {
+ text-align: left;
+
+ > :first-child { margin-block-start: 0; }
+ > :last-child { margin-block-end: 0; }
+
+ pre.Agda {
+ margin-block: 0;
+ }
+ }
+
+ h1, h2, h3, h4, p { margin-block: 0.75rem; }
+
+ h1 { font-size: 1.75em; }
+
+ a[href] {
+ color: theme(--primary);
+ text-decoration: none;
+
+ &:hover {
+ text-decoration: 2px currentColor underline !important;
+ }
+
+ &.header-link span.header-link-emoji {
+ display: none;
+ }
+ }
+
+ div.commented-out {
+ display: none;
+ }
+
+ em { font-style: italic; }
+ strong { font-weight: bold; }
+
+ span.reasoning-step {
+ .as-written {
+ display: none;
+ }
+ .alternate {
+ display: inline;
+ }
+ }
+}
+
+ul, ol {
+ margin-inline-start: 1em;
+}
+
+table {
+ border-collapse: collapse;
+ width: 100%;
+
+ tr.header {
+ text-align: center;
+ padding-inline: 1em;
+
+ border-block-end: 2px;
+ }
+
+ td, th {
+ border: 1px solid theme(--text-fg);
+ padding-inline: 0.25em;
+ }
+}
+
+span.katex {
+ font-size: inherit;
+ line-height: inherit;
+
+ span.mord.text > span.mord.textrm {
+ font-family: var(--serif), var(--sans-serif);
+ }
+}
+
+div.diagram-container {
+ width: 100%;
+ overflow-x: auto;
+
+ margin-block: 1em;
+
+ img.diagram {
+ margin: auto;
+ display: block;
+ height: var(--height);
+
+ overflow-x: auto;
+ }
+}
+
+span.katex-display {
+ overflow-x: auto;
+ overflow-y: clip;
+
+ margin-block: -0.25em;
+
+ > span.katex {
+ white-space: normal;
+ padding-block: 0.5em;
+ }
+}
+
+div.type-tooltip {
+ transform: scale(var(--slide-scale));
+}
diff --git a/support/web/css/theme.scss b/support/web/css/theme.scss
index 11ab6dce2..69121f5a0 100644
--- a/support/web/css/theme.scss
+++ b/support/web/css/theme.scss
@@ -187,3 +187,38 @@ $-allowed-keys: -flatten-theme($theme);
@include dark-theme-vars;
}
}
+
+:root {
+ --serif: "EB Garamond", "Times New Roman", "serif";
+ --sans-serif: "Inria Sans", -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif;
+ --font-size: 1.4rem;
+ --code-font-size: calc(0.85 * var(--font-size));
+
+ --sidenote-separation: 2em;
+
+ &.sans-serif {
+ --serif: "";
+ --font-size: 1.3rem;
+ --code-font-size: calc(0.92 * var(--font-size));
+ }
+
+ &.show-equations span.reasoning-step {
+ .as-written {
+ display: inline;
+ }
+ .alternate {
+ display: none;
+ }
+ }
+
+ &.show-hidden-code .commented-out {
+ display: revert;
+ }
+
+ &.justified article {
+ p, li, summary, blockquote {
+ text-align: justify;
+ hyphens: auto;
+ }
+ }
+}
diff --git a/support/web/js/highlight-hover.ts b/support/web/js/highlight-hover.ts
index 1a2ede4dc..88a2926db 100644
--- a/support/web/js/highlight-hover.ts
+++ b/support/web/js/highlight-hover.ts
@@ -34,15 +34,18 @@ document.addEventListener('highlight', (({ detail: { link, on } }: CustomEvent)
const selfRect = link.getBoundingClientRect();
const hoverRect = currentHover.getBoundingClientRect();
+
+ console.log(link.getClientRects())
+
// If we're close to the bottom of the page, push the tooltip above instead.
// The constant here is arbitrary, because trying to convert em to px in JS is a fool's errand.
if (selfRect.bottom + hoverRect.height + 30 > window.innerHeight) {
// 2em from the material mixin. I'm sorry
- currentHover.style.top = `calc(${link.offsetTop - hoverRect.height}px - 1em`;
+ currentHover.style.top = `calc(${selfRect.top - hoverRect.height}px - 1em`;
} else {
- currentHover.style.top = `${link.offsetTop + (link.offsetHeight / 2)}px`;
+ currentHover.style.top = `${selfRect.top + (selfRect.height / 2)}px`;
}
- currentHover.style.left = `${link.offsetLeft}px`;
+ currentHover.style.left = `${selfRect.left}px`;
}
}
match = that => that.href === link.href;
diff --git a/support/web/template.reveal.html b/support/web/template.reveal.html
new file mode 100644
index 000000000..52d34d8ef
--- /dev/null
+++ b/support/web/template.reveal.html
@@ -0,0 +1,85 @@
+
+
+
+
+
+ $if(title-prefix)$$title-prefix$ – $endif$$pagetitle$
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+