Merge branch 'main' into lattice-refactor

CITATION.bib

@@ -0,0 +1,6 @@
+@online{1lab,
+  author = {{The 1Lab Development Team}},
+  title = {{The 1Lab}},
+  url = {https://1lab.dev},
+  year = 2023,
+}

CONTRIBUTING.md

@@ -15,6 +15,10 @@ British spelling **must** be used throughout: Homotopy fib**re**,
 fib**red** category, colo**u**red operad, etc --- both in prose and in
 Agda.
 
+Headers **should** be written in sentence case, *not* title case, except
+when the concept they introduce is itself commonly written in title case
+(e.g. "Structure Identity Principle").
+
 Prose **should** be kept to a width of 72 characters.
 
 The first time a concept is introduced, it **should** appear in bold.

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

@@ -15,7 +15,7 @@ open import 1Lab.Type
 module 1Lab.Counterexamples.Russell where
 ```
 
-# Russell's Paradox {defines="russell's-paradox"}
+# Russell's paradox {defines="russell's-paradox"}
 
 This page reproduces [Russell's paradox] from naïve set theory using an
 inductive type of `Type`{.Agda}-indexed trees. By default, Agda places

src/1Lab/Equiv.lagda.md

@@ -605,7 +605,7 @@ is-empty→≃⊥ : ∀ {ℓ} {A : Type ℓ} → ¬ A → A ≃ ⊥
 is-empty→≃⊥ ¬a = _ , ¬-is-equiv ¬a
 ```
 
-# Equivalence Reasoning
+# Equivalence reasoning
 
 To make composing equivalences more intuitive, we implement operators to
 do equivalence reasoning in the same style as equational reasoning.
@@ -697,7 +697,7 @@ infixr 2 _≃⟨⟩_ _≃⟨_⟩_
 infix  3 _≃∎
 ```
 
-# Propositional Extensionality
+# Propositional extensionality
 
 The following observation is not very complex, but it is incredibly
 useful: Equivalence of propositions is the same as biimplication.

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

@@ -16,7 +16,7 @@ open import 1Lab.Type
 module 1Lab.Equiv.Fibrewise where
 ```
 
-# Fibrewise Equivalences
+# Fibrewise equivalences
 
 In HoTT, a type family `P : A → Type` can be seen as a [_fibration_]
 with total space `Σ P`, with the fibration being the projection

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

@@ -16,7 +16,7 @@ open import 1Lab.Type
 module 1Lab.Equiv.FromPath {ℓ} (P : (i : I) → Type ℓ) where
 ```
 
-# Equivs from Paths
+# Equivs from paths
 
 In [@CCHM], a direct _cubical_ construction of an equivalence `A ≃ B`
 from a path `A ≡ B` is presented. This is in contrast with the

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

@@ -24,7 +24,7 @@ open import 1Lab.Type
 module 1Lab.Equiv.HalfAdjoint where
 ```
 
-# Adjoint Equivalences
+# Adjoint equivalences
 
 An **adjoint equivalence** is an [isomorphism] $(f, g, \eta,
 \varepsilon)$ where the [homotopies] ($\eta$, $\varepsilon$) satisfy the

src/1Lab/Extensionality.agda

@@ -290,12 +290,21 @@ iso→extensional
 iso→extensional f ext =
   embedding→extensional (Iso→Embedding f) ext
 
+injection→extensional
+  : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
+  → is-set B
+  → {f : A → B}
+  → (∀ {x y} → f x ≡ f y → x ≡ y)
+  → Extensional B ℓr
+  → Extensional A ℓr
+injection→extensional b-set {f} inj ext =
+  embedding→extensional (f , injective→is-embedding b-set f inj) ext
+
 injection→extensional!
   : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
   → {@(tactic hlevel-tactic-worker) sb : is-set B}
   → {f : A → B}
   → (∀ {x y} → f x ≡ f y → x ≡ y)
   → Extensional B ℓr
   → Extensional A ℓr
-injection→extensional! {sb = b-set} {f} inj ext =
-  embedding→extensional (f , injective→is-embedding b-set f inj) ext
+injection→extensional! {sb = b-set} = injection→extensional b-set

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

@@ -5,6 +5,7 @@ definition: |
 ---
 <!--
 ```agda
+open import 1Lab.Reflection.Induction
 open import 1Lab.Reflection.HLevel
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Path.Reasoning
@@ -20,7 +21,7 @@ open import 1Lab.Type
 module 1Lab.HIT.Truncation where
 ```
 
-# Propositional Truncation {defines="propositional-truncation"}
+# Propositional truncation {defines="propositional-truncation"}
 
 Let $A$ be a type. The **propositional truncation** of $A$ is a type
 which represents the [[proposition]] "A is inhabited". In MLTT,
@@ -346,31 +347,19 @@ principles.
 <!--
 ```agda
 ∥-∥³-elim-set
-  : ∀ {ℓ ℓ'} {A : Type ℓ} {P : ∥ A ∥³ → Type ℓ'}
+  : ∀ {ℓ} {A : Type ℓ} {ℓ'} {P : ∥ A ∥³ → Type ℓ'}
   → (∀ a → is-set (P a))
   → (f : (a : A) → P (inc a))
   → (∀ a b → PathP (λ i → P (iconst a b i)) (f a) (f b))
   → ∀ a → P a
-∥-∥³-elim-set {P = P} sets f fconst = go where
-  go : ∀ a → P a
-  go (inc x) = f x
-  go (iconst a b i) = fconst a b i
-  go (icoh a b c i j) = is-set→squarep (λ i j → sets (icoh a b c i j))
-    refl (λ i → go (iconst a b i)) (λ i → go (iconst a c i)) (λ i → go (iconst b c i))
-    i j
-  go (squash x y a b p q i j k) = is-hlevel→is-hlevel-dep 2 (λ _ → is-hlevel-suc 2 (sets _))
-    (go x) (go y)
-    (λ k → go (a k)) (λ k → go (b k))
-    (λ j k → go (p j k)) (λ j k → go (q j k))
-    (squash x y a b p q) i j k
+unquoteDef ∥-∥³-elim-set = make-elim-n 2 ∥-∥³-elim-set (quote ∥_∥³)
 
 ∥-∥³-elim-prop
-  : ∀ {ℓ ℓ'} {A : Type ℓ} {P : ∥ A ∥³ → Type ℓ'}
+  : ∀ {ℓ} {A : Type ℓ} {ℓ'} {P : ∥ A ∥³ → Type ℓ'}
   → (∀ a → is-prop (P a))
   → (f : (a : A) → P (inc a))
   → ∀ a → P a
-∥-∥³-elim-prop props f = ∥-∥³-elim-set (λ _ → is-hlevel-suc 1 (props _)) f
-  (λ _ _ → is-prop→pathp (λ _ → props _) _ _)
+unquoteDef ∥-∥³-elim-prop = make-elim-n 1 ∥-∥³-elim-prop (quote ∥_∥³)
 ```
 -->
 
@@ -441,7 +430,7 @@ data ∥_∥⁴ {ℓ} (A : Type ℓ) : Type ℓ where
   squash : is-hlevel ∥ A ∥⁴ 4
 
 ∥-∥⁴-rec
-  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
+  : ∀ {ℓ} {A : Type ℓ} {ℓ'} {B : Type ℓ'}
   → is-hlevel B 4
   → (f : A → B)
   → (fconst : ∀ a b → f a ≡ f b)
@@ -450,18 +439,7 @@ data ∥_∥⁴ {ℓ} (A : Type ℓ) : Type ℓ where
                                     (fconst a b) (fcoh a c d i))
                        (fcoh a b c) (fcoh a b d))
   → ∥ A ∥⁴ → B
-∥-∥⁴-rec {A = A} {B} b4 f fconst fcoh fassoc = go where
-  go : ∥ A ∥⁴ → B
-  go (inc x) = f x
-  go (iconst a b i) = fconst a b i
-  go (icoh a b c i j) = fcoh a b c i j
-  go (iassoc a b c d i j k) = fassoc a b c d i j k
-  go (squash x y a b p q r s i j k l) = b4
-    (go x) (go y)
-    (λ i → go (a i)) (λ i → go (b i))
-    (λ i j → go (p i j)) (λ i j → go (q i j))
-    (λ i j k → go (r i j k)) (λ i j k → go (s i j k))
-    i j k l
+unquoteDef ∥-∥⁴-rec = make-rec-n 4 ∥-∥⁴-rec (quote ∥_∥⁴)
 ```
 </details>
 

src/1Lab/HLevel.lagda.md

@@ -400,7 +400,7 @@ is-hlevel-is-hlevel-suc k n = is-prop→is-hlevel-suc (is-hlevel-is-prop n)
 ```
 -->
 
-# Dependent h-Levels
+# Dependent h-levels
 
 In cubical type theory, it's natural to consider a notion of _dependent_
 h-level for a _family_ of types, where, rather than having (e.g.)

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

@@ -173,12 +173,25 @@ homotopy n-type is itself a homotopy n-type.
   → is-hlevel (∀ x y → C x y) n
 Π-is-hlevel² n w = Π-is-hlevel n λ _ → Π-is-hlevel n (w _)
 
+Π-is-hlevel²'
+  : ∀ {a b c} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
+  → (n : Nat) (Bhl : (x : A) (y : B x) → is-hlevel (C x y) n)
+  → is-hlevel (∀ {x y} → C x y) n
+Π-is-hlevel²' n w = Π-is-hlevel' n λ _ → Π-is-hlevel' n (w _)
+
 Π-is-hlevel³
   : ∀ {a b c d} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
       {D : ∀ a b → C a b → Type d}
   → (n : Nat) (Bhl : (x : A) (y : B x) (z : C x y) → is-hlevel (D x y z) n)
   → is-hlevel (∀ x y z → D x y z) n
 Π-is-hlevel³ n w = Π-is-hlevel n λ _ → Π-is-hlevel² n (w _)
+
+Π-is-hlevel³'
+  : ∀ {a b c d} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
+      {D : ∀ a b → C a b → Type d}
+  → (n : Nat) (Bhl : (x : A) (y : B x) (z : C x y) → is-hlevel (D x y z) n)
+  → is-hlevel (∀ {x y z} → D x y z) n
+Π-is-hlevel³' n w = Π-is-hlevel' n λ _ → Π-is-hlevel²' n (w _)
 ```
 -->
 

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

@@ -41,7 +41,7 @@ $n$-types is a $(n+1)$-type in $1+\ell$. That means: the universe of
 propositions is a set, the universe of sets is a groupoid, the universe
 of groupoids is a bigroupoid, and so on.
 
-## h-Levels of Equivalences
+## h-Levels of equivalences
 
 As warmup, we prove that if $A$ and $B$ are $n$-types, then so is the
 type of equivalences $A \simeq B$. For the case where $n$ is a
@@ -91,7 +91,7 @@ proof that $A$ has the given h-level. This is because, for $n \ge 1$, $A
     λ f → is-prop→is-hlevel-suc (is-equiv-is-prop f)
 ```
 
-## h-Levels of Paths
+## h-Levels of paths
 
 Univalence states that the type $X ≡ Y$ is equivalent to $X \simeq Y$.
 Since the latter is of h-level $n$ when $X$ and $Y$ are $n$-types, then

src/1Lab/Path.lagda.md

@@ -8,7 +8,7 @@ open import 1Lab.Type
 module 1Lab.Path where
 ```
 
-# The Interval
+# The interval
 
 In HoTT, the inductively-defined identity type gets a new meaning
 explanation: continuous paths, in a topological sense. The "key idea" of
@@ -133,7 +133,7 @@ familiar description, a De Morgan algebra is a Boolean algebra that does
 not (necessarily) satisfy the law of excluded middle. This is necessary
 to maintain type safety.
 
-## Raising Dimension
+## Raising dimension
 
 To wit: In cubical type theory, a term in a context with $n$ interval
 variables expresses a way of mapping an $n$-cube into that type. One
@@ -566,7 +566,7 @@ type-correct, and b) get something with the right endpoints. `(λ i → B i
 The case for dependent products (i.e. general `Σ`{.Agda} types) is
 analogous, but without any inverse transports.
 
-## Path Induction {defines="path-induction contractibility-of-singletons"}
+## Path induction {defines="path-induction contractibility-of-singletons"}
 
 The path induction principle, also known as "axiom J", essentially
 breaks down as the following two statements:
@@ -698,7 +698,7 @@ The interpretation of types as _Kan_ cubical sets guarantees that the
 open box above extends to a complete square, and thus the line $w \equiv
 z$ exists.
 
-## Partial Elements
+## Partial elements
 
 The definition of Kan cubical sets as those having fillers for all open
 boxes is all well and good, but to use this from within type theory we
@@ -1239,7 +1239,7 @@ its filler), it is contractible:
 ```
 -->
 
-# Functorial Action
+# Functorial action
 
 This composition structure on paths makes every type into an
 $\infty$-groupoid, which is discussed in [a different module].
@@ -1345,7 +1345,7 @@ for the open box with sides `refl`, `ap f p` and `ap f q`, so they must be equal
   ap-∙ f p q = ap-·· f refl p q
 ```
 
-# Syntax Sugar
+# Syntax sugar
 
 When constructing long chains of identifications, it's rather helpful to
 be able to visualise _what_ is being identified with more "priority"
@@ -1411,7 +1411,7 @@ your convenience, it's here too:
 
 Try pressing it!
 
-# Dependent Paths
+# Dependent paths
 
 Surprisingly often, we want to compare inhabitants $a : A$ and $b : B$
 where the types $A$ and $B$ are not _definitionally_ equal, but only
@@ -1597,7 +1597,7 @@ from-to-pathp {A = A} {x} {y} p i j =
 
 </details>
 
-# Path Spaces
+# Path spaces
 
 A large part of the study of HoTT is the _characterisation of path
 spaces_. Given a type `A`, what does `Path A x y` look like? [Hedberg's
@@ -1612,7 +1612,7 @@ Most of these characterisations need machinery that is not in this
 module to be properly stated. Even then, we can begin to outline a few
 simple cases:
 
-## Σ Types
+## Σ types
 
 For `Σ`{.Agda} types, a path between `(a , b) ≡ (x , y)` consists of a
 path `p : a ≡ x`, and a path between `b` and `y` laying over `p`.

src/1Lab/Path/Groupoid.lagda.md

@@ -24,7 +24,7 @@ _ = ap-sym
 ```
 -->
 
-# Types are Groupoids
+# Types are groupoids
 
 The `Path`{.Agda} types equip every `Type`{.Agda} with the structure of
 an _$\infty$-groupoid_. The higher structure of a type begins with its

src/1Lab/Path/IdentitySystem/Strict.lagda.md

@@ -22,7 +22,7 @@ private variable
 ```
 -->
 
-# Strict Identity Systems
+# Strict identity systems
 
 Since [[identity systems]] are a tool for classifying identity _types_,
 the relation underlying an identity system enjoys any additional

src/1Lab/Reflection.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+open import 1Lab.Type.Sigma
 open import 1Lab.Path
 open import 1Lab.Type hiding (absurd)
 
@@ -186,6 +187,9 @@ instance
 # Reflection helpers
 
 ```agda
+Args : Type
+Args = List (Arg Term)
+
 Fun : ∀ {ℓ ℓ'} → Type ℓ → Type ℓ' → Type (ℓ ⊔ ℓ')
 Fun A B = A → B
 
@@ -218,10 +222,13 @@ block-on-meta m = blockTC (blocker-meta m)
 vlam : String → Term → Term
 vlam nam body = lam visible (abs nam body)
 
-infer-hidden : Nat → List (Arg Term) → List (Arg Term)
+infer-hidden : Nat → Args → Args
 infer-hidden zero    xs = xs
 infer-hidden (suc n) xs = unknown h∷ infer-hidden n xs
 
+infer-tel : Telescope → Args
+infer-tel tel = (λ (_ , arg ai _) → arg ai unknown) <$> tel
+
 “refl” : Term
 “refl” = def (quote refl) []
 
@@ -296,9 +303,13 @@ get-boundary : Term → TC (Maybe (Term × Term))
 get-boundary tm = unapply-path tm >>= λ where
   (just (_ , x , y)) → pure (just (x , y))
   nothing            → pure nothing
+
+instance
+  Has-visibility-Telescope : Has-visibility Telescope
+  Has-visibility-Telescope .set-visibility v tel = ×-map₂ (set-visibility v) <$> tel
 ```
 
-## Debugging Tools
+## Debugging tools
 
 ```agda
 debug! : ∀ {ℓ} {A : Type ℓ} → Term → TC A