Popups for header definitions

.gitignore

@@ -29,6 +29,10 @@ hie.yaml
 *.o-boot
 /rubtmp*
 
+*.eventlog
+*.prof
+*.html
+
 # LaTeX stuff that occasionally gets generated
 *.log
 *.synctex.gz

CONTRIBUTING.md

@@ -61,6 +61,7 @@ Link targets, called definitions, can be introduced in two ways:
   ```
   ::: {.definition #anchor-1 alias="anchor-2"}
   [the definition]
+  :::
   ```
 
 Wikilink targets are case insensitive, and get "mangled" for whitespace:
@@ -69,6 +70,32 @@ bound]]`, or `[[lub|least upper bound]]` if different textual content is
 required, or `[[lub|least-upper-bound]]`. White space **should** be used
 instead of dashes at use sites.
 
+### Definition popups
+
+Definition links can have associated "popup" information which is
+displayed when the reader hovers over that link. Popup information is
+collected according to the following rules:
+
+* If the definition is associated with a header, **the content of all
+  top-level `div.popup`{.css} before the next header** will be
+  concatenated to make up the popup.
+
+* If the definition is associated with a `div`{.html} *and* that div
+  directly contains `div.popup`{.css}s, **their contents and those of
+  other blocks directly under the definition** will be concatenated to
+  make up the popup.
+
+  This means that **non-paragraph, non-`popup`** content under a
+  definition will always be rendered on both the page and in popups.
+
+  Otherwise, the content of the popup is just the literal content of the
+  div.
+
+Note that any paragraphs contained within divs with
+`class="popup"`{.html} will be removed from the page entirely; other
+elements (e.g. code) will be preserved. Divs that have other classes
+will be preserved.
+
 ## Linking identifiers
 
 An Agda identifier that _has been referred to_ in the current module can

default.nix

@@ -2,6 +2,8 @@
   inNixShell ? false
   # Do we want the full Agda package for interactive use? Set to false in CI
 , interactive ? true
+  # Do we only want GHC?
+, ghcOnly ? false
 , system ? builtins.currentSystem
 }:
 let
@@ -68,7 +70,7 @@ in
         ".github"
       ] ./.;
 
-    nativeBuildInputs = deps;
+    nativeBuildInputs = if ghcOnly then [ our-ghc ] else deps;
 
     shellHook = ''
       export out=_build/site

src/1Lab/Classical.lagda.md

@@ -22,16 +22,22 @@ module 1Lab.Classical where
 While we do not assume any classical principles in the 1Lab, we can still state
 them and explore their consequences.
 
-The **law of excluded middle** (LEM) is the defining principle of classical logic,
-which states that any proposition is either true or false (in other words,
-[[decidable]]). Of course, assuming this as an axiom requires giving up canonicity:
-we could prove that, for example, any Turing machine either halts or does not halt,
-but this would not give us any computational information.
+The **law of excluded middle** (LEM) is the defining principle of
+classical logic, which states that any proposition is either true or
+false (in other words, [[decidable]]). Of course, assuming this as an
+axiom requires giving up canonicity: we could prove that, for example,
+any Turing machine either halts or does not halt, but this would not
+give us any computational information.
+
+::: popup
+The **law of excluded middle** says that every [[proposition]] is
+[[decidable]].
 
 ```agda
 LEM : Type
 LEM = ∀ (P : Ω) → Dec ∣ P ∣
 ```
+:::
 
 Note that we cannot do without the assumption that $P$ is a proposition: the statement
 that all types are decidable is [[inconsistent with univalence|LEM-infty]].
@@ -65,14 +71,16 @@ LEM≃DNE = prop-ext LEM-is-prop DNE-is-prop LEM→DNE DNE→LEM
 
 ## Weak excluded middle {defines="weak-excluded-middle"}
 
+::: {.popup .keep}
 The **weak law of excluded middle** (WLEM) is a slightly weaker variant
-of excluded middle which asserts that every proposition is either false
-or not false.
+of [[excluded middle]], which asserts that every proposition is either
+false or not false.
 
 ```agda
 WLEM : Type
 WLEM = ∀ (P : Ω) → Dec (¬ ∣ P ∣)
 ```
+:::
 
 As the name suggests, the law of excluded middle implies the weak law
 of excluded middle.
@@ -91,8 +99,11 @@ WLEM-is-prop = hlevel 1
 
 ## The axiom of choice {defines="axiom-of-choice"}
 
-The **axiom of choice** is a stronger classical principle which allows us to commute
-propositional truncations past Π types.
+::: {.popup .keep}
+The **axiom of choice** is a stronger classicality principle, which says
+we can commute [[propositional truncations]] over dependent product
+types (over [[sets]]).
+:::
 
 ```agda
 Axiom-of-choice : Typeω
@@ -112,9 +123,9 @@ _ = Fibration-equiv
 ```
 -->
 
-An equivalent and sometimes useful statement is that all surjections between sets
-merely have a section. This is essentially jumping to the other side of the
-`fibration equivalence`{.Agda ident=Fibration-equiv}.
+An equivalent and sometimes useful statement is that all surjections
+between sets merely have a section. This is essentially jumping to the
+other side of the `fibration equivalence`{.Agda ident=Fibration-equiv}.
 
 ```agda
 Surjections-split : Typeω

src/1Lab/Counterexamples/Isovalence.lagda.md

@@ -42,7 +42,7 @@ fact will be crucial in the proof below.
 
 We say that **isovalence holds** if the isomorphisms, equipped with the
 natural choice of identity, form an identity system on every universe
-$\ty_j$.
+$\type_j$.
 
 ```agda
 Isovalence : Typeω

src/1Lab/Equiv.lagda.md

@@ -34,6 +34,7 @@ that page has a formalisation of its failure.
 
 [provably not the case]: 1Lab.Counterexamples.IsIso.html
 
+:::{.definition #good-notion-of-equivalence}
 We must therefore define a property of functions which refines being an
 isomorphism but *is* an isomorphism: functions satisfying this property
 will be called equivalences. More specifically, we're looking for a
@@ -51,6 +52,7 @@ family $\isequiv(f)$ which
   and its inverse map.
 
 - and finally, is an actual [[proposition]].
+:::
 
 Put concisely, we're looking to define a [[propositional truncation]] of
 $\isiso(f)$ --- one which allows us to conveniently project out the
@@ -83,6 +85,7 @@ up by defining, and proving basic things about, isomorphisms. First, we
 define what it means for functions to be inverses of eachother, on both
 the left and the right.
 
+::: {.popup .keep}
 ```agda
 is-left-inverse : (B → A) → (A → B) → Type _
 is-left-inverse g f = (x : _) → g (f x) ≡ x
@@ -94,6 +97,7 @@ is-right-inverse g f = (x : _) → f (g x) ≡ x
 A function $g$ which is both a left- and right inverse to $f$ is called
 a **two-sided inverse** (to $f$). To say that a function is an
 isomorphism is to equip it with a two-sided inverse.
+:::
 
 ::: warning
 Despite the name `is-iso`{.Agda}, a two-sided inverse is actual *data*
@@ -213,12 +217,17 @@ conjunction of the assertions above, just packaged in a way that does
 not require us to first define [[propositional truncations]]. A function
 is an **equivalence** if all of its fibres are contractible:
 
+::: popup
+A function $f : A \to B$ is an **equivalence** if the [[fibre]] $f^*(y)$
+over each point $y : B$ is [[contractible]].
+
 ```agda
 record is-equiv (f : A → B) : Type (level-of A ⊔ level-of B) where
   no-eta-equality
   field
     is-eqv : (y : B) → is-contr (fibre f y)
 ```
+:::
 
 <!--
 ```agda
@@ -553,6 +562,7 @@ x_1$. This square _also_ has a filler, connecting $\pi_0$ and $\pi_1$
 over the line $g\ y ≡ \pi\ i$.
 
 <div class=mathpar>
+
 ~~~{.quiver}
 \[\begin{tikzcd}
   {g\ y} && {g\ y} \\
@@ -910,17 +920,17 @@ postcomposition with $p\inv$, so it too is an equivalence.
 ### The Lift type
 
 Because Agda's universes are not *cumulative*, we can not freely move a
-type $A : \ty_0$ to conclude that $A : \ty_1$, or to higher universes.
+type $A : \type_0$ to conclude that $A : \type_1$, or to higher universes.
 To work around this, we have a `Lift`{.Agda} type, which, given a small
-type $A : \ty_i$ and some universe $j \gt i$, gives us a _name_ for $A$
-in $\ty_j$. To know that this operation is coherent, we can prove that
+type $A : \type_i$ and some universe $j \gt i$, gives us a _name_ for $A$
+in $\type_j$. To know that this operation is coherent, we can prove that
 the lifting map
 
 $$
 A \to \operatorname{Lift}_j A
 $$
 
-is an equivalence: the name of $A$ in $\ty_j$ really is equivalent to
+is an equivalence: the name of $A$ in $\type_j$ really is equivalent to
 the type we started with. Because `Lift`{.Agda} is a very well-behaved
 record type, the proof that this is an equivalence looks very similar to
 the proof that the identity function is an equivalence:

src/1Lab/Equiv/Biinv.lagda.md

@@ -54,6 +54,7 @@ notion of equivalence that still satisfies the three conditions? The
 answer is yes! Paradoxically, adding _more_ data to `is-iso`{.Agda}
 leaves us with a good notion of equivalence.
 
+::: {.popup .keep}
 A **left inverse** to a function $f : A \to B$ is a function $g : B \to
 A$ equipped with a [[homotopy]] $g \circ f \sim \id$. Symmetrically, a
 **right inverse** to $f$ is a function $h : B \to A$ equipped with a
@@ -68,10 +69,9 @@ rinv f = Σ[ h ∈ (_ → _) ] (f ∘ h ≡ id)
 ```
 
 A map $f$ equipped with a choice of left- and right- inverse is said to
-be **biinvertible**. Perhaps surprisingly, `is-biinv`{.Agda} is a [good
-notion of equivalence].
-
-[good notion of equivalence]: 1Lab.Equiv.html#equivalences
+be **biinvertible**. Perhaps surprisingly, `is-biinv`{.Agda} is a [[good
+notion of equivalence]].
+:::
 
 ```agda
 is-biinv : (A → B) → Type _

src/1Lab/Equiv/Fibrewise.lagda.md

@@ -97,16 +97,18 @@ equiv→total always-eqv .is-eqv y =
 
 ## Equivalences over {defines="equivalence-over"}
 
+::: {.popup .keep}
 We can generalise the notion of fibrewise equivalence to families
-$P : A \to \ty$, $Q : B \to \ty$ over *different* base types,
+$P : A \to \type$, $Q : B \to \type$ over *different* base types,
 provided we have an equivalence $e : A \simeq B$. In that case, we
 say that $P$ and $Q$ are **equivalent over** $e$ if $P(a) \simeq Q(b)$
 whenever $a : A$ and $b : B$ are identified [[over|path over]] $e$.
+:::
 
-Using univalence, we can see this as a special case of [[dependent paths]],
-where the base type is taken to be the universe and the type family sends
-a type $A$ to the type of type families over $A$. However, the
-following explicit definition is easier to work with.
+Using univalence, we can see this as a special case of [[dependent
+paths]], where the base type is taken to be the universe and the type
+family sends a type $A$ to the type of type families over $A$. However,
+the following explicit definition is easier to work with.
 
 <!--
 ```agda

src/1Lab/Equiv/HalfAdjoint.lagda.md

@@ -25,17 +25,19 @@ module 1Lab.Equiv.HalfAdjoint where
 
 # Adjoint equivalences {defines="half-adjoint-equivalence"}
 
-An **adjoint equivalence** is an [isomorphism] $(f, g, \eta,
-\varepsilon)$ where the [homotopies] ($\eta$, $\varepsilon$) satisfy the
-[triangle identities], thus witnessing $f$ and $g$ as [[adjoint
-functors]]. In Homotopy Type Theory, we can use a _half_ adjoint
-equivalence - satisfying only _one_ of the triangle identities - as a
-[good notion of equivalence].
-
-[isomorphism]: 1Lab.Equiv.html#improving-isomorphisms
-[homotopies]: 1Lab.Path.html#π-types
-[triangle identities]: https://ncatlab.org/nlab/show/triangle+identities
-[good notion of equivalence]: 1Lab.Equiv.html#equivalences
+:::{.popup .keep}
+An **adjoint equivalence** is an [[isomorphism|quasi-inverse]] $(f, g,
+\eta, \varepsilon)$ where the [[homotopies]] ($\eta$, $\varepsilon$)
+satisfy the triangle identities, thus witnessing $f$ and $g$ as
+[[adjoint functors]].
+
+A **half-adjoint equivalence** $f : A \to B$ is equipped with an inverse
+$g : B \to A$, the homotopies $\eta, \eps$, and a witness for
+*one* of the triangle identities. These data imply that the other
+triangle identity is also satisfied, but most importantly they are a
+[[property]] of $f$, making half-adjoint equivalences into a [[good
+notion of equivalence]].
+:::
 
 ```agda
 is-half-adjoint-equiv : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : Type ℓ₂} (f : A → B) → Type _

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

@@ -88,10 +88,17 @@ really want to _not_ care about _how_ a function is a subtype inclusion,
 only that it is, we define **embeddings** as those functions which have
 propositional fibres:
 
+::: popup
+A function $f : A \to B$ is an **embedding** if the [[fibre]] $f^*(y)$
+over each $y : B$ is a [[proposition]].
+
 ```agda
 is-embedding : (A → B) → Type _
 is-embedding f = ∀ x → is-prop (fibre f x)
+```
+:::
 
+```agda
 _↪_ : Type ℓ → Type ℓ₁ → Type _
 A ↪ B = Σ[ f ∈ (A → B) ] is-embedding f
 ```

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

@@ -29,15 +29,15 @@ private variable
 
 # Surjections {defines=surjection}
 
+::: {.popup .keep}
 A function $f : A \to B$ is a **surjection** if, for each $b : B$, we
 have $\| f^*b \|$: that is, all of its [[fibres]] are inhabited. Using
 the notation for [[mere existence|merely]], we may write this as
-
 $$
 \forall (b : B),\ \exists (a : A),\ f(a) = b
 $$.
-
 which is evidently the familiar notion of surjection.
+:::
 
 ```agda
 is-surjective : (A → B) → Type _

src/1Lab/HIT/Truncation.lagda.md

@@ -207,13 +207,23 @@ is-prop≃equiv∥-∥ {P = P} =
                           (is-equiv-is-prop _ _ _)
 ```
 
-:::{.definition #merely alias="mere"}
+:::{.definition .terminology #merely alias="mere"}
 Throughout the 1Lab, we use the words "mere" and "merely" to modify a
 type to mean its propositional truncation. This terminology is adopted
 from the HoTT book. For example, a type $X$ is said _merely equivalent_
 to $Y$ if the type $\| X \equiv Y \|$ is inhabited.
 :::
 
+:::{.popup .summary}
+The **propositional truncation** $\| A \|$ of a type $A$ is the
+universal [[proposition]] equipped with a map `inc`{.Agda} mapping $A
+\to \| A \|$.
+
+Its recursion principle says that, if $P$ is a proposition, then any map
+$f : A \to P$ can be extended to $f' : \| A \| \to P$ satisfying
+$f'(\operatorname{inc} x) = f(x)$.
+:::
+
 ## Maps into sets
 
 The elimination principle for $\| A \|$ says that we can only use the