wording: another batch of descriptions

Author: plt-amy

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

@@ -1,3 +1,8 @@
+---
+description: |
+  We formalise Russell's paradox: It is impossible for the collection of
+  all types to be a type.
+---
 ```agda
 {-# OPTIONS --type-in-type #-}
 open import 1Lab.Path

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

@@ -1,3 +1,10 @@
+---
+description: |
+  We make precise the difference between dependent sum types and
+  existential quantifiers. In particular, we show that the "image" of a
+  function, but defined with Σ rather than ∃, fails to be different from
+  the domain of the function.
+---
 ```
 open import 1Lab.Equiv
 open import 1Lab.Path

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

@@ -1,3 +1,10 @@
+---
+description: |
+  We formalise _embeddings_, a homotopically well-behaved generalisation
+  of injective functions. It's immediate from our definition that every
+  injective function between sets is an embedding, and that every
+  equivalence is an embedding.
+---
 ```agda
 open import 1Lab.HLevel.Retracts
 open import 1Lab.HLevel.Universe

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

@@ -1,3 +1,8 @@
+---
+description: |
+  We establish a correspondence between "fibrewise equivalences" and
+  equivalences of total spaces (Σ-types).
+---
 ```agda
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Equiv

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

@@ -1,3 +1,8 @@
+---
+description: |
+  We show how to turn a path into an equivalence, in a computationally
+  efficient manner, using cubical methods.
+---
 ```
 open import 1Lab.HLevel
 open import 1Lab.Equiv

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

@@ -1,3 +1,10 @@
+---
+description: |
+  We formalise the theory of _half-adjoint equivalences_, another
+  well-behaved alternative to the notion of isomorphism. Then, we use
+  half-adjoint equivalences as a stepping stone to show that
+  isomorphisms are equivalences.
+---
 ```agda
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Path.Groupoid

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

@@ -1,3 +1,9 @@
+---
+description: |
+  We construct the circle as a cell complex, and compute its fundamental
+  group.
+---
+
 ```agda
 open import 1Lab.Path.Groupoid
 open import 1Lab.Univalence

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

@@ -1,3 +1,8 @@
+---
+description: |
+  We construct the torus in components as a cell complex, and establish
+  the equivalence between that definition and a product of circles.
+---
 ```agda
 open import 1Lab.Univalence
 open import 1Lab.HIT.S1

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

@@ -1,3 +1,8 @@
+---
+definition: |
+  We construct propositional truncations, the reflections of a type into
+  the universe of propositions.
+---
 ```agda
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Type.Sigma

src/1Lab/HLevel/Retracts.lagda.md

@@ -1,3 +1,10 @@
+---
+description: |
+  We establish that h-levels are closed under retractions, and use this
+  to establish many closure properties of h-levels. Then we table
+  these closure properties using Agda's instance resolution mechanism,
+  automating "boring" h-level obligations.
+---
 ```agda
 open import 1Lab.Path.Groupoid
 open import 1Lab.Type.Sigma