diff --git a/CITATION.bib b/CITATION.bib new file mode 100644 index 000000000..ebe66f2cf --- /dev/null +++ b/CITATION.bib @@ -0,0 +1,6 @@ +@online{1lab, + author = {{The 1Lab Development Team}}, + title = {{The 1Lab}}, + url = {https://1lab.dev}, + year = 2023, +} diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 833ca57f3..d0d19957b 100644 --- a/CONTRIBUTING.md +++ b/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. diff --git a/src/1Lab/Counterexamples/Russell.lagda.md b/src/1Lab/Counterexamples/Russell.lagda.md index 8f684bd5f..ed2567c43 100644 --- a/src/1Lab/Counterexamples/Russell.lagda.md +++ b/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 diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md index ea2eb9c7a..ec9170648 100644 --- a/src/1Lab/Equiv.lagda.md +++ b/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. diff --git a/src/1Lab/Equiv/Fibrewise.lagda.md b/src/1Lab/Equiv/Fibrewise.lagda.md index 9cffcbe7b..0e9995c4b 100644 --- a/src/1Lab/Equiv/Fibrewise.lagda.md +++ b/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 diff --git a/src/1Lab/Equiv/FromPath.lagda.md b/src/1Lab/Equiv/FromPath.lagda.md index 8b9a6f449..b2da4ba6c 100644 --- a/src/1Lab/Equiv/FromPath.lagda.md +++ b/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 diff --git a/src/1Lab/Equiv/HalfAdjoint.lagda.md b/src/1Lab/Equiv/HalfAdjoint.lagda.md index 43239d9b0..0017f097c 100644 --- a/src/1Lab/Equiv/HalfAdjoint.lagda.md +++ b/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 diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda index 508cd89df..7af01f6b1 100644 --- a/src/1Lab/Extensionality.agda +++ b/src/1Lab/Extensionality.agda @@ -290,6 +290,16 @@ 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} @@ -297,5 +307,4 @@ injection→extensional! → (∀ {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 diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md index 811b87144..eaf96f228 100644 --- a/src/1Lab/HIT/Truncation.lagda.md +++ b/src/1Lab/HIT/Truncation.lagda.md @@ -5,6 +5,7 @@ definition: | --- @@ -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 ∥_∥⁴) ``` diff --git a/src/1Lab/HLevel.lagda.md b/src/1Lab/HLevel.lagda.md index 006dafcc8..1517c9127 100644 --- a/src/1Lab/HLevel.lagda.md +++ b/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.) diff --git a/src/1Lab/HLevel/Retracts.lagda.md b/src/1Lab/HLevel/Retracts.lagda.md index 6f8a15024..a1ddf4462 100644 --- a/src/1Lab/HLevel/Retracts.lagda.md +++ b/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 _) ``` --> diff --git a/src/1Lab/HLevel/Universe.lagda.md b/src/1Lab/HLevel/Universe.lagda.md index 9b6444efa..a74d4a7bf 100644 --- a/src/1Lab/HLevel/Universe.lagda.md +++ b/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 diff --git a/src/1Lab/Path.lagda.md b/src/1Lab/Path.lagda.md index 8c37bb08f..03d154f4a 100644 --- a/src/1Lab/Path.lagda.md +++ b/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 = -# 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`. diff --git a/src/1Lab/Path/Groupoid.lagda.md b/src/1Lab/Path/Groupoid.lagda.md index 348fd5aff..abc96aa29 100644 --- a/src/1Lab/Path/Groupoid.lagda.md +++ b/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 diff --git a/src/1Lab/Path/IdentitySystem/Strict.lagda.md b/src/1Lab/Path/IdentitySystem/Strict.lagda.md index ec6bdc8b0..7816e4e00 100644 --- a/src/1Lab/Path/IdentitySystem/Strict.lagda.md +++ b/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 diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md index 9cfc44174..7303e1a70 100644 --- a/src/1Lab/Reflection.lagda.md +++ b/src/1Lab/Reflection.lagda.md @@ -1,5 +1,6 @@ diff --git a/src/1Lab/Univalence.lagda.md b/src/1Lab/Univalence.lagda.md index f6411511a..8a5d17b92 100644 --- a/src/1Lab/Univalence.lagda.md +++ b/src/1Lab/Univalence.lagda.md @@ -489,7 +489,7 @@ univalence-lift {ℓ = ℓ} = is-iso→is-equiv morp where morp .is-iso.linv x = Path≃Equiv .snd .is-iso.linv _ ``` -## Equivalence Induction {defines="equivalence-induction"} +## Equivalence induction {defines="equivalence-induction"} One useful consequence of $(A \equiv B) \simeq (A \simeq B)$[^2] is that the type of _equivalences_ satisfies [the same induction principle] as @@ -555,7 +555,7 @@ where $B$ is $A$, and $f$ is the identity function. $\id$, which is known to be `an equivalence`{.Agda ident=id-equiv}. $\blacksquare$ -## Object Classifiers {defines="object-classifier"} +## Object classifiers {defines="object-classifier"} In category theory, the idea of _classifiers_ (or _classifying objects_) often comes up when categories applied to the study of logic. For diff --git a/src/1Lab/Univalence/SIP.lagda.md b/src/1Lab/Univalence/SIP.lagda.md index fdc3cf3e2..b98638584 100644 --- a/src/1Lab/Univalence/SIP.lagda.md +++ b/src/1Lab/Univalence/SIP.lagda.md @@ -156,7 +156,7 @@ sip : {σ : Structure ℓ S} → is-univalent σ → {X Y : Σ _ S} → (X ≃[ sip σ = SIP σ .fst ``` -# Structure Combinators +# Structure combinators Univalent structures can be built up in an algebraic manner through the use of _structure combinators_. These express closure of structures @@ -388,7 +388,7 @@ We have a similar phenomenon that happens with NAND and NOR: true true → refl ``` -# Transport Structures +# Transport structures As an alternative to equipping a type family `S : Type → Type` with a notion of S-homomorphism, we can equip it with a notion of _action_. @@ -586,7 +586,7 @@ Function-action-is-transport {S = S} {α = α} {β = β} α-tr β-tr eqv f = ``` -# Adding Axioms +# Adding axioms Most mathematical objects of interest aren't merely sets with structure. More often, the objects we're interested in have _stuff_ (the underlying @@ -666,7 +666,7 @@ transfer-axioms {univ = univ} {axioms = axioms} A B eqv = subst (λ { (x , y) → axioms x y }) (sip univ eqv) (A .snd .snd) ``` -# A Language for Structures +# A language for structures The structure combinators can be abstracted away into a _language_ for defining structures. A `Str-term`{.Agda} describes a structure, that may be @@ -761,7 +761,7 @@ Term→action-is-transport (s s× s₁) = (Term→action-is-transport s) (Term→action-is-transport s₁) ``` -## Descriptions of Structures +## Descriptions of structures To make convenient descriptions of structures-with-axioms, we introduce a record type, `Str-desc`{.Agda}, which packages together the structure diff --git a/src/1Lab/intro.lagda.md b/src/1Lab/intro.lagda.md index f1c1db220..315a23236 100644 --- a/src/1Lab/intro.lagda.md +++ b/src/1Lab/intro.lagda.md @@ -831,7 +831,7 @@ This is, however, an iterative process: For example, our definition of formalising more desirable properties of topoi, we have found that the definition only really mentions two levels. -# Interlude: Basics of Paths +# Interlude: Basics of paths Since the treatment of paths is the most important aspect of homotopy type theory, rest assured that we'll talk about it in more detail later. diff --git a/src/Algebra/Group.lagda.md b/src/Algebra/Group.lagda.md index b7751e3da..00a33b2ef 100644 --- a/src/Algebra/Group.lagda.md +++ b/src/Algebra/Group.lagda.md @@ -134,7 +134,7 @@ instance H-Level-is-group = prop-instance is-group-is-prop ``` -# Group Homomorphisms +# Group homomorphisms In contrast with monoid homomorphisms, for group homomorphisms, it is not necessary for the underlying map to explicitly preserve the unit @@ -287,7 +287,7 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where open make-group using (to-group-on) public ``` -# Symmetric Groups +# Symmetric groups If $X$ is a set, then the type of all bijections $X \simeq X$ is also a set, and it forms the carrier for a group: The _symmetric group_ on $X$. diff --git a/src/Algebra/Group/Action.lagda.md b/src/Algebra/Group/Action.lagda.md index 2d703e0ea..6693bd93f 100644 --- a/src/Algebra/Group/Action.lagda.md +++ b/src/Algebra/Group/Action.lagda.md @@ -41,7 +41,7 @@ which "visually" has the effect of rotating the point $a$ so it lands $x$ radians around the circle, in the counterclockwise direction. Each $x$-radian rotation has an inverse, given by rotation $x$ radians in the clockwise direction; but observe that this is the same as rotating $-x$ -degrees counterclockwise. Addiitonally, observe that rotating by zero +degrees counterclockwise. Additionally, observe that rotating by zero radians does nothing to the circle. We say that $\bb{R}$ _acts_ on the circle by counterclockwise rotation; diff --git a/src/Algebra/Group/Cat/Base.lagda.md b/src/Algebra/Group/Cat/Base.lagda.md index 852f3c25b..b974517dc 100644 --- a/src/Algebra/Group/Cat/Base.lagda.md +++ b/src/Algebra/Group/Cat/Base.lagda.md @@ -23,7 +23,7 @@ import Cat.Reasoning as CR ``` --> -# The category of Groups +# The category of groups The category of groups, as the name implies, has its objects the `Groups`{.Agda ident=Group}, with the morphisms between them the `group diff --git a/src/Algebra/Group/Cat/Monadic.lagda.md b/src/Algebra/Group/Cat/Monadic.lagda.md index 320e06113..a2c4255d3 100644 --- a/src/Algebra/Group/Cat/Monadic.lagda.md +++ b/src/Algebra/Group/Cat/Monadic.lagda.md @@ -179,7 +179,7 @@ but the other direction is by induction on "words". go : rec .hom ≡ x .snd .ν go = funext $ Free-elim-prop _ (λ _ → hlevel 1) (λ x → sym (happly (alg .ν-unit) x)) - (λ x y p q → rec .preserves .is-group-hom.pres-⋆ x y + (λ x p y q → rec .preserves .is-group-hom.pres-⋆ x y ·· ap₂ G._⋆_ p q ·· happly (alg .ν-mult) (inc _ ◆ inc _)) (λ x p → is-group-hom.pres-inv (rec .preserves) {x = x} diff --git a/src/Algebra/Group/Cayley.lagda.md b/src/Algebra/Group/Cayley.lagda.md index 323857505..5a740df4c 100644 --- a/src/Algebra/Group/Cayley.lagda.md +++ b/src/Algebra/Group/Cayley.lagda.md @@ -13,7 +13,7 @@ module Algebra.Group.Cayley {ℓ} (G : Group ℓ) where open Group-on (G .snd) renaming (underlying-set to G-set) ``` -# Cayley's Theorem +# Cayley's theorem Cayley's theorem says that any group $G$ admits a representation as a subgroup of a [symmetric group], specifically the symmetric group acting diff --git a/src/Algebra/Group/Free.lagda.md b/src/Algebra/Group/Free.lagda.md index eed9aaf51..f56466010 100644 --- a/src/Algebra/Group/Free.lagda.md +++ b/src/Algebra/Group/Free.lagda.md @@ -1,5 +1,7 @@ -# Free Groups {defines=free-group-construction} +# Free groups {defines=free-group-construction} We give a direct, higher-inductive constructor of the **free group $F(A)$ on a type $A$ of generators**. While we allow the parameter to be @@ -90,41 +92,23 @@ Free-elim-prop : ∀ {ℓ} (B : Free-group A → Type ℓ) → (∀ x → is-prop (B x)) → (∀ x → B (inc x)) - → (∀ x y → B x → B y → B (x ◆ y)) + → (∀ x → B x → ∀ y → B y → B (x ◆ y)) → (∀ x → B x → B (inv x)) → B nil → ∀ x → B x ``` -
- The proof of it is a direct (by which I mean repetitive) case analysis, -so I've put it in a `
`{.html} tag. -
 +so we let our reflection machinery handle it for us. ```agda -Free-elim-prop B bp bi bd binv bnil = go where - go : ∀ x → B x - go (inc x) = bi x - go (x ◆ y) = bd x y (go x) (go y) - go (inv x) = binv x (go x) - go nil = bnil - go (f-assoc x y z i) = - is-prop→pathp (λ i → bp (f-assoc x y z i)) - (bd x (y ◆ z) (go x) (bd y z (go y) (go z))) - (bd (x ◆ y) z (bd x y (go x) (go y)) (go z)) - i - go (f-invl x i) = - is-prop→pathp (λ i → bp (f-invl x i)) (bd (inv x) x (binv x (go x)) (go x)) bnil i - go (f-idl x i) = is-prop→pathp (λ i → bp (f-idl x i)) (bd nil x bnil (go x)) (go x) i - go (squash x y p q i j) = - is-prop→squarep (λ i j → bp (squash x y p q i j)) - (λ i → go x) (λ i → go (p i)) (λ i → go (q i)) (λ i → go y) i j +unquoteDef Free-elim-prop = make-elim-with (default-elim-visible into 1) + Free-elim-prop (quote Free-group) ```
-## Universal Property {defines=free-group} +## Universal property {defines=free-group} We now prove the universal property of `Free-group`{.Agda}, or, more specifically, of the map `inc`{.Agda}: It gives a [universal way of @@ -193,7 +177,7 @@ make-free-group .Ml.commutes f = refl make-free-group .Ml.unique {y = y} {g = g} p = ext $ Free-elim-prop _ (λ _ → hlevel!) (p $ₚ_) - (λ a b p q → ap₂ y._⋆_ p q ∙ sym (g .preserves .is-group-hom.pres-⋆ _ _)) + (λ a p b q → ap₂ y._⋆_ p q ∙ sym (g .preserves .is-group-hom.pres-⋆ _ _)) (λ a p → ap y.inverse p ∙ sym (is-group-hom.pres-inv (g .preserves))) (sym (is-group-hom.pres-id (g .preserves))) where module y = Group-on (y .snd) diff --git a/src/Algebra/Group/Homotopy.lagda.md b/src/Algebra/Group/Homotopy.lagda.md index f5438546d..8184bf0c7 100644 --- a/src/Algebra/Group/Homotopy.lagda.md +++ b/src/Algebra/Group/Homotopy.lagda.md @@ -1,5 +1,6 @@ -# Homotopy Groups {defines="homotopy-group fundamental-group"} +# Homotopy groups {defines="homotopy-group fundamental-group"} Given a `pointed type`{.Agda ident=Type∙} $(A, a)$ we refer to the type $a = a$ as the **loop space of $A$**, and refer to it in short as @@ -236,26 +237,16 @@ eliminator into propositions later, so we define that now. → SquareP (λ i j → P (path-sq x y i j)) (λ _ → p) (ploop x) (ploop (x ⋆ y)) (ploop y)) → ∀ x → P x - Deloop-elim P grpd pp ploop psq base = pp - Deloop-elim P grpd pp ploop psq (path x i) = ploop x i - Deloop-elim P grpd pp ploop psq (path-sq x y i j) = psq x y i j - Deloop-elim P grpd pp ploop psq (squash a b p q r s i j k) = - is-hlevel→is-hlevel-dep 2 grpd - (g a) (g b) (λ i → g (p i)) (λ i → g (q i)) - (λ i j → g (r i j)) (λ i j → g (s i j)) (squash a b p q r s) i j k - where - g = Deloop-elim P grpd pp ploop psq + unquoteDef Deloop-elim = make-elim-with (default-elim-visible into 3) + Deloop-elim (quote Deloop) Deloop-elim-prop : ∀ {ℓ'} (P : Deloop → Type ℓ') → (∀ x → is-prop (P x)) → P base → ∀ x → P x - Deloop-elim-prop P pprop p = - Deloop-elim P - (λ x → is-prop→is-hlevel-suc {n = 2} (pprop x)) p - (λ x → is-prop→pathp (λ i → pprop (path x i)) p p) - (λ x y → is-prop→squarep (λ i j → pprop (path-sq x y i j)) _ _ _ _) + unquoteDef Deloop-elim-prop = make-elim-with (default-elim-visible into 1) + Deloop-elim-prop (quote Deloop) ``` We can then proceed to characterise the type `point ≡ x` by an diff --git a/src/Algebra/Group/NAry.lagda.md b/src/Algebra/Group/NAry.lagda.md index 7f486e121..c0b619438 100644 --- a/src/Algebra/Group/NAry.lagda.md +++ b/src/Algebra/Group/NAry.lagda.md @@ -13,7 +13,7 @@ open import Data.Fin module Algebra.Group.NAry where ``` -# n-Ary Sums +# n-Ary sums An important property of [[abelian groups]] (really, of abelian _monoids_, but we will only need them for [[groups]]) is that their diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md index b72281fb9..7c1aada48 100644 --- a/src/Algebra/Group/Subgroup.lagda.md +++ b/src/Algebra/Group/Subgroup.lagda.md @@ -85,7 +85,7 @@ predicate→subgroup {G = G} H p = record { map = it ; monic = ism } where ism = Homomorphism-monic it (λ p → Σ-prop-path (λ _ → hlevel!) p) ``` -# Kernels and Images +# Kernels and images To a group homomorphism $f : A \to B$ we can associate two canonical subgroups, one of $A$ and one of $B$: $f$'s [[**image factorisation**]], diff --git a/src/Algebra/Magma/Unital.lagda.md b/src/Algebra/Magma/Unital.lagda.md index 3a64b8e59..7138cd9ae 100644 --- a/src/Algebra/Magma/Unital.lagda.md +++ b/src/Algebra/Magma/Unital.lagda.md @@ -18,7 +18,7 @@ private variable ``` --> -# Unital Magmas +# Unital magmas A **unital magma** is a `magma`{.Agda ident=is-magma} equipped with a _two-sided identity element_, that is, an element $e$ such that diff --git a/src/Algebra/Magma/Unital/EckmannHilton.lagda.md b/src/Algebra/Magma/Unital/EckmannHilton.lagda.md index 7c9c118f9..5cd652b64 100644 --- a/src/Algebra/Magma/Unital/EckmannHilton.lagda.md +++ b/src/Algebra/Magma/Unital/EckmannHilton.lagda.md @@ -12,7 +12,7 @@ open import Algebra.Monoid module Algebra.Magma.Unital.EckmannHilton where ``` -# The Eckmann-Hilton Argument +# The Eckmann-Hilton argument The **Eckmann-Hilton argument** shows that two `unital magmas`{.Agda ident=is-unital-magma} on the same carrier type that diff --git a/src/Algebra/Monoid.lagda.md b/src/Algebra/Monoid.lagda.md index 5b13b1705..fc21a9510 100644 --- a/src/Algebra/Monoid.lagda.md +++ b/src/Algebra/Monoid.lagda.md @@ -108,7 +108,7 @@ Monoid≃ : (A B : Monoid ℓ) (e : A .fst ≃ B .fst) → Type _ Monoid≃ A B (e , _) = Monoid-hom (A .snd) (B .snd) e ``` -# Relationships to Unital Magmas +# Relationships to unital magmas ```agda open import Algebra.Magma.Unital diff --git a/src/Authors.lagda.md b/src/Authors.lagda.md index 719aee8ab..dd3fec754 100644 --- a/src/Authors.lagda.md +++ b/src/Authors.lagda.md @@ -2,7 +2,7 @@ module Authors where ``` -# About the Authors +# About the authors This is a page where everyone who adds to the 1lab can write a little bit about themselves. I mean it: everyone can write a bit about diff --git a/src/Cat/Abelian/Functor.lagda.md b/src/Cat/Abelian/Functor.lagda.md index 008f59b42..f04e29ec4 100644 --- a/src/Cat/Abelian/Functor.lagda.md +++ b/src/Cat/Abelian/Functor.lagda.md @@ -14,7 +14,7 @@ open import Cat.Prelude module Cat.Abelian.Functor where ``` -# Ab-enriched Functors +# Ab-enriched functors Since [$\Ab$-categories] are additionally equipped with the structure of [[abelian groups]] on their $\hom$-sets, it's natural that we ask that diff --git a/src/Cat/Allegory/Morphism.lagda.md b/src/Cat/Allegory/Morphism.lagda.md index fff0eca02..b4b5c1617 100644 --- a/src/Cat/Allegory/Morphism.lagda.md +++ b/src/Cat/Allegory/Morphism.lagda.md @@ -23,12 +23,12 @@ private variable ``` --> -# Morphisms in an Allegory +# Morphisms in an allegory This module defines a couple of important classes of morphisms that can be found in an allegory. -# Reflexive Morphisms +# Reflexive morphisms A morphism $f : X \to X$ in an allegory is **reflexive** if $id \le f$. @@ -85,7 +85,7 @@ reflexive→diagonal f-refl = ∩-univ f-refl (reflexive-dual f-refl) ``` -# Symmetric Morphisms +# Symmetric morphisms A morphism $f : X \to X$ is **symmetric** if $f \le f^o$. @@ -145,7 +145,7 @@ symmetric→self-dual f-sym = ≤-antisym f-sym (dual-≤ₗ A f-sym) ``` -# Transitive Morphisms +# Transitive morphisms A morphism $f : X \to X$ is **transitive** if $ff \le f$. @@ -283,7 +283,7 @@ transitive+symmetric→cotransitive {f = f} f-trans f-sym = f ∘ f ≤∎ ``` -# Coreflexive Morphisms +# Coreflexive morphisms ```agda is-coreflexive : Hom x x → Type _ @@ -403,7 +403,7 @@ coreflexive-comm f-corefl g-corefl = ·· sym (coreflexive-∘-∩ g-corefl f-corefl) ``` -# Functional Morphisms +# Functional morphisms A morphism $$ is **functional** when $ff^o \le id$. In $\Rel$, these are the relations $R \mono X \times Y$ such that every $x$ is related to @@ -452,7 +452,7 @@ functional-∩ {f = f} {g = g} f-func g-func = id ≤∎ ``` -# Entire Morphisms +# Entire morphisms A morphism is **entire** when $id \le f^of$. In $\Rel$, these are the relations $R \mono X \times Y$ where each $x$ must be related to at least @@ -714,7 +714,7 @@ domain-entire f-entire = (∩-univ ≤-refl f-entire) ``` -# Antisymmetric Morphisms +# Antisymmetric morphisms A morphism is **anti-symmetric** if $f \cap f^o \le id$. diff --git a/src/Cat/Diagram/Colimit/Base.lagda.md b/src/Cat/Diagram/Colimit/Base.lagda.md index 917a5084f..ef039e356 100644 --- a/src/Cat/Diagram/Colimit/Base.lagda.md +++ b/src/Cat/Diagram/Colimit/Base.lagda.md @@ -546,7 +546,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory ``` -# Preservation of Colimits +# Preservation of colimits The definitions here are the same idea as [preservation of limits], just dualized. diff --git a/src/Cat/Diagram/Colimit/Cocone.lagda.md b/src/Cat/Diagram/Colimit/Cocone.lagda.md index 7577e38f6..c1df591cc 100644 --- a/src/Cat/Diagram/Colimit/Cocone.lagda.md +++ b/src/Cat/Diagram/Colimit/Cocone.lagda.md @@ -22,7 +22,7 @@ open _=>_ ``` --> -# Colimits via Cocones +# Colimits via cocones As noted in the main page on [[colimits]], most introductory texts opt to define colimits via categorical gadgets called **cocones**. A @@ -67,7 +67,7 @@ module _ {J : Precategory o ℓ} {C : Precategory o' ℓ'} (F : Functor J C) whe ``` --> -## Cocone Maps +## Cocone maps To express the universal property of a colimit in terms of cocones, we now have to define the notion of **cocone homomorphism**. We define a @@ -128,7 +128,7 @@ category, it's immediate that they form a category. --> -## Initial Cocones as Colimits +## Initial cocones as colimits A cocone over some diagram $F$ contains the same data as natural transformation from $F$ to a constant functor. Since we have defined a diff --git a/src/Cat/Diagram/Colimit/Finite.lagda.md b/src/Cat/Diagram/Colimit/Finite.lagda.md index b9e949aeb..7d8e9538f 100644 --- a/src/Cat/Diagram/Colimit/Finite.lagda.md +++ b/src/Cat/Diagram/Colimit/Finite.lagda.md @@ -24,7 +24,7 @@ module _ {ℓ ℓ'} (C : Precategory ℓ ℓ') where ``` --> -# Finitely Cocomplete Categories {defines="finite-colimit finitely-cocomplete finitely-cocomplete-category"} +# Finitely cocomplete categories {defines="finite-colimit finitely-cocomplete finitely-cocomplete-category"} Finitely **cocomplete** categories are dual to [[finitely complete categories]] in that they admit colimits for all diagrams of diff --git a/src/Cat/Diagram/Colimit/Representable.lagda.md b/src/Cat/Diagram/Colimit/Representable.lagda.md index 69078b0f2..56a4b2bcc 100644 --- a/src/Cat/Diagram/Colimit/Representable.lagda.md +++ b/src/Cat/Diagram/Colimit/Representable.lagda.md @@ -17,7 +17,7 @@ import Cat.Reasoning module Cat.Diagram.Colimit.Representable where ``` -## Representability of Colimits +## Representability of colimits Since [colimits] are defined by universal property, we can also phrase the definition in terms of an equivalence between $\hom$-functors. diff --git a/src/Cat/Diagram/Limit/Base.lagda.md b/src/Cat/Diagram/Limit/Base.lagda.md index 149204c82..62ef1262e 100644 --- a/src/Cat/Diagram/Limit/Base.lagda.md +++ b/src/Cat/Diagram/Limit/Base.lagda.md @@ -669,7 +669,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory ``` -# Preservation of Limits +# Preservation of limits -## Terminal Cones as Limits +## Terminal cones as limits Note that cones over some diagram $F$ contain the exact same data as natural transformations from a constant functor to $F$. To obtain a diff --git a/src/Cat/Diagram/Limit/Finite.lagda.md b/src/Cat/Diagram/Limit/Finite.lagda.md index 0e5a93673..e524c666a 100644 --- a/src/Cat/Diagram/Limit/Finite.lagda.md +++ b/src/Cat/Diagram/Limit/Finite.lagda.md @@ -39,7 +39,7 @@ module _ {ℓ ℓ'} (C : Precategory ℓ ℓ') where ``` --> -# Finitely Complete Categories {defines="finite-limit finitely-complete finitely-complete-category"} +# Finitely complete categories {defines="finite-limit finitely-complete finitely-complete-category"} A category is said to be **finitely complete** if it admits limits for every diagram with a [[finite|finite category]] shape. diff --git a/src/Cat/Diagram/Monad.lagda.md b/src/Cat/Diagram/Monad.lagda.md index 84612ae18..928361497 100644 --- a/src/Cat/Diagram/Monad.lagda.md +++ b/src/Cat/Diagram/Monad.lagda.md @@ -118,7 +118,7 @@ doesn't matter whether you first join then evaluate, or evaluate twice. ``` --> -# Eilenberg-Moore Category +# Eilenberg-Moore category If we take a monad $M$ as the signature of an (algebraic) theory, and $M$-algebras as giving _models_ of that theory, then we can ask (like @@ -214,6 +214,12 @@ module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where → Extensionality (Algebra-hom C M (a , A) (b , B)) extensionality-algebra-hom = record { lemma = quote Extensional-Algebra-Hom } + instance + Funlike-Algebra-hom : ⦃ i : Funlike C.Hom ⦄ → Funlike (Algebra-hom C M) + Funlike-Algebra-hom ⦃ i ⦄ .Funlike.au = Underlying-Σ ⦃ ua = Funlike.au i ⦄ + Funlike-Algebra-hom ⦃ i ⦄ .Funlike.bu = Underlying-Σ ⦃ ua = Funlike.bu i ⦄ + Funlike-Algebra-hom ⦃ i ⦄ .Funlike._#_ f x = f .morphism # x + module _ {o ℓ} (C : Precategory o ℓ) where private module C = Cat.Reasoning C private unquoteDecl eqv = declare-record-iso eqv (quote Algebra-hom) @@ -294,7 +300,7 @@ faithful. Forget-is-faithful = ext ``` -## Free Algebras +## Free algebras In exactly the same way that we may construct a _[free group]_ by taking the inhabitants of some set $X$ as generating the "words" of a group, we diff --git a/src/Cat/Diagram/Product/Solver.lagda.md b/src/Cat/Diagram/Product/Solver.lagda.md index ed77bad09..c70e6ae19 100644 --- a/src/Cat/Diagram/Product/Solver.lagda.md +++ b/src/Cat/Diagram/Product/Solver.lagda.md @@ -15,7 +15,7 @@ import Cat.Reasoning module Cat.Diagram.Product.Solver where ``` -# A Solver for Categories with Binary Products +# A solver for categories with binary products Much like the [category solver], this module is split into two halves. The first implements an algorithm for normalizing expressions in the @@ -247,7 +247,7 @@ morphism as naively interpreting the expression. sound X Y e = sound-k X X Y e vid ∙ elimr (vhom-sound X X id) ``` -## Solver Interface +## Solver interface In order to make the reflection easier later, we bundle up the soundness proof. Marking this as abstract is *very important*. This prevents diff --git a/src/Cat/Diagram/Zero.lagda.md b/src/Cat/Diagram/Zero.lagda.md index bc17b0369..622a8b84a 100644 --- a/src/Cat/Diagram/Zero.lagda.md +++ b/src/Cat/Diagram/Zero.lagda.md @@ -17,7 +17,7 @@ open import Cat.Reasoning C ``` --> -# Zero Objects +# Zero objects In some categories, `Initial`{.Agda} and `Terminal`{.Agda} objects coincide. When this occurs, we call the object a **zero object**. diff --git a/src/Cat/Displayed/Adjoint.lagda.md b/src/Cat/Displayed/Adjoint.lagda.md index 011ed4171..6d0362a21 100644 --- a/src/Cat/Displayed/Adjoint.lagda.md +++ b/src/Cat/Displayed/Adjoint.lagda.md @@ -13,7 +13,7 @@ open import Cat.Prelude module Cat.Displayed.Adjoint where ``` -# Displayed Adjunctions +# Displayed adjunctions Following the general theme of defining displayed structure over 1-categorical structure, we can define a notion of displayed @@ -84,7 +84,7 @@ module _ → (R' .F₁' (counit'.ε' x') ℰ.∘' unit'.η' (R' .F₀' x')) ℰ.≡[ zag ] ℰ.id' ``` -## Fibred Adjunctions {defines="fibred-adjunction fibred-left-adjoint fibred-right-adjoint"} +## Fibred adjunctions {defines="fibred-adjunction fibred-left-adjoint fibred-right-adjoint"} Let $\cE$ and $\cF$ be categories displayed over some $\cB$. We say that a pair of vertical [[fibred functors]] $L : \cE \to \cF$, $R : \cF diff --git a/src/Cat/Displayed/Base.lagda.md b/src/Cat/Displayed/Base.lagda.md index 391ccb6a3..6c88ff16e 100644 --- a/src/Cat/Displayed/Base.lagda.md +++ b/src/Cat/Displayed/Base.lagda.md @@ -12,7 +12,7 @@ open import Cat.Base module Cat.Displayed.Base where ``` -# Displayed Categories {defines=displayed-category} +# Displayed categories {defines=displayed-category} The core idea behind displayed categories is that we want to capture the idea of being able to place extra structure over some sort of "base" diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md index 7d5cb942e..f3703180c 100644 --- a/src/Cat/Displayed/Bifibration.lagda.md +++ b/src/Cat/Displayed/Bifibration.lagda.md @@ -73,7 +73,7 @@ record is-bifibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where module opfibration = Cocartesian-fibration opfibration ``` -# Bifibrations and Adjoints +# Bifibrations and adjoints If $\cE$ is a bifibration, then its opreindexing functors are [[left adjoints]] to its reindexing functors. To show this, it will suffice to diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md index 0b2b039ed..365b4c4ac 100644 --- a/src/Cat/Displayed/Cartesian.lagda.md +++ b/src/Cat/Displayed/Cartesian.lagda.md @@ -253,7 +253,7 @@ Cartesian-morphism-is-set = Iso→is-hlevel 2 eqv $ ``` --> -## Properties of Cartesian Morphisms +## Properties of cartesian morphisms The composite of 2 cartesian morphisms is in turn cartesian. diff --git a/src/Cat/Displayed/Cartesian/Discrete.lagda.md b/src/Cat/Displayed/Cartesian/Discrete.lagda.md index a0fbf2deb..14cb6d293 100644 --- a/src/Cat/Displayed/Cartesian/Discrete.lagda.md +++ b/src/Cat/Displayed/Cartesian/Discrete.lagda.md @@ -77,7 +77,7 @@ module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where → is-contr (Σ[ x' ∈ E.Ob[ x ] ] E.Hom[ f ] x' y') ``` -## Discrete fibrations are Cartesian +## Discrete fibrations are cartesian To prove that discrete fibrations deserve the name discrete _fibrations_, we prove that any discrete fibration is a [[Cartesian @@ -172,7 +172,7 @@ are unique, we have $f = g$. where open Discrete-fibration disc ``` -## Morphisms in Discrete Fibrations +## Morphisms in discrete fibrations If $\cE$ is a discrete fibration, then the only vertical morphisms are identities. This follows directly from lifts being contractible. @@ -204,7 +204,7 @@ that every vertical morphism in a discrete fibration is invertible. x''≡x' = ap fst (discrete→vertical-id disc (x' , f')) ``` -## Discrete Fibrations are Presheaves +## Discrete fibrations are presheaves As noted earlier, a discrete fibration over $\cB$ encodes the same data as a presheaf on $\cB$. First, let us show that we can construct diff --git a/src/Cat/Displayed/Cartesian/Identity.lagda.md b/src/Cat/Displayed/Cartesian/Identity.lagda.md index bfdb5338b..1114864d7 100644 --- a/src/Cat/Displayed/Cartesian/Identity.lagda.md +++ b/src/Cat/Displayed/Cartesian/Identity.lagda.md @@ -18,7 +18,7 @@ module Cat.Displayed.Cartesian.Identity where ``` -# Identity of Cartesian lifts +# Identity of cartesian lifts In this module, we prove that [[Cartesian morphisms]] are unique up to _vertical_ isomorphism, which, if the [[displayed category]] is univalent diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md index 766236f1e..37d337c85 100644 --- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md @@ -41,7 +41,7 @@ private ``` --> -# Reindexing for Cartesian fibrations +# Reindexing for cartesian fibrations A [[cartesian fibration]] can be thought of as a [[displayed category]] $\cE$ whose [[fibre categories]] $\cE^*(b)$ depend ([pseudo])functorially diff --git a/src/Cat/Displayed/Cartesian/Right.lagda.md b/src/Cat/Displayed/Cartesian/Right.lagda.md index 7b7f1511f..e0b19d966 100644 --- a/src/Cat/Displayed/Cartesian/Right.lagda.md +++ b/src/Cat/Displayed/Cartesian/Right.lagda.md @@ -30,7 +30,7 @@ open Cat.Displayed.Morphism ℰ open Cat.Displayed.Reasoning ℰ ``` -# Right Fibrations +# Right fibrations A [[cartesian fibration]] $\cE$ is said to be a **right fibration** if every morphism in $\cE$ is cartesian. @@ -133,7 +133,7 @@ discrete→right-fibration dfib = (discrete→vertical-invertible ℰ dfib) ``` -## Fibred Functors and Right Fibrations +## Fibred functors and right fibrations As every map in a right fibration is cartesian, every [[displayed functor]] into a right fibration is automatically fibred. diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md index 0d26785a7..12673508c 100644 --- a/src/Cat/Displayed/Cartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cartesian/Weak.lagda.md @@ -38,7 +38,7 @@ private module Fib = FibR ℰ ``` --> -# Weak Cartesian Morphisms +# Weak cartesian morphisms Some authors use a weaker notion of [[cartesian morphism]] when defining fibrations, referred to as a "weak cartesian" or "hypocartesian" @@ -200,7 +200,7 @@ weak-cartesian→postcompose-equiv wcart = (λ h' → sym $ wcart .unique _ (to-pathp refl)) ``` -## Weak Cartesian Lifts {defines=weak-cartesian-fibration} +## Weak cartesian lifts {defines=weak-cartesian-fibration} We can also define a notion of weak cartesian lifts, much like we can with their stronger cousins. @@ -443,7 +443,7 @@ a cartesian lift of $f$. f-lift .Cartesian-lift.cartesian = f*-cartesian ``` -## Factorisations in Weak Fibrations +## Factorisations in weak fibrations If $\cE$ is a weak fibration, then every morphism factorizes into a vertical morphism followed by a weak cartesian morphism. @@ -489,7 +489,7 @@ weak-fibration→weak-cartesian-factors {y' = y'} {f = f} wfib f' = weak-factor weak-factor .factors = symP $ f-lift.commutes f' ``` -## Weak Fibrations and Equivalence of Hom Sets +## Weak fibrations and equivalence of Hom sets If $\cE$ is a weak fibration, then the hom sets $x' \to_f y'$ and $x' \to_{id} f^{*}(y')$ are equivalent, where $f^{*}(y')$ is the domain diff --git a/src/Cat/Displayed/Cocartesian.lagda.md b/src/Cat/Displayed/Cocartesian.lagda.md index da0a899aa..b3a09f77f 100644 --- a/src/Cat/Displayed/Cocartesian.lagda.md +++ b/src/Cat/Displayed/Cocartesian.lagda.md @@ -249,7 +249,7 @@ co-cartesian≡cocartesian = ua (co-cartesian→cocartesian , co-cartesian→cocartesian-is-equiv) ``` -## Properties of Cocartesian Morphisms +## Properties of cocartesian morphisms We shall now prove the following properties of cocartesian morphisms. @@ -374,7 +374,7 @@ cocartesian→precompose-equiv cocart = ``` -## Cocartesian Lifts +## Cocartesian lifts We call an object $b'$ over $b$ together with a cartesian arrow $f' : a \to_{f} b'$ a **cocartesian lift** of $f$. diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md index ead76f168..3228ec13d 100644 --- a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md @@ -27,7 +27,7 @@ open Functor ``` --> -# Opreindexing for Cocartesian fibrations +# Opreindexing for cocartesian fibrations [Opfibrations] are dual to [fibrations], so they inherit the ability to [reindex along morphisms in the base]. However, this reindexing is diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md index 0a9d70e38..fa72fb900 100644 --- a/src/Cat/Displayed/Cocartesian/Weak.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Weak.lagda.md @@ -41,7 +41,7 @@ private ``` --> -# Weak Cocartesian Morphisms +# Weak cocartesian morphisms We can define a weaker notion of [cocartesian morphism] much like we can with their [cartesian counterparts]. @@ -616,7 +616,7 @@ cartesian+weak-opfibration→opfibration fib wlifts = (fibration+weak-cocartesian→cocartesian fib g-weak) ``` -# Weak Opfibrations and Equivalence of Hom Sets +# Weak opfibrations and equivalence of Hom sets If $\cE$ is a weak opfibration, then the hom sets $x' \to_f y'$ and $f^{*}(x') \to_{id} y'$ are equivalent, where $f^{*}(x')$ is the codomain diff --git a/src/Cat/Displayed/Composition.lagda.md b/src/Cat/Displayed/Composition.lagda.md index c9c995025..2ccaf1890 100644 --- a/src/Cat/Displayed/Composition.lagda.md +++ b/src/Cat/Displayed/Composition.lagda.md @@ -14,7 +14,7 @@ import Cat.Displayed.Reasoning as DR module Cat.Displayed.Composition where ``` -# Composition of Displayed Categories +# Composition of displayed categories A [[displayed category]] $\cE$ over $\cB$ is equivalent to the data of a functor into $\cB$; the forward direction of this equivalence is diff --git a/src/Cat/Displayed/Comprehension.lagda.md b/src/Cat/Displayed/Comprehension.lagda.md index 3bf373eef..ced0dae73 100644 --- a/src/Cat/Displayed/Comprehension.lagda.md +++ b/src/Cat/Displayed/Comprehension.lagda.md @@ -380,7 +380,7 @@ of is a projection $\Gamma.A \to \Gamma$. sub-proj f ``` -## Comprehension structures as Comonads +## Comprehension structures as comonads Comprehension structures on fibrations $\cE$ induce [comonads] on the [[total category]] of $\cE$. These comonads are particularly nice: all diff --git a/src/Cat/Displayed/Comprehension/Coproduct/VeryStrong.lagda.md b/src/Cat/Displayed/Comprehension/Coproduct/VeryStrong.lagda.md index 7f70623ef..2ae4141e4 100644 --- a/src/Cat/Displayed/Comprehension/Coproduct/VeryStrong.lagda.md +++ b/src/Cat/Displayed/Comprehension/Coproduct/VeryStrong.lagda.md @@ -20,7 +20,7 @@ import Cat.Reasoning module Cat.Displayed.Comprehension.Coproduct.VeryStrong where ``` -# Very Strong Comprehension Coproducts {defines="very-strong-comprehension-coproduct"} +# Very strong comprehension coproducts {defines="very-strong-comprehension-coproduct"} As noted in [[strong comprehension coproducts]], the elimination principle for [[comprehension coproducts]] is quite weak, being more of diff --git a/src/Cat/Displayed/Functor.lagda.md b/src/Cat/Displayed/Functor.lagda.md index 821b85730..e068044f9 100644 --- a/src/Cat/Displayed/Functor.lagda.md +++ b/src/Cat/Displayed/Functor.lagda.md @@ -244,7 +244,7 @@ The identity functor is obviously fibred. ``` -## Vertical Functors +## Vertical functors Functors displayed over the identity functor are of particular interest. Such functors are known as **vertical functors**, and are commonly used @@ -533,7 +533,7 @@ module _ IdVf = Fibred→Vertical-fibred Idf' ``` -## Displayed Natural Transformations +## Displayed natural transformations Just like we have defined a [displayed functor][disfct] $\bf{F} : \cE \to \cF$ lying over an ordinary functor $F : \cA \to \cB$ diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md index 7de32b081..d3069e155 100644 --- a/src/Cat/Displayed/GenericObject.lagda.md +++ b/src/Cat/Displayed/GenericObject.lagda.md @@ -27,7 +27,7 @@ open Functor ``` --> -# Generic Objects +# Generic objects There are 2 perspectives one can take on generic objects. The first is a purely logical one: generic objects provide us a tool for giving @@ -149,7 +149,7 @@ complexity of this sentence is a bit high, so please refer to the code: ``` --> -## Skeletal Generic Objects +## Skeletal generic objects We say that a generic object $t'$ is **skeletal** if the classifying map in the base category is unique: if $u : x \to t$ underlies a Cartesian @@ -184,7 +184,7 @@ is-skeletal-generic-object-is-prop = hlevel! ``` --> -## Gaunt Generic Objects +## Gaunt generic objects A generic object is **gaunt** if the classifying maps _themselves_ are unique. This condition expands on that of skeletality: if $u' : x' \to_u @@ -240,7 +240,7 @@ is-gaunt-generic-object-is-prop → is-prop (is-gaunt-generic-object gobj) is-gaunt-generic-object-is-prop = Iso→is-hlevel 1 eqv $ Σ-is-hlevel 1 hlevel! λ _ → - Π-is-hlevel' 1 λ _ → Π-is-hlevel' 1 λ _ → Π-is-hlevel' 1 λ _ → Π-is-hlevel' 1 λ _ → + Π-is-hlevel' 1 λ _ → Π-is-hlevel³' 1 λ _ _ _ → Π-is-hlevel 1 λ _ → PathP-is-hlevel' 1 (Hom[ _ ]-set _ _) _ _ where unquoteDecl eqv = declare-record-iso eqv (quote is-gaunt-generic-object) diff --git a/src/Cat/Displayed/Instances/CT-Structure.lagda.md b/src/Cat/Displayed/Instances/CT-Structure.lagda.md index ade9a9670..e48449345 100644 --- a/src/Cat/Displayed/Instances/CT-Structure.lagda.md +++ b/src/Cat/Displayed/Instances/CT-Structure.lagda.md @@ -25,7 +25,7 @@ open Binary-products B has-prods open Simple B has-prods ``` -# CT Structures +# CT structures CT-Structures are a refinement of [simple fibrations], which allow us to model type theories where the contexts aren't necessarily @@ -74,7 +74,7 @@ Simple-ct ct .Displayed.assoc' {f = u} {g = v} {h = w} f g h = (f ∘ ⟨ v ∘ π₁ , g ⟩) ∘ ⟨ w ∘ π₁ , h ⟩ ∎ ``` -# Cartesian Maps +# Cartesian maps If a map is cartesian in the simple fibration, then it is cartesian in a simple CT fibration. @@ -96,7 +96,7 @@ Simple-cartesian→Simple-ct-cartesian ct x-tp y-tp cart = ct-cart where ``` -# Fibration Structure +# Fibration structure Much like the simple fibration, the simple fibration associated to a CT-structure also deserves its name. diff --git a/src/Cat/Displayed/Instances/Chaotic.lagda.md b/src/Cat/Displayed/Instances/Chaotic.lagda.md index addb50357..447da5215 100644 --- a/src/Cat/Displayed/Instances/Chaotic.lagda.md +++ b/src/Cat/Displayed/Instances/Chaotic.lagda.md @@ -28,7 +28,7 @@ open Displayed open Total-hom ``` -# The Chaotic Bifibration +# The chaotic bifibration Let $\cB$ and $\cJ$ be precategories. We define the **chaotic bifibration** of $\cJ$ over $\cB$ to be the [[displayed @@ -149,7 +149,7 @@ Chaotic-bifibration .is-bifibration.fibration = Chaotic-fibration Chaotic-bifibration .is-bifibration.opfibration = Chaotic-opfibration ``` -## Fibre Categories +## Fibre categories Unsurprisingly, the [[fibre categories]] of the chaotic bifibration are isomorphic to $\cJ$. @@ -166,7 +166,7 @@ ChaoticFib-is-iso x .is-precat-iso.has-is-ff = id-equiv ChaoticFib-is-iso x .is-precat-iso.has-is-iso = id-equiv ``` -## Total Category +## Total category The [[total category]] of the chaotic bifibration is isomorphic to the product of $\cB$ and $\cJ$. diff --git a/src/Cat/Displayed/Instances/Diagrams.lagda.md b/src/Cat/Displayed/Instances/Diagrams.lagda.md index f2f615c21..c02d8ccf5 100644 --- a/src/Cat/Displayed/Instances/Diagrams.lagda.md +++ b/src/Cat/Displayed/Instances/Diagrams.lagda.md @@ -28,7 +28,7 @@ open Functor open _=>_ ``` -# The Diagram Fibration +# The diagram fibration The appropriate notion of structure for a [[displayed category]] $\cE \liesover \cB$ is fibrewise structure: structure found in each [[fibre @@ -173,7 +173,7 @@ functor. ``` --> -## Fibre Categories +## Fibre categories The fibre category of the fibration of diagrams are equivalent to functor categories $[\cJ, \cE_x]$. diff --git a/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md b/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md index e90e91faf..50d493f07 100644 --- a/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md +++ b/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md @@ -35,7 +35,7 @@ open Slice-hom ``` --> -# The Displayed Family Fibration +# The displayed family fibration The [family fibration] is a critical part of the theory of fibrations, as it acts as a stepping off point for generalizing structure found @@ -180,7 +180,7 @@ module _ fibration-∘ (Codomain-fibration B pb) (Change-of-base-fibration Dom E fib) ``` -## Constant Families +## Constant families There is a vertical functor from $\cE$ to the category of $\cE$-valued families that takes each $\cE_{x}$ to the constant family. diff --git a/src/Cat/Displayed/Instances/Elements.lagda.md b/src/Cat/Displayed/Instances/Elements.lagda.md index 448b745c2..ef57c8405 100644 --- a/src/Cat/Displayed/Instances/Elements.lagda.md +++ b/src/Cat/Displayed/Instances/Elements.lagda.md @@ -24,7 +24,7 @@ private ``` --> -# The Displayed Category of Elements +# The displayed category of elements It is useful to view the [category of elements] of a presheaf `P`{.Agda} as a [[displayed category]]. Instead of considering pairs of diff --git a/src/Cat/Displayed/Instances/Identity.lagda.md b/src/Cat/Displayed/Instances/Identity.lagda.md index 9ad746a85..85381fea0 100644 --- a/src/Cat/Displayed/Instances/Identity.lagda.md +++ b/src/Cat/Displayed/Instances/Identity.lagda.md @@ -24,7 +24,7 @@ open Functor open Total-hom ``` -## The Identity Bifibration +## The identity bifibration Let $\cB$ be a precategory. We can define a [[displayed category]] $\mathrm{Id}(\cB)$ over $B$ whose [[total category]] is isomorphic to @@ -95,7 +95,7 @@ IdD-bifibration .is-bifibration.opfibration = IdD-opfibration ``` --> -## Fibre Categories +## Fibre categories The [[fibre categories]] of the identity bifibration are isomorphic to the [[terminal category]]. @@ -112,7 +112,7 @@ IdD-is-iso x .is-precat-iso.has-is-ff = id-equiv IdD-is-iso x .is-precat-iso.has-is-iso = id-equiv ``` -## Total Category +## Total category The total category of the identity bifibration is isomorphic to $\cB$ itself. diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md index fec38df75..89cb2218d 100644 --- a/src/Cat/Displayed/Instances/Lifting.lagda.md +++ b/src/Cat/Displayed/Instances/Lifting.lagda.md @@ -142,7 +142,7 @@ higher level of strictness than usual. ni .natural _ _ _ = id-comm ``` -## Natural Transformations between Liftings +## Natural transformations between liftings As liftings are a reorganization of functors, it is reasonable to expect that we can express natural transformations between these. Fix functors @@ -288,7 +288,7 @@ composition. H' .F₁' f' ∘' α' .η' i ∘' β' .η' i ∎ ``` -## The Fibration of Liftings +## The fibration of liftings The liftings of functors $\cJ \to \cB$ assemble into a displayed category over the functor category $[\cJ, \cB]$. We shall denote this @@ -420,7 +420,7 @@ implies that our natural transformation is cartesian. (λ x → has-lift.cartesian (α .η x) (G' .F₀' x)) ``` -## Total Category +## Total category As noted earlier, the total category of $\cE^{\cJ}$ *is* the functor category $[\cJ, \int \cE]$. First, we shall need a heaping pile of diff --git a/src/Cat/Displayed/Instances/Objects.lagda.md b/src/Cat/Displayed/Instances/Objects.lagda.md index 07dac816c..b910ffdad 100644 --- a/src/Cat/Displayed/Instances/Objects.lagda.md +++ b/src/Cat/Displayed/Instances/Objects.lagda.md @@ -27,7 +27,7 @@ open Vertical-functor ``` --> -# The Fibration of Objects +# The fibration of objects Let $\cE \liesover \cB$ be a fibration. Its **fibration of objects** is the [wide subcategory] spanned by the [[cartesian morphisms]]. The idea diff --git a/src/Cat/Displayed/Instances/Simple.lagda.md b/src/Cat/Displayed/Instances/Simple.lagda.md index 5a582e28a..ceb2b9ba4 100644 --- a/src/Cat/Displayed/Instances/Simple.lagda.md +++ b/src/Cat/Displayed/Instances/Simple.lagda.md @@ -25,7 +25,7 @@ open Cat.Reasoning B open Binary-products B has-prods ``` -# Simple Fibrations +# Simple fibrations One reason to be interested in fibrations is that they provide an excellent setting to study logical and type-theoretical phenomena. @@ -90,7 +90,7 @@ Simple .Displayed.assoc' {f = u} {g = v} {h = w} f g h = (f ∘ ⟨ v ∘ π₁ , g ⟩) ∘ ⟨ w ∘ π₁ , h ⟩ ∎ ``` -# Cartesian Morphisms +# Cartesian morphisms A morphism $f' : \Gamma \times X \to Y$ in the simple fibration is cartesian if and only if the morphism $\langle \pi_1 , f' \rangle : @@ -251,7 +251,7 @@ a right inverse. id ∎ ``` -# Fibration Structure +# Fibration structure As suggested by it's name, the simple fibration is a fibration. given a map $\Gamma \to Delta$ in the base, and a $(\Delta , Y)$ @@ -281,7 +281,7 @@ Simple-fibration .has-lift f Y .cartesian .unique {m = g} {h' = h} h' p = h ∎ ``` -# Comprehension Structure +# Comprehension structure The simple fibration admits a [[fibred functor]] into the [[codomain fibration]] that maps an object $X$ over $\Gamma$ to the projection diff --git a/src/Cat/Displayed/Instances/Slice.lagda.md b/src/Cat/Displayed/Instances/Slice.lagda.md index 1558a8ebf..4b5a3570f 100644 --- a/src/Cat/Displayed/Instances/Slice.lagda.md +++ b/src/Cat/Displayed/Instances/Slice.lagda.md @@ -176,7 +176,7 @@ Fibre→slice-is-equiv = is-precat-iso→is-equivalence $ } ``` -## Cartesian Maps +## Cartesian maps A map $f' : x' \to y'$ over $f : x \to y$ in the codomain fibration is cartesian if and only if it forms a pullback square as below: @@ -293,7 +293,7 @@ categories, then the interpretation of Cartesian fibrations as reinterpret the above results as, essentially, giving the [[pullback functors]] between slice categories. -## As an Opfibration +## As an opfibration The canonical self-indexing is *always* an opfibration, where opreindexing is given by postcomposition. If we think about slices as diff --git a/src/Cat/Displayed/Instances/TotalProduct.lagda.md b/src/Cat/Displayed/Instances/TotalProduct.lagda.md index a4d80299b..93f27c907 100644 --- a/src/Cat/Displayed/Instances/TotalProduct.lagda.md +++ b/src/Cat/Displayed/Instances/TotalProduct.lagda.md @@ -23,7 +23,7 @@ module Cat.Displayed.Instances.TotalProduct private module EC = Displayed EC private module ED = Displayed ED ``` -# The Total Product of Displayed Categories +# The total product of displayed categories If $\cE\to \cB$ and $q :\cD \to \cC$ are displayed categories, then we can define their **total product** diff --git a/src/Cat/Displayed/Instances/Trivial.lagda.md b/src/Cat/Displayed/Instances/Trivial.lagda.md index 3db00b861..b14a76f92 100644 --- a/src/Cat/Displayed/Instances/Trivial.lagda.md +++ b/src/Cat/Displayed/Instances/Trivial.lagda.md @@ -27,7 +27,7 @@ open Total-hom ``` --> -# The Trivial Bifibration +# The trivial bifibration Any category $\ca{C}$ can be regarded as being displayed over the [[terminal category]] $\top$. diff --git a/src/Cat/Displayed/InternalSum.lagda.md b/src/Cat/Displayed/InternalSum.lagda.md index cd5a765f4..2cecf68f0 100644 --- a/src/Cat/Displayed/InternalSum.lagda.md +++ b/src/Cat/Displayed/InternalSum.lagda.md @@ -20,7 +20,7 @@ open Precategory B ``` --> -# Internal Sums +# Internal sums As has been noted before, fibrations are an excellent setting for studying logical and type-theoretic phenomena. Internal sums are an example of this; diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md index 4c40e7143..3903e91a8 100644 --- a/src/Cat/Displayed/Morphism.lagda.md +++ b/src/Cat/Displayed/Morphism.lagda.md @@ -28,7 +28,7 @@ private variable ``` --> -# Displayed Morphisms +# Displayed morphisms This module defines the displayed analogs of monomorphisms, epimorphisms, and isomorphisms. @@ -71,7 +71,7 @@ record _↪[_]_ open _↪[_]_ public ``` -## Weak Monos +## Weak monos When working in a displayed setting, we also have weaker versions of the morphism classes we are familiar with, wherein we can only left/right @@ -147,7 +147,7 @@ record _↠[_]_ open _↠[_]_ public ``` -## Weak Epis +## Weak epis We can define a weaker notion of epis that is dual to the definition of a weak mono. diff --git a/src/Cat/Displayed/Morphism/Duality.lagda.md b/src/Cat/Displayed/Morphism/Duality.lagda.md index d732c4e0b..8a317139b 100644 --- a/src/Cat/Displayed/Morphism/Duality.lagda.md +++ b/src/Cat/Displayed/Morphism/Duality.lagda.md @@ -42,7 +42,7 @@ private variable --> -# Duality of Displayed Morphism Classes +# Duality of displayed morphism classes In this file we prove that morphism classes in a [[displayed category]] correspond to their duals in the total opposite displayed category. diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md index b00467845..3a1077472 100644 --- a/src/Cat/Displayed/Reasoning.lagda.md +++ b/src/Cat/Displayed/Reasoning.lagda.md @@ -382,7 +382,7 @@ module _ {f' : Hom[ f ] x' y'} {g' : Hom[ g ] x' y'} (p : f ≡ g) where abstrac shiftr q i = from-pathp (λ j → q (i ∧ ~ j)) (~ i) ``` -## Path Actions +## Path actions Due to the plethora of `PathP`{.Agda}, we can no longer perform `ap`{.Agda} as easily. This is especially true when we have a `PathP`{.Agda} as well as a path between @@ -414,7 +414,7 @@ module _ {f' : Hom[ f ] y' z'} {g' : Hom[ g ] x' y'} {p : f ∘ g ≡ a} where a ``` -## Generalized Category Laws +## Generalized category laws In the definition of displayed categories, the identity and associativity laws are defined over `idl`{.Agda}, `idr`{.Agda}, and `assoc`{.Agda}. However, @@ -439,7 +439,7 @@ assoc[] {a = a} {b = b} {c = c} {a' = a'} {b' = b'} {c' = c'} {p = p} {q = q} = hom[ q ] ((a' ∘' b') ∘' c') ∎ ``` -## Identity Morphisms +## Identity morphisms These are the displayed counterparts to the [identity morphism combinators] for categories. diff --git a/src/Cat/Displayed/Total.lagda.md b/src/Cat/Displayed/Total.lagda.md index 1d8396132..041e885ad 100644 --- a/src/Cat/Displayed/Total.lagda.md +++ b/src/Cat/Displayed/Total.lagda.md @@ -21,7 +21,7 @@ open DM E open CR B ``` -# The Total Category of a Displayed Category {defines=total-category} +# The total category of a displayed category {defines=total-category} So far, we've been thinking of [[displayed categories]] as "categories of structures" over some base category. However, it's often useful to diff --git a/src/Cat/Displayed/Total/Op.lagda.md b/src/Cat/Displayed/Total/Op.lagda.md index cc8d04a3c..4756e6f3b 100644 --- a/src/Cat/Displayed/Total/Op.lagda.md +++ b/src/Cat/Displayed/Total/Op.lagda.md @@ -20,7 +20,7 @@ open Functor open Total-hom ``` -# Total Opposites +# Total opposites Opposites of [[displayed categories]] are somewhat subtle, as there are multiple constructions that one could reasonably call the "opposite". @@ -77,7 +77,7 @@ private ``` --> -## The Total Opposites and Total Categories +## The total opposites and total categories The reason we refer to this construction as the total opposite is that its total is **equal** to the opposite of the [[total category]]! To diff --git a/src/Cat/Functor/Adjoint/Monad.lagda.md b/src/Cat/Functor/Adjoint/Monad.lagda.md index a0beb871b..a0f364251 100644 --- a/src/Cat/Functor/Adjoint/Monad.lagda.md +++ b/src/Cat/Functor/Adjoint/Monad.lagda.md @@ -13,7 +13,7 @@ open _=>_ ``` --> -# The Monad from an Adjunction +# The monad from an adjunction ```agda module diff --git a/src/Cat/Functor/Adjoint/Monadic.lagda.md b/src/Cat/Functor/Adjoint/Monadic.lagda.md index 294e74746..b158bae84 100644 --- a/src/Cat/Functor/Adjoint/Monadic.lagda.md +++ b/src/Cat/Functor/Adjoint/Monadic.lagda.md @@ -17,7 +17,7 @@ open _=>_ ``` --> -# Monadic Adjunctions +# Monadic adjunctions An adjunction $F \dashv G$ between functors $F : C \to D$ and $G : D \to C$ is _monadic_ if the induced `comparison functor`{.Agda diff --git a/src/Cat/Functor/Conservative.lagda.md b/src/Cat/Functor/Conservative.lagda.md index 158d01c42..f17898d52 100644 --- a/src/Cat/Functor/Conservative.lagda.md +++ b/src/Cat/Functor/Conservative.lagda.md @@ -23,7 +23,7 @@ open Functor ``` --> -# Conservative Functors +# Conservative functors We say a functor is _conservative_ if it reflects isomorphisms. More concretely, if $f : A \to B$ is some morphism $\cC$, and if $F(f)$ is an iso in $\cD$, diff --git a/src/Cat/Functor/Equivalence.lagda.md b/src/Cat/Functor/Equivalence.lagda.md index f8434eafa..7cbb9602e 100644 --- a/src/Cat/Functor/Equivalence.lagda.md +++ b/src/Cat/Functor/Equivalence.lagda.md @@ -648,7 +648,7 @@ record Equivalence ``` --> -## Properties of Equivalences +## Properties of equivalences If $F : \cC \to \cD$ is fully-faithfuly and essentially surjective, then for every hom-set $\cD(d,d')$ there (merely) exists an equivalent hom-set diff --git a/src/Cat/Functor/Hom/Coyoneda.lagda.md b/src/Cat/Functor/Hom/Coyoneda.lagda.md index 6e947ce91..ce0276ba1 100644 --- a/src/Cat/Functor/Hom/Coyoneda.lagda.md +++ b/src/Cat/Functor/Hom/Coyoneda.lagda.md @@ -28,7 +28,7 @@ open _=>_ ``` --> -## The Coyoneda Lemma +## The Coyoneda lemma The Coyoneda lemma is, like its dual, a statement about presheaves. It states that "every presheaf is a colimit of representables", which, in diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md index d8f9cd4f0..1d8c81b55 100644 --- a/src/Cat/Functor/Hom/Displayed.lagda.md +++ b/src/Cat/Functor/Hom/Displayed.lagda.md @@ -25,7 +25,7 @@ open Functor ``` --> -# Displayed Hom Functors +# Displayed Hom functors Let $\cE$ be a [[displayed category]] over $\cB$. For every $u : x \to y$ in the base, we can obtain a bifunctor from $\cE_{x}\op \times \cE_{y}$ diff --git a/src/Cat/Functor/Kan/Pointwise.lagda.md b/src/Cat/Functor/Kan/Pointwise.lagda.md index 4272120c3..63044315f 100644 --- a/src/Cat/Functor/Kan/Pointwise.lagda.md +++ b/src/Cat/Functor/Kan/Pointwise.lagda.md @@ -129,7 +129,7 @@ As noted earlier, limits and colimits are pointwise Kan extensions. colimit→pointwise colim x = よ-reverses-colimits x colim ``` -## Computing Pointwise Extensions +## Computing pointwise extensions One useful fact about pointwise left Kan extensions (resp. right) is that they can be computed via colimits (resp. limits). We will focus on @@ -415,7 +415,7 @@ words, the extension we constructed is pointwise. (よ-reverses-colimits d) ``` -## All Pointwise Extensions are Computed via (Co)limits +## All pointwise extensions are computed via (co)limits As we've seen earlier, we can compute the extension of $F : \cC \to \cD$ along $p : \cC \to \cC'$ when $\cD$ has enough colimits, and that this diff --git a/src/Cat/Functor/Properties.lagda.md b/src/Cat/Functor/Properties.lagda.md index 2a8a80945..1211f0d2e 100644 --- a/src/Cat/Functor/Properties.lagda.md +++ b/src/Cat/Functor/Properties.lagda.md @@ -67,7 +67,7 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where ``` --> -## Fully Faithful Functors {defines="fully-faithful-functor fully-faithful ff"} +## Fully faithful functors {defines="fully-faithful-functor fully-faithful ff"} A functor is **fully faithful** (abbreviated **ff**) when its action on hom-sets is an equivalence. Since Hom-sets are sets, it suffices for the @@ -171,7 +171,7 @@ the domain category to serve as an inverse for $f$: im' .inverses .Cm.Inverses.invr = invr ``` -## Essential Fibres {defines="essential-fibre"} +## Essential fibres {defines="essential-fibre"} The **essential fibre** of a functor $F : C \to D$ over an object $y : D$ is the space of objects of $C$ which $F$ takes, up to isomorphism, to @@ -219,7 +219,7 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where ``` --> -## Pseudomonic Functors {defines="pseudomonic pseudomonic-functor"} +## Pseudomonic functors {defines="pseudomonic pseudomonic-functor"} A functor is **pseudomonic** if it is faithful and full on isomorphisms. Pseudomonic functors are arguably the correct notion of subcategory, as @@ -301,7 +301,7 @@ essentially injective. ext (equiv→counit ff (D.to f))) ``` -## Equivalence on Objects Functors +## Equivalence on objects functors A functor $F : \cC \to \cD$ is an **equivalence on objects** if its action on objects is an equivalence. diff --git a/src/Cat/Functor/Reasoning.lagda.md b/src/Cat/Functor/Reasoning.lagda.md index 7d8693add..67bb89ff0 100644 --- a/src/Cat/Functor/Reasoning.lagda.md +++ b/src/Cat/Functor/Reasoning.lagda.md @@ -30,7 +30,7 @@ private variable --> -# Reasoning Combinators for Functors +# Reasoning combinators for functors The combinators exposed in [category reasoning] abstract out a lot of common algebraic manipulations, and make proofs much more concise. However, once functors @@ -40,7 +40,7 @@ This module is meant to be imported qualified. [category reasoning]: Cat.Reasoning.html -## Identity Morphisms +## Identity morphisms ```agda module _ (a≡id : a ≡ 𝒞.id) where diff --git a/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md b/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md index b6f08f1d5..5dbf6da14 100644 --- a/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md +++ b/src/Cat/Functor/Reasoning/FullyFaithful.lagda.md @@ -17,7 +17,7 @@ module where ``` -# Reasoning for ff Functors +# Reasoning for ff functors -# Internal Categories +# Internal categories We often think of categories as _places where we can do mathematics_. This is done by translating definitions into the internal language of @@ -559,7 +559,7 @@ module _ {ℂ 𝔻 : Internal-cat} {F G : Internal-functor ℂ 𝔻} where Internal-nat-set = Iso→is-hlevel 2 nat-eqv $ Σ-is-hlevel 2 hlevel! $ λ _ → Σ-is-hlevel 2 hlevel! $ λ _ → - Π-is-hlevel' 2 λ _ → Π-is-hlevel' 2 λ _ → + Π-is-hlevel²' 2 λ _ _ → Π-is-hlevel 2 λ _ → Π-is-hlevel 2 λ _ → PathP-is-hlevel 2 Internal-hom-set diff --git a/src/Cat/Internal/Functor/Outer.lagda.md b/src/Cat/Internal/Functor/Outer.lagda.md index a218c9485..966d8fcef 100644 --- a/src/Cat/Internal/Functor/Outer.lagda.md +++ b/src/Cat/Internal/Functor/Outer.lagda.md @@ -27,7 +27,7 @@ open Internal-hom ``` --> -# Outer Functors +# Outer functors The category $\Sets$ is not [[strict|strict category]], so it is not [internal] to any category of sets, even setting aside size issues. @@ -115,7 +115,7 @@ functors from the [internal opposite category] of $\ica{C}$. [discrete fibrations]: Cat.Displayed.Cartesian.Discrete.html [internal opposite category]: Cat.Internal.Opposite.html -## Internal Hom Functors +## Internal Hom functors The canonical example of an outer functor is the internal analog of the hom functor $\cC(X,-)$. We require the following data: $\cC$ is diff --git a/src/Cat/Internal/Reasoning.lagda.md b/src/Cat/Internal/Reasoning.lagda.md index ec30fc145..6c8553e9d 100644 --- a/src/Cat/Internal/Reasoning.lagda.md +++ b/src/Cat/Internal/Reasoning.lagda.md @@ -40,7 +40,7 @@ private variable ``` --> -## Identity Morphisms +## Identity morphisms ```agda abstract @@ -132,7 +132,7 @@ sub-id : ∀ {f : Homi x y} → PathP (λ i → Homi (idr x i) (idr y i)) (f [ i sub-id = Internal-hom-pathp (idr _) (idr _) (idr _) ``` -## Generalized Morphisms +## Generalized morphisms ```agda ∘i-ihom diff --git a/src/Cat/Morphism/Duality.lagda.md b/src/Cat/Morphism/Duality.lagda.md index b332d6e43..d4bc005f8 100644 --- a/src/Cat/Morphism/Duality.lagda.md +++ b/src/Cat/Morphism/Duality.lagda.md @@ -22,7 +22,7 @@ private variable ``` --> -# Duality of Morphism Classes +# Duality of morphism classes In this file we prove that morphisms classes in a category correspond to their duals in the opposite category. There is very diff --git a/src/Cat/Reasoning.lagda.md b/src/Cat/Reasoning.lagda.md index 0e2406220..07c3dd5ad 100644 --- a/src/Cat/Reasoning.lagda.md +++ b/src/Cat/Reasoning.lagda.md @@ -13,7 +13,7 @@ module Cat.Reasoning {o ℓ} (C : Precategory o ℓ) where open import Cat.Morphism C public ``` -# Reasoning Combinators for Categories +# Reasoning combinators for categories When doing category theory, we often have to perform many "trivial" algebraic manipulations like reassociation, insertion of identity morphisms, etc. @@ -33,7 +33,7 @@ private variable ``` --> -## Identity Morphisms +## Identity morphisms ```agda id-comm : ∀ {a b} {f : Hom a b} → f ∘ id ≡ id ∘ f diff --git a/src/Cat/Restriction/Base.lagda.md b/src/Cat/Restriction/Base.lagda.md index 57b572b6b..a18f16d84 100644 --- a/src/Cat/Restriction/Base.lagda.md +++ b/src/Cat/Restriction/Base.lagda.md @@ -8,7 +8,7 @@ open import Cat.Prelude module Cat.Restriction.Base where ``` -# Restriction Categories +# Restriction categories Much of computer science involves the study of partial functions. Unfortunately, partial functions are somewhat tedious to work with, diff --git a/src/Cat/Restriction/Functor.lagda.md b/src/Cat/Restriction/Functor.lagda.md index 7309d7668..afdb461fa 100644 --- a/src/Cat/Restriction/Functor.lagda.md +++ b/src/Cat/Restriction/Functor.lagda.md @@ -17,7 +17,7 @@ open Functor ``` --> -# Restriction Functors +# Restriction functors A functor $F : \cC \to \cD$ between [restriction categories] is a **restriction functor** if $F (\restrict{f}) = \restrict{(F f)}$. @@ -59,7 +59,7 @@ F∘-restriction F∘-restriction F G F↓ G↓ f = ap (F .F₁) (G↓ f) ∙ F↓ (G .F₁ f) ``` -# Properties of Restriction Functors +# Properties of restriction functors Let $F : \cC \to \cD$ be a restriction functor. Note that $F$ preserves [total morphisms] and [restriction idempotents]. diff --git a/src/Cat/Restriction/Instances/Allegory.lagda.md b/src/Cat/Restriction/Instances/Allegory.lagda.md index e1e3a67d0..cdeb2490d 100644 --- a/src/Cat/Restriction/Instances/Allegory.lagda.md +++ b/src/Cat/Restriction/Instances/Allegory.lagda.md @@ -13,7 +13,7 @@ import Cat.Allegory.Morphism module Cat.Restriction.Instances.Allegory where ``` -# Restriction Categories from Allegories +# Restriction categories from allegories Let $\cA$ be an [allegory], considered as a sort of generalized category of "sets and relations". Much like we can recover a category of "sets and diff --git a/src/Cat/Restriction/Reasoning.lagda.md b/src/Cat/Restriction/Reasoning.lagda.md index f792f729f..01d25c989 100644 --- a/src/Cat/Restriction/Reasoning.lagda.md +++ b/src/Cat/Restriction/Reasoning.lagda.md @@ -23,7 +23,7 @@ open Restriction-category C-restrict public ``` --> -# Reasoning in Restriction Categories +# Reasoning in restriction categories This module provides some useful lemmas about restriction categories. We begin by noting that for every $f$, $\restrict{f}$ is an [idempotent]. @@ -87,7 +87,7 @@ Next, we note that iterating $(-)downarrow$ does nothing. f ↓ ∎ ``` -## Total Morphisms +## Total morphisms We say that a morphism $f : X \to Y$ in a restriction category is **total** if its restriction $\restrict{f}$ is the identity morphism. @@ -194,7 +194,7 @@ total-smashl {f = f} {g = g} f-total = g ↓ ∎ ``` -## Restriction Idempotents +## Restriction idempotents We say that a morphism $f : X \to X$ is a **restriction idempotent** if $\restrict{f} = f$. @@ -236,7 +236,7 @@ restriction-idem-comm f-dom g-dom = ·· ap₂ _∘_ g-dom f-dom ``` -## Restricted Monics +## Restricted monics A morphism $f : X \to Y$ is a **restricted monic** if for all $g, h : A \to X$, $fg = fh$ implies that $\restrict{f}g = \restrict{f}h$. @@ -304,7 +304,7 @@ restricted-monic-cancell {f = f} {g = g} fg-rmonic f-total h1 h2 p = g ↓ ∘ h2 ∎ ``` -## Restricted Retracts +## Restricted retracts Let $r : X \to Y$ and $s : Y \to X$ be a pair of morphisms. The map $r$ is a **restricted retract** of $s$ when $rs = \restrict{s}$. @@ -384,7 +384,7 @@ has-restricted-retract-cancell {f = f} {g = g} fg-sect f-total .is-restricted-re g ↓ ∎ ``` -## Restricted Isomorphisms +## Restricted isomorphisms Let $f : X \to Y$ and $g : Y \to X$ be a pair of morphisms. $f$ and $g$ are **restricted inverses** if $fg = \restrict{g}$ and @@ -475,7 +475,7 @@ restricted-inverses+total→inverses {f = f} {g = g} fg-inv f-total g-total = re } ``` -## Refining Morphisms +## Refining morphisms Let $\cC$ be a restriction category, and $f, g : \cC(X,Y)$. We say that $g$ **refines** $f$ if $g$ agrees with $f$ when restricted to the domain of diff --git a/src/Cat/Restriction/Total.lagda.md b/src/Cat/Restriction/Total.lagda.md index 154ab552e..15aa15128 100644 --- a/src/Cat/Restriction/Total.lagda.md +++ b/src/Cat/Restriction/Total.lagda.md @@ -13,7 +13,7 @@ import Cat.Restriction.Reasoning module Cat.Restriction.Total where ``` -# The Subcategory of Total Maps +# The subcategory of total maps Let $\cC$ be a restriction category. We can construct a [wide subcategory] of $\cC$ containing only the [total maps] of $\cC$, diff --git a/src/Cat/Skeletal.lagda.md b/src/Cat/Skeletal.lagda.md index 0267943f5..ee08da91f 100644 --- a/src/Cat/Skeletal.lagda.md +++ b/src/Cat/Skeletal.lagda.md @@ -15,7 +15,7 @@ open Precategory using (Ob) module Cat.Skeletal where ``` -# Skeletal Precategories +# Skeletal precategories A precategory $\cC$ is **skeletal** if objects having _the property of being isomorphic_ are identical. The clunky rephrasing is proposital: if diff --git a/src/Cat/Solver.lagda.md b/src/Cat/Solver.lagda.md index a5544b0d3..3302f3855 100644 --- a/src/Cat/Solver.lagda.md +++ b/src/Cat/Solver.lagda.md @@ -21,7 +21,7 @@ private variable ``` --> -# Solver for Categories +# Solver for categories This module is split pretty cleanly into two halves: the first half implements an algorithm for reducing, in a systematic way, problems diff --git a/src/Cat/Strict.lagda.md b/src/Cat/Strict.lagda.md index f83c23650..5d03558ba 100644 --- a/src/Cat/Strict.lagda.md +++ b/src/Cat/Strict.lagda.md @@ -8,7 +8,7 @@ open import Cat.Prelude module Cat.Strict where ``` -# Strict Precategories {defines="strict-category strict-categories"} +# Strict precategories {defines="strict-category strict-categories"} We call a precategory **strict** if its type of objects is a `Set`{.Agda ident=is-set}. diff --git a/src/Cat/Univalent.lagda.md b/src/Cat/Univalent.lagda.md index 137f8823e..b08d90ce3 100644 --- a/src/Cat/Univalent.lagda.md +++ b/src/Cat/Univalent.lagda.md @@ -15,7 +15,7 @@ open Precategory using (Ob) module Cat.Univalent where ``` -# (Univalent) Categories {defines="univalent-categories univalent-category"} +# (Univalent) categories {defines="univalent-categories univalent-category"} In much the same way that a [[partial order]] is a preorder where $x \le y \land y \le x \to x = y$, a **category** is a precategory where diff --git a/src/Cat/Univalent/Instances/Algebra.lagda.md b/src/Cat/Univalent/Instances/Algebra.lagda.md index bc128697d..8277602de 100644 --- a/src/Cat/Univalent/Instances/Algebra.lagda.md +++ b/src/Cat/Univalent/Instances/Algebra.lagda.md @@ -16,7 +16,7 @@ module where ``` -# Univalence of Eilenberg-Moore Categories +# Univalence of Eilenberg-Moore categories Given a base [[univalent category]] $\cC$, we can consider a [monad] $M$ on $\cC$, and its associated [Eilenberg-Moore category] diff --git a/src/Data/Bool.lagda.md b/src/Data/Bool.lagda.md index fb997e293..d553bfd0a 100644 --- a/src/Data/Bool.lagda.md +++ b/src/Data/Bool.lagda.md @@ -23,7 +23,7 @@ module Data.Bool where open import Prim.Data.Bool public ``` -# The Booleans +# The booleans The type of booleans is interesting in homotopy type theory because it is the simplest type where its automorphisms in `Type`{.Agda} are diff --git a/src/Data/Fin.lagda.md b/src/Data/Fin.lagda.md index 3c19aded6..3c5837d76 100644 --- a/src/Data/Fin.lagda.md +++ b/src/Data/Fin.lagda.md @@ -6,7 +6,7 @@ open import Data.Fin.Finite public open import Data.Fin.Base public ``` -# Finite Sets - Index +# Finite sets - index The natural numbers are constructed in the module [`Data.Fin.Base`]. Their arithmetical properties are proved in diff --git a/src/Data/Fin/Base.lagda.md b/src/Data/Fin/Base.lagda.md index 2e25595b0..050e8c1ed 100644 --- a/src/Data/Fin/Base.lagda.md +++ b/src/Data/Fin/Base.lagda.md @@ -19,7 +19,7 @@ import Data.Nat.Base as Nat module Data.Fin.Base where ``` -# Finite Sets {defines=standard-finite-set} +# Finite sets {defines=standard-finite-set} The type `Fin`{.Agda} is the type of size `n`. These are defined as an inductive family over `Nat`{.Agda}, such that `Fin 0` has 0 elements, @@ -284,7 +284,7 @@ opposite {n = suc n} fzero = from-nat n opposite {n = suc n} (fsuc i) = weaken (opposite i) ``` -## Vector Operations +## Vector operations ```agda _[_≔_] diff --git a/src/Data/Fin/Properties.lagda.md b/src/Data/Fin/Properties.lagda.md index bf79accb8..e38c7d95a 100644 --- a/src/Data/Fin/Properties.lagda.md +++ b/src/Data/Fin/Properties.lagda.md @@ -14,7 +14,7 @@ module Data.Fin.Properties where ``` -# Finite Sets - Properties +# Finite sets - properties ## Ordering @@ -197,7 +197,7 @@ finite-surjection-split finite-surjection-split f = finite-choice _ ``` -## Vector Operations +## Vector operations ```agda avoid-insert diff --git a/src/Data/Image.lagda.md b/src/Data/Image.lagda.md index 0f1966e86..ba95f4cbf 100644 --- a/src/Data/Image.lagda.md +++ b/src/Data/Image.lagda.md @@ -38,7 +38,7 @@ of $A$". Can we do better? It turns out that we can! This generally goes by the name of **type-theoretic replacement**, after Rijke [@Rijke:2017 §5]; in turn, the name _replacement_ comes from the axiom of material set theory -sayings the image of a set under a function is again set.^[Keep in mind +saying the image of a set under a function is again set.^[Keep in mind that material set theory says "is a set" in a very different way than we do; They mean it about size.] Here we implement a slight generalization of [Evan Cavallo's construction] in terms of higher induction-recursion. @@ -193,36 +193,39 @@ module Replacement data Image where inc : A → Image quot : ∀ {r r'} → embed r ∼ embed r' → r ≡ r' - coh : ∀ r → quot (rr (embed r)) ≡ refl embed (inc a) = f a embed (quot p i) = locally-small .to-path p i - embed (coh r i j) = - to-path-refl {a = embed r} locally-small i j ``` -Well, there's still a minor coherence quibble. To show that -`image-embedding` is an embedding, we need `quot`{.Agda} to send the -reflexivity of the identity system to the actual reflexivity path. But -that's a single coherence constructor, not infinitely many, and it's -satisfied by our projection function. We'll show that it's an embedding -by showing that it's coherently cancellable, i.e. that we have an -equivalence $(f'(x) \equiv f'(y)) \simeq (x \equiv y)$. +And, having used inductive-recursion to tie the dependency knot, we're +actually done: the construction above is coherent enough, _even if_ it +looks like the `quot`{.Agda} constructor only says that `embed`{.Agda} +is an injection. We can use the algebraic properties of identity systems +to show that it's actually a proper embedding: ```agda - embed-is-embedding : is-embedding embed - embed-is-embedding = cancellable→embedding λ {x y} → - Iso→Equiv (from , iso (ap embed) invr (invl {x} {y})) where + embed-is-embedding' : ∀ x → is-contr (fibre embed (embed x)) + embed-is-embedding' x .centre = x , refl + embed-is-embedding' x .paths (y , q) = + Σ-pathp (quot (ls.from (sym q))) (commutes→square coh) + where abstract + coh : ls.to (ls.from (sym q)) ∙ q ≡ refl ∙ refl + coh = ap (_∙ q) (ls.ε (sym q)) ·· ∙-invl q ·· sym (∙-idl refl) - from : ∀ {x y} → embed x ≡ embed y → x ≡ y - from path = quot (ls.from path) + embed-is-embedding : is-embedding embed + embed-is-embedding = embedding-lemma embed-is-embedding' +``` - invr : ∀ {x y} → is-right-inverse (ap embed {x} {y}) from - invr = J (λ y p → from (ap embed p) ≡ p) - (ap quot (transport-refl _) ∙ coh _) +And it's possible to pull back the identity system on $b$ to one on $\im +f$, to really drive home the point that points in the image are +identified precisely through their identification, under $f$, in the +codomain. - invl : ∀ {x y} → is-left-inverse (ap embed {x} {y}) from - invl p = ls.ε _ +```agda + Image-identity-system : is-identity-system (λ x y → embed x ∼ embed y) (λ _ → rr _) + Image-identity-system = pullback-identity-system locally-small + (embed , embed-is-embedding) ``` -## Path Space +## Path space Using these lemmas, we can characterise the path space of `List A` in terms of the path space of `A`. For this, we define by induction a type @@ -100,9 +100,9 @@ We use this to prove that lists preserve h-levels for $n \ge 2$, i.e. if Code-is-hlevel {x ∷ x₁} {x₂ ∷ y} = ×-is-hlevel (suc n) (ahl _ _) Code-is-hlevel instance - H-Level-List : ∀ {n} {k} → ⦃ H-Level A (2 + n) ⦄ → H-Level (List A) (2 + n + k) + H-Level-List : ∀ {n} → ⦃ H-Level A (2 + n) ⦄ → H-Level (List A) (2 + n) H-Level-List {n = n} ⦃ x ⦄ = - basic-instance (2 + n) (List-is-hlevel n (H-Level.has-hlevel x)) + record { has-hlevel = List-is-hlevel n (H-Level.has-hlevel x) } is-set→List-is-set : is-set A → is-set (List A) is-set→List-is-set = List-is-hlevel zero diff --git a/src/Data/List/Base.lagda.md b/src/Data/List/Base.lagda.md index 50d6fc5d6..3806054f3 100644 --- a/src/Data/List/Base.lagda.md +++ b/src/Data/List/Base.lagda.md @@ -172,6 +172,8 @@ reverse = go [] where _∷r_ : List A → A → List A xs ∷r x = xs ++ (x ∷ []) +infixl 20 _∷r_ + all=? : (A → A → Bool) → List A → List A → Bool all=? eq=? [] [] = true all=? eq=? [] (x ∷ ys) = false @@ -216,6 +218,15 @@ intercalate x [] = [] intercalate x (y ∷ []) = y ∷ [] intercalate x (y ∷ z ∷ xs) = y ∷ x ∷ intercalate x (z ∷ xs) +zip : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → List A → List B → List (A × B) +zip [] _ = [] +zip _ [] = [] +zip (a ∷ as) (b ∷ bs) = (a , b) ∷ zip as bs + +unzip : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → List (A × B) → List A × List B +unzip [] = [] , [] +unzip ((a , b) ∷ xs) = ×-map (a ∷_) (b ∷_) (unzip xs) + instance Idiom-List : Idiom (eff List) Idiom-List .pure a = a ∷ [] diff --git a/src/Data/List/Membership.lagda.md b/src/Data/List/Membership.lagda.md index fbfafeedc..4c1b8f54a 100644 --- a/src/Data/List/Membership.lagda.md +++ b/src/Data/List/Membership.lagda.md @@ -13,7 +13,7 @@ open import Data.Sum.Base module Data.List.Membership where ``` -## Pointwise Predicates +## Pointwise predicates ```agda data Some {ℓ ℓ'} {A : Type ℓ} (P : A → Type ℓ') : List A → Type (ℓ ⊔ ℓ') where @@ -149,7 +149,7 @@ instance --> -## Membership in Lists +## Membership in lists ```agda _∈ₗ_ : ∀ {ℓ} {A : Type ℓ} → A → List A → Type ℓ diff --git a/src/Data/Maybe/Properties.lagda.md b/src/Data/Maybe/Properties.lagda.md index 39c1e1252..57b46a0e9 100644 --- a/src/Data/Maybe/Properties.lagda.md +++ b/src/Data/Maybe/Properties.lagda.md @@ -25,7 +25,7 @@ private variable # Properties of Maybe -## Path Space +## Path space We can use these lemmas to characterise the path space of `Maybe A` in terms of the path space of `A`. This involves a standard encode-decode @@ -169,7 +169,7 @@ Finite-Maybe {A = A} ⦃ fa ⦄ .enumeration = maybe-iso f .snd .is-iso.linv nothing = refl ``` -# Misc. Properties +# Misc. properties If `A` is empty, then a `Maybe A` must be `nothing`{.Agda}. diff --git a/src/Data/Nat.lagda.md b/src/Data/Nat.lagda.md index 1dc6477fe..14374e02f 100644 --- a/src/Data/Nat.lagda.md +++ b/src/Data/Nat.lagda.md @@ -11,7 +11,7 @@ open import Prim.Data.Nat using (Nat ; _+_ ; _-_) public ``` -# Natural Numbers - Index +# Natural numbers - index The natural numbers are constructed in the module [`Data.Nat.Base`]. Their arithmetical properties are proved in diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md index d3d42fe11..1f006067c 100644 --- a/src/Data/Nat/Base.lagda.md +++ b/src/Data/Nat/Base.lagda.md @@ -21,7 +21,7 @@ open import Prim.Data.Nat hiding (_<_) public ``` --> -# Natural Numbers {defines="natural-numbers"} +# Natural numbers {defines="natural-numbers"} The natural numbers are the inductive type generated by `zero`{.Agda} and closed under taking `suc`{.Agda}cessors. Thus, they satisfy the diff --git a/src/Data/Nat/Properties.lagda.md b/src/Data/Nat/Properties.lagda.md index 819d29ce8..f5e74797e 100644 --- a/src/Data/Nat/Properties.lagda.md +++ b/src/Data/Nat/Properties.lagda.md @@ -15,7 +15,7 @@ open import Data.Bool module Data.Nat.Properties where ``` -# Natural Numbers - Properties +# Natural numbers - properties This module contains proofs of arithmetic identities for [the natural numbers]. Since they're mostly simple inductive arguments written in @@ -288,6 +288,20 @@ max-≤r zero zero = 0≤x max-≤r zero (suc y) = ≤-refl max-≤r (suc x) zero = 0≤x max-≤r (suc x) (suc y) = s≤s (max-≤r x y) + +max-is-lub : (x y z : Nat) → x ≤ z → y ≤ z → max x y ≤ z +max-is-lub zero zero z 0≤x 0≤x = 0≤x +max-is-lub zero (suc y) (suc z) 0≤x (s≤s q) = s≤s q +max-is-lub (suc x) zero (suc z) (s≤s p) 0≤x = s≤s p +max-is-lub (suc x) (suc y) (suc z) (s≤s p) (s≤s q) = s≤s (max-is-lub x y z p q) + +max-zerol : (x : Nat) → max 0 x ≡ x +max-zerol zero = refl +max-zerol (suc x) = refl + +max-zeror : (x : Nat) → max x 0 ≡ x +max-zeror zero = refl +max-zeror (suc x) = refl ``` ### Minimum @@ -314,4 +328,16 @@ min-≤r zero zero = 0≤x min-≤r zero (suc y) = 0≤x min-≤r (suc x) zero = 0≤x min-≤r (suc x) (suc y) = s≤s (min-≤r x y) + +min-is-glb : (x y z : Nat) → z ≤ x → z ≤ y → z ≤ min x y +min-is-glb x y zero 0≤x 0≤x = 0≤x +min-is-glb (suc x) (suc y) (suc z) (s≤s p) (s≤s q) = s≤s (min-is-glb x y z p q) + +min-zerol : (x : Nat) → min 0 x ≡ 0 +min-zerol zero = refl +min-zerol (suc x) = refl + +min-zeror : (x : Nat) → min x 0 ≡ 0 +min-zeror zero = refl +min-zeror (suc x) = refl ``` diff --git a/src/Data/Nat/Solver.lagda.md b/src/Data/Nat/Solver.lagda.md index f2014909c..3db677584 100644 --- a/src/Data/Nat/Solver.lagda.md +++ b/src/Data/Nat/Solver.lagda.md @@ -15,7 +15,7 @@ open import Data.List hiding (lookup) module Data.Nat.Solver where ``` -# The Nat Solver +# The Nat solver This module defines a solver for equations in the commutative semiring of [natural numbers]. Our approach splits cleanly into 3 distinct parts: @@ -26,7 +26,7 @@ of [natural numbers]. Our approach splits cleanly into 3 distinct parts: - Evaluation of reflected terms into polynomials - The reflection interface -## Horner Normal Forms +## Horner normal forms If we ignore the `suc`{.Agda} and `zero`{.Agda} constructors, and their respective equations, the core problem at hand is trying to compute @@ -129,7 +129,7 @@ decidedly more difficult. As the solver is not expected to deal with polynomials with large degrees, this term blow-up will not be a problem in practice. -### Operations on Horner Normal Forms +### Operations on Horner normal forms Now, let's define a handful of functions for constructing and combining polynomials. The naming here can get a bit confusing, so let's stick @@ -221,7 +221,7 @@ r *ₚ' zerop = zerop r *ₚ' (p *X+ q) = (r *ₚ' p) *X+ (r *ₚ q) ``` -### Evaluation of Horner Normal Forms +### Evaluation of Horner normal forms Multivariate polynomials represent functions $A^n \to A$, so we should be able to interpret them as such. Luckily, Horner Normal Forms are @@ -243,7 +243,7 @@ block x = x ⟦ p *X+ q ⟧ₚ (x₀ ∷ env) = ⟦ p ⟧ₚ (x₀ ∷ env) * x₀ + ⟦ q ⟧ₚ env ``` -### Soundness of the Operations +### Soundness of the operations Now, it's important that the operations we defined actually denote the correct operations on natural numbers. As a warm up, let's show that the @@ -385,7 +385,7 @@ sound-*ₚ' r (p *X+ q) x₀ env = This concludes phase one of the solver. -## Evaluation into Polynomials +## Evaluation into polynomials Now that we've gotten the first phase of the solver done, let's move on to expressions in the language of natural numbers. Our first move shall @@ -443,7 +443,7 @@ handle literals separately. ↓ (e₁ ‵* e₂) = (↓ e₁) *ₚ (↓ e₂) ``` -### Soundness of Evaluation +### Soundness of evaluation With all of that machinery in place, our final proof shall be to show that evaluating an expression into a polynomial has the same semantics @@ -557,7 +557,7 @@ private (unknown h∷ lhs v∷ rhs v∷ env v∷ def (quote refl) [] v∷ []) ``` -### The Actual Macros +### The actual macros Now, the actual reflection API calls. In order to keep drawing this file out, we start by defining some useful debugging macros. As we noted a diff --git a/src/Data/Power.lagda.md b/src/Data/Power.lagda.md index 6907a1eb7..bf19dd63e 100644 --- a/src/Data/Power.lagda.md +++ b/src/Data/Power.lagda.md @@ -18,7 +18,7 @@ private variable ``` --> -# Power Sets {defines="power-set"} +# Power sets {defines="power-set"} The **power set** of a type $X$ is the collection of all maps from $X$ into the universe of `propositional types`{.Agda ident=Ω}. Since @@ -64,7 +64,7 @@ propositions to each inhabitant of $X$. Ω-ua (A⊆B x) (B⊂A x) ``` -## Lattice Structure +## Lattice structure The type $\bb{P}(X)$ has a lattice structure, with the order given by `subset inclusion`{.Agda ident=_⊆_}. We call the meets diff --git a/src/Data/Product/NAry.lagda.md b/src/Data/Product/NAry.lagda.md index 95366af3b..a7e170bb7 100644 --- a/src/Data/Product/NAry.lagda.md +++ b/src/Data/Product/NAry.lagda.md @@ -9,7 +9,7 @@ open import 1Lab.Type module Data.Product.NAry where ``` -# n-Ary Products +# n-Ary products This is an alternative definition of the type of n-ary products, which, unlike [`Vec`](Data.Vec.Base.html), is defined by _recursion_ on the diff --git a/src/Data/Reflection/Argument.agda b/src/Data/Reflection/Argument.agda index dcc291339..5de209164 100644 --- a/src/Data/Reflection/Argument.agda +++ b/src/Data/Reflection/Argument.agda @@ -64,7 +64,7 @@ record Arg {a} (A : Type a) : Type a where pattern _v∷_ t xs = arg (arginfo visible (modality relevant quantity-ω)) t ∷ xs pattern _h∷_ t xs = arg (arginfo hidden (modality relevant quantity-ω)) t ∷ xs pattern _hm∷_ t xs = arg (arginfo hidden (modality relevant _)) t ∷ xs -infixr 30 _v∷_ _h∷_ _hm∷_ +infixr 20 _v∷_ _h∷_ _hm∷_ argH0 argI argH argN : ∀ {ℓ} {A : Type ℓ} → A → Arg A argH = arg (arginfo hidden (modality relevant quantity-ω)) @@ -125,3 +125,22 @@ instance Traversable-Arg : Traversable (eff Arg) Traversable-Arg .Traversable.traverse f (arg ai x) = arg ai <$> f x + +record Has-visibility {ℓ} (A : Type ℓ) : Type ℓ where + field set-visibility : Visibility → A → A + +open Has-visibility ⦃ ... ⦄ public + +instance + Has-visibility-Arg : ∀ {ℓ} {A : Type ℓ} → Has-visibility (Arg A) + Has-visibility-Arg .set-visibility v (arg (arginfo _ m) x) = arg (arginfo v m) x + + Has-visibility-Args : ∀ {ℓ} {A : Type ℓ} → Has-visibility (List (Arg A)) + Has-visibility-Args .set-visibility v l = set-visibility v <$> l + +hide : ∀ {ℓ} {A : Type ℓ} → ⦃ Has-visibility A ⦄ → A → A +hide = set-visibility hidden + +hide-if : ∀ {ℓ} {A : Type ℓ} → ⦃ Has-visibility A ⦄ → Bool → A → A +hide-if true a = hide a +hide-if false a = a diff --git a/src/Data/Reflection/Term.agda b/src/Data/Reflection/Term.agda index da4d4e177..f434c9237 100644 --- a/src/Data/Reflection/Term.agda +++ b/src/Data/Reflection/Term.agda @@ -364,6 +364,16 @@ unpi-view : Telescope → Term → Term unpi-view [] k = k unpi-view ((n , a) ∷ t) k = pi a (abs n (unpi-view t k)) +tel→lam : Telescope → Term → Term +tel→lam [] t = t +tel→lam ((n , arg (arginfo v _) _) ∷ ts) t = lam v (abs n (tel→lam ts t)) + +tel→args : Nat → Telescope → List (Arg Term) +tel→args skip tel = map-up (λ i (_ , arg ai _) → arg ai (var (skip + length tel - i) [])) 1 tel + +tel→pats : Nat → Telescope → List (Arg Pattern) +tel→pats skip tel = map-up (λ i (_ , arg ai _) → arg ai (var (skip + length tel - i))) 1 tel + list-term : List Term → Term list-term [] = con (quote List.[]) [] list-term (x ∷ xs) = con (quote List._∷_) (argN x ∷ argN (list-term xs) ∷ []) diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md index f6fe6e55e..4fffca1c2 100644 --- a/src/Data/Set/Coequaliser.lagda.md +++ b/src/Data/Set/Coequaliser.lagda.md @@ -18,7 +18,7 @@ private variable ``` --> -# Set Coequalisers +# Set coequalisers In their most general form, colimits can be pictured as taking disjoint unions and then "gluing together" some parts. The "gluing together" part diff --git a/src/Data/Sum.lagda.md b/src/Data/Sum.lagda.md index 74b2b285c..7c57feaa6 100644 --- a/src/Data/Sum.lagda.md +++ b/src/Data/Sum.lagda.md @@ -2,7 +2,7 @@ module Data.Sum where ``` -# Sum Types +# Sum types ```agda open import Data.Sum.Properties public diff --git a/src/Data/Sum/Base.lagda.md b/src/Data/Sum/Base.lagda.md index a228ed95b..58b87c70e 100644 --- a/src/Data/Sum/Base.lagda.md +++ b/src/Data/Sum/Base.lagda.md @@ -13,7 +13,7 @@ open import Data.Dec.Base module Data.Sum.Base where ``` -# Sum Types +# Sum types Sum types are one of the fundamental ingredients of type theory. They play a dual role to the [[product type]]; if products allow us to state @@ -39,7 +39,7 @@ private variable --> -## Universal Properties +## Universal properties One of the most important things about sum types is the following property: given two functions `A → C` and `B → C`, we can construct a function diff --git a/src/Homotopy/Space/Sinfty.lagda.md b/src/Homotopy/Space/Sinfty.lagda.md index 86c2c540b..027906611 100644 --- a/src/Homotopy/Space/Sinfty.lagda.md +++ b/src/Homotopy/Space/Sinfty.lagda.md @@ -8,7 +8,7 @@ open import 1Lab.Prelude module Homotopy.Space.Sinfty where ``` -# The Infinite Sphere +# The infinite sphere The $(n+1)$-sphere can be constructed from the $n$-sphere via suspension. By writing a recursive HIT, we can define a type which is its own @@ -28,7 +28,7 @@ contractible. In Homotopy Type Theory, then, the only meaningful statement that can be made of `S∞`{.Agda} is that it is contractible. We prove this in two different ways. -## The Book HoTT Approach +## The Book HoTT approach ```agda open is-contr @@ -66,7 +66,7 @@ is-contrS∞' .centre = N is-contrS∞' .paths = pathsS∞' ``` -## The Cubical Approach +## The cubical approach The cubical approach essentially acomplishes the same thing as the previous proof, without using any helper lemmas, by way of drawing a slightly clever diff --git a/src/Homotopy/Space/Sphere.lagda.md b/src/Homotopy/Space/Sphere.lagda.md index 1a78c6adf..bb8cb006e 100644 --- a/src/Homotopy/Space/Sphere.lagda.md +++ b/src/Homotopy/Space/Sphere.lagda.md @@ -11,7 +11,7 @@ open import Homotopy.Space.Circle module Homotopy.Space.Sphere where ``` -# The -1 and 0 Spheres +# The -1 and 0 spheres In classical topology, the _topological space_ $S^n$ is typically defined as the subspace of $\bb{R}^{n+1}$ consisting of all points diff --git a/src/Homotopy/Space/Torus.lagda.md b/src/Homotopy/Space/Torus.lagda.md index 6422f547b..9332cb7e2 100644 --- a/src/Homotopy/Space/Torus.lagda.md +++ b/src/Homotopy/Space/Torus.lagda.md @@ -15,7 +15,7 @@ open import Homotopy.Space.Circle module Homotopy.Space.Torus where ``` -# The Torus +# The torus In classical topology, the two-dimensional torus $T^2$ may be defined as the product of circles, i.e., $T^2$ may be defined as $S^1 \times diff --git a/src/Logic/Propositional/Classical.lagda.md b/src/Logic/Propositional/Classical.lagda.md index ee8292b69..651b2b251 100644 --- a/src/Logic/Propositional/Classical.lagda.md +++ b/src/Logic/Propositional/Classical.lagda.md @@ -16,7 +16,7 @@ open import Meta.Brackets module Logic.Propositional.Classical where ``` -# Classical Propositional Logic {defines="classical-propositional-logic"} +# Classical propositional logic {defines="classical-propositional-logic"} Classical propositional logic is a simple classical logic that only contains "atomic" propositions and connectives like "and", "or" and "not". @@ -344,7 +344,7 @@ rename rn (¬-elim p q) = ¬-elim (rename rn p) (rename rn q) rename rn (dneg-elim p) = dneg-elim (rename rn p) ``` -## Some Elementary Theorems +## Some elementary theorems With those bits of structural work completed, we can focus our attention to some theorems. First, note that we can prove the law of excluded middle. diff --git a/src/Logic/Propositional/Classical/CNF.lagda.md b/src/Logic/Propositional/Classical/CNF.lagda.md index 613a8599a..a1f526854 100644 --- a/src/Logic/Propositional/Classical/CNF.lagda.md +++ b/src/Logic/Propositional/Classical/CNF.lagda.md @@ -21,7 +21,7 @@ import Data.List as List module Logic.Propositional.Classical.CNF where ``` -## Conjunctive Normal Forms {defines="conjunctive-normal-form CNF"} +## Conjunctive normal forms {defines="conjunctive-normal-form CNF"} As a general theme, it is often very useful to have some notion of normal-form for logical and algebraic expressions, and @@ -241,7 +241,7 @@ cnf-distrib-sound (P ∷ Ps) Q ρ = ``` -## A Naive Algorithm +## A naive algorithm Armed with these operations on CNFs, we can give a translation from propositions into CNF. However, note that this is extremely naive, and diff --git a/src/Logic/Propositional/Classical/SAT.lagda.md b/src/Logic/Propositional/Classical/SAT.lagda.md index b338c381c..2582934fd 100644 --- a/src/Logic/Propositional/Classical/SAT.lagda.md +++ b/src/Logic/Propositional/Classical/SAT.lagda.md @@ -32,7 +32,7 @@ private variable ``` --> -# SAT Solving {defines="SAT-solving SAT"} +# SAT solving {defines="SAT-solving SAT"} SAT solving is the process of determining if we can find some assignment of variables $\rho$ that makes a given formula $\phi$ in classical diff --git a/src/Order/DCPO.lagda.md b/src/Order/DCPO.lagda.md index c2b5b6187..58c350596 100644 --- a/src/Order/DCPO.lagda.md +++ b/src/Order/DCPO.lagda.md @@ -29,7 +29,7 @@ private variable ``` --> -# Directed-Complete Partial Orders +# Directed-complete partial orders Let $(P, \le)$ be a [[partial order]]. A family of elements $f : I \to P$ is a **semi-directed family** if for every $i, j$, there merely exists @@ -299,7 +299,7 @@ module Scott {o ℓ} {D E : DCPO o ℓ} (f : DCPOs.Hom D E) where mono = Subcat-hom.hom f monotone : ∀ {x y} → x D.≤ y → f # x E.≤ f # y - monotone = mono .pres-≤ + monotone = mono .pres-≤ opaque pres-directed-lub diff --git a/src/Order/DCPO/Free.lagda.md b/src/Order/DCPO/Free.lagda.md index 20985a237..43668e1f4 100644 --- a/src/Order/DCPO/Free.lagda.md +++ b/src/Order/DCPO/Free.lagda.md @@ -94,7 +94,7 @@ Free-DCPO⊣Forget-DCPO .zig = trivial! Free-DCPO⊣Forget-DCPO .zag = refl ``` -# Free Pointed DCPOs +# Free pointed DCPOs We construct the free [pointed DCPO] on a set $A$; IE a pointed DCPO $A_{\bot}$ with the property that for all pointed DCPOs $B$, @@ -538,7 +538,7 @@ Free-Pointed-dcpo⊣Forget-Pointed-dcpo .zag {B} = where module B = Pointed-dcpo B ``` -## Monad Structure +## Monad structure The adjunction from the previous section yields a monad on the category of sets, but we opt to define it by hand to get better computational behaviour. diff --git a/src/Order/DCPO/Pointed.lagda.md b/src/Order/DCPO/Pointed.lagda.md index 0a52ce3f2..6027c5d1f 100644 --- a/src/Order/DCPO/Pointed.lagda.md +++ b/src/Order/DCPO/Pointed.lagda.md @@ -289,7 +289,7 @@ Pointed-DCPOs-is-category = subcat-is-category DCPOs-is-category is-pointed-dcpo-is-prop ``` -# Reasoning with Pointed DCPOs +# Reasoning with pointed DCPOs The following module re-exports facts about pointed DCPOs, and also proves a bunch of useful lemma.s diff --git a/src/Order/Diagram/Glb.lagda.md b/src/Order/Diagram/Glb.lagda.md index bb7a0ebd4..5099b3f54 100644 --- a/src/Order/Diagram/Glb.lagda.md +++ b/src/Order/Diagram/Glb.lagda.md @@ -306,7 +306,7 @@ Top≃Glb = prop-ext! _ Glb→Top .snd ``` --> -### As Terminal Objects +### As terminal objects Bottoms are the decategorifcation of [[terminal objects]]; we don't need to require the uniqueness of the universal morphism, as we've replaced our diff --git a/src/Order/Instances/Discrete.lagda.md b/src/Order/Instances/Discrete.lagda.md index ebca449a3..233642643 100644 --- a/src/Order/Instances/Discrete.lagda.md +++ b/src/Order/Instances/Discrete.lagda.md @@ -16,7 +16,7 @@ import Order.Reasoning as Poset module Order.Instances.Discrete where ``` -# Discrete Orders +# Discrete orders Every set $A$ can be turned into a [[poset]] by defining $x \le y$ to be $x = y$. @@ -56,7 +56,7 @@ DiscF⊣Forget ._⊣_.zig {A = A} = trivial! DiscF⊣Forget ._⊣_.zag = refl ``` -## Least Upper Bounds +## Least upper bounds If $f : I \to A$ has a [[least upper bound]] in the discrete poset on $A$, then $f$ must be a constant family. diff --git a/src/Order/Instances/Pointwise.lagda.md b/src/Order/Instances/Pointwise.lagda.md index 9759a6fe2..62adf4a76 100644 --- a/src/Order/Instances/Pointwise.lagda.md +++ b/src/Order/Instances/Pointwise.lagda.md @@ -18,19 +18,22 @@ module Order.Instances.Pointwise where # The pointwise ordering -If $(B, \le)$ is a [[partially ordered set]], then so is $A \to B$, for -any type $A$ which we might choose! There might be other ways of making -$A \to B$ into a poset, of course, but the canonical way we're talking -about here is the **pointwise ordering** on $A \to B$, where $f \le g$ -iff $f(x) \le g(x)$ for all $x$. +The product of a family of [[partially ordered sets]] $\prod_{i : I} P_i$ is a +poset, for any index type $I$ which we might choose! There might be other ways +of making $\prod_{i : I} P_i$ into a poset, of course, but the canonical way +we're talking about here is the **pointwise ordering** on $\prod_{i : I} P_i$, +where $f \le g$ iff $f(x) \le g(x)$ for all $x$. + +[partially ordered sets]: Order.Base.html ```agda -Pointwise : ∀ {ℓ ℓₐ ℓᵣ} → Type ℓ → Poset ℓₐ ℓᵣ → Poset (ℓ ⊔ ℓₐ) (ℓ ⊔ ℓᵣ) -Pointwise A B = po where - open Pr B +Pointwise : ∀ {ℓ ℓₐ ℓᵣ} (I : Type ℓ) (P : I → Poset ℓₐ ℓᵣ) + → Poset (ℓ ⊔ ℓₐ) (ℓ ⊔ ℓᵣ) +Pointwise I P = po where + open module PrP {i : I} = Pr (P i) po : Poset _ _ - po .Poset.Ob = A → ⌞ B ⌟ + po .Poset.Ob = (i : I) → ⌞ P i ⌟ po .Poset._≤_ f g = ∀ x → f x ≤ g x po .Poset.≤-thin = hlevel! po .Poset.≤-refl x = ≤-refl @@ -43,7 +46,7 @@ of subsets of a fixed type, which has underlying set $A \to \Omega$. ```agda Subsets : ∀ {ℓ} → Type ℓ → Poset ℓ ℓ -Subsets A = Pointwise A Props +Subsets A = Pointwise A (λ _ → Props) ``` Another important case: when your domain is not an arbitrary type but diff --git a/src/Order/Instances/Pointwise/Diagrams.lagda.md b/src/Order/Instances/Pointwise/Diagrams.lagda.md index e42b5f021..660cd9616 100644 --- a/src/Order/Instances/Pointwise/Diagrams.lagda.md +++ b/src/Order/Instances/Pointwise/Diagrams.lagda.md @@ -27,12 +27,12 @@ notation for clarity.], then $h = f \land g$ when $I \to P$ is given the ```agda module - _ {ℓₒ ℓᵣ ℓᵢ} {I : Type ℓᵢ} (P : Poset ℓₒ ℓᵣ) - (f g h : I → ⌞ P ⌟) + _ {ℓₒ ℓᵣ ℓᵢ} {I : Type ℓᵢ} (P : I → Poset ℓₒ ℓᵣ) + (f g h : (i : I) → ⌞ P i ⌟) where is-meet-pointwise - : (∀ i → is-meet P (f i) (g i) (h i)) + : (∀ i → is-meet (P i) (f i) (g i) (h i)) → is-meet (Pointwise I P) f g h is-meet-pointwise pwise .is-meet.meet≤l i = pwise i .is-meet.meet≤l is-meet-pointwise pwise .is-meet.meet≤r i = pwise i .is-meet.meet≤r @@ -40,7 +40,7 @@ module pwise i .is-meet.greatest (lb' i) (lb' [Tag Text] -> [Tag Text] foldEquations _ (to@(TagOpen "a" attrs):tt@(TagText t):tc@(TagClose "a"):rest) - | Text.length t > 1, Text.last t == '⟨', Just href <- lookup "href" attrs = + | t `Set.notMember` don'tFold, Text.length t > 1, Text.last t == '⟨', Just href <- lookup "href" attrs = [ TagOpen "span" [("class", "reasoning-step")] , TagOpen "span" [("class", "as-written " <> fromMaybe "" (lookup "class" attrs))] , to, tt, tc ] ++ go href rest @@ -390,8 +397,8 @@ foldEquations _ (to@(TagOpen "a" attrs):tt@(TagText t):tc@(TagClose "a"):rest) go href (c:cs) = c:go href cs go _ [] = [] foldEquations False (TagClose "html":cs) = - [TagOpen "style" [], TagText ".equations { display: none !important; }", TagClose "style", TagClose "html"] - ++ foldEquations True cs + [TagOpen "style" [], TagText ".equations { display: none !important; }", TagClose "style", TagClose "html"] + ++ foldEquations True cs foldEquations has_eqn (c:cs) = c:foldEquations has_eqn cs foldEquations _ [] = [] @@ -405,7 +412,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) = { idIdent = module' , idAnchor = module' <> ".html" , idType = Nothing - , idDesc = stringify <$> (Map.lookup "description" meta <|> Map.lookup "pagetitle" meta) , idDefines = Nothing } @@ -430,7 +436,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) = { idIdent = Text.intercalate " > " . reverse $ map snd path' , idAnchor = module' <> ".html#" <> hId , idType = Nothing - , idDesc = getDesc xs , idDefines = Text.words <$> lookup "defines" keys } <$> go xs go (Div (hId, _, keys) blocks:xs) | hId /= "" = do @@ -440,7 +445,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) = { idIdent = Text.intercalate " > " . reverse $ hId:map snd path , idAnchor = module' <> ".html#" <> hId , idType = Nothing - , idDesc = getDesc blocks , idDefines = (:) hId . Text.words <$> lookup "alias" keys } <$> go xs go (_:xs) = go xs @@ -452,14 +456,6 @@ getHeaders module' markdown@(Pandoc (Meta meta) _) = write = writePlain def{ writerExtensions = enableExtension Ext_raw_html (writerExtensions def) } renderPlain inlines = either (error . show) id . runPure . write $ Pandoc mempty [Plain inlines] - -- | Attempt to find the "description" of a heading. Effectively, if a header - -- is followed by a paragraph, use its contents. - getDesc (Para x:_) = Just (renderPlain x) - getDesc (Plain x:_) = Just (renderPlain x) - getDesc (Div (_, cls, _) _:xs) | "warning" `elem` cls = getDesc xs - getDesc (BlockQuote blocks:_) = getDesc blocks - getDesc _ = Nothing - htmlInl :: Text -> Inline htmlInl = RawInline "html" diff --git a/support/shake/app/Shake/SearchData.hs b/support/shake/app/Shake/SearchData.hs index e8b5bd1c2..4dd498d28 100644 --- a/support/shake/app/Shake/SearchData.hs +++ b/support/shake/app/Shake/SearchData.hs @@ -13,7 +13,6 @@ data SearchTerm = SearchTerm { idIdent :: Text , idAnchor :: Text , idType :: Maybe Text - , idDesc :: Maybe Text , idDefines :: Maybe [Text] } deriving (Eq, Show, Ord, Generic, ToJSON, FromJSON) diff --git a/support/static/cube-128x.png b/support/static/cube-128x.png index 1365f5978..d09ffae33 100644 Binary files a/support/static/cube-128x.png and b/support/static/cube-128x.png differ diff --git a/support/static/cube-32x.png b/support/static/cube-32x.png index 33fffae7a..c649718a4 100644 Binary files a/support/static/cube-32x.png and b/support/static/cube-32x.png differ diff --git a/support/static/cube-512x.png b/support/static/cube-512x.png index 5a3b82157..d3559e1a8 100644 Binary files a/support/static/cube-512x.png and b/support/static/cube-512x.png differ diff --git a/support/static/cube-72x.png b/support/static/cube-72x.png index df46364e2..b695f46ed 100644 Binary files a/support/static/cube-72x.png and b/support/static/cube-72x.png differ diff --git a/support/static/icons/all-pages.svg b/support/static/icons/all-pages.svg new file mode 100644 index 000000000..ed4dda9a9 --- /dev/null +++ b/support/static/icons/all-pages.svg @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/support/static/icons/github.svg b/support/static/icons/github.svg new file mode 100644 index 000000000..8b427b7a6 --- /dev/null +++ b/support/static/icons/github.svg @@ -0,0 +1,3 @@ + + + diff --git a/support/static/icons/home.svg b/support/static/icons/home.svg new file mode 100644 index 000000000..c779cf756 --- /dev/null +++ b/support/static/icons/home.svg @@ -0,0 +1,4 @@ + + + + diff --git a/support/static/icons/justified.svg b/support/static/icons/justified.svg new file mode 100644 index 000000000..1e72bc5ac --- /dev/null +++ b/support/static/icons/justified.svg @@ -0,0 +1,14 @@ + + + + + + + + + + + + + + diff --git a/support/static/icons/raggedleft.svg b/support/static/icons/raggedleft.svg new file mode 100644 index 000000000..f2d18e014 --- /dev/null +++ b/support/static/icons/raggedleft.svg @@ -0,0 +1,11 @@ + + + + + + + + + + + diff --git a/support/static/icons/raggedright.svg b/support/static/icons/raggedright.svg new file mode 100644 index 000000000..99eb44f67 --- /dev/null +++ b/support/static/icons/raggedright.svg @@ -0,0 +1,11 @@ + + + + + + + + + + + diff --git a/support/static/icons/serif.svg b/support/static/icons/serif.svg new file mode 100644 index 000000000..3b2221351 --- /dev/null +++ b/support/static/icons/serif.svg @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/support/static/icons/star.svg b/support/static/icons/star.svg new file mode 100644 index 000000000..dcd6ee1d4 --- /dev/null +++ b/support/static/icons/star.svg @@ -0,0 +1,4 @@ + + + + diff --git a/support/static/icons/view-controls.svg b/support/static/icons/view-controls.svg new file mode 100644 index 000000000..48cfbf807 --- /dev/null +++ b/support/static/icons/view-controls.svg @@ -0,0 +1,12 @@ + + + + + + + + + + + + diff --git a/support/web/css/code.scss b/support/web/css/code.scss index eb8a158ba..d352cd246 100644 --- a/support/web/css/code.scss +++ b/support/web/css/code.scss @@ -26,6 +26,7 @@ div.sourceCode { div.sourceCode > pre { background-color: var(--code-bg); color: var(--code-fg); + flex-grow: 0; overflow-x: auto; @@ -122,7 +123,7 @@ a[href].hover-highlight { } // background-color: $code-bg; - font-family: 'Julia Mono', 'Iosevka', 'Fantasque Sans Mono', 'Roboto Mono', monospace; + @include monospaced; font-weight: 400; font-size: initial; @@ -158,7 +159,7 @@ code.do, span.do { color: var(--code-string); } /* Documentation */ code.an, span.an { color: var(--code-string); } /* Annotation */ code.cv, span.cv { color: var(--code-string); } /* CommentVar */ -.typeTooltip { +.type-tooltip { position: absolute; z-index: 100; @@ -166,6 +167,10 @@ code.cv, span.cv { color: var(--code-string); } /* CommentVar */ color: var(--code-fg); background: var(--code-bg); - padding: 0.3em; + &.sourceCode { + padding: 0.3em; + border: 0; + }; + box-shadow: 2px 2px 6px var(--shadow); } diff --git a/support/web/css/components/controls.scss b/support/web/css/components/controls.scss new file mode 100644 index 000000000..044cc8a34 --- /dev/null +++ b/support/web/css/components/controls.scss @@ -0,0 +1,220 @@ +@import "../vars.scss"; + +$dropdown-popup-width: 280px; +$button-size: 32px; + +div#controls { + position: sticky; + top: 3rem; + + display: flex; + flex-direction: column; + gap: 0.25em; + + --serif: ""; + --font-size: 1.3rem; + + hr { + margin: 0.75em 0em; + } +} + +button.labelled-button.button-large { + --button-size: 48px; +} + +button.labelled-button { + position: relative; + + --button-size: #{$button-size}; + width: var(--button-size); + height: var(--button-size); + + background-color: var(--text-bg); + + border-style: none; + border-radius: 5px; + + cursor: pointer; + + direction: rtl; + + .icon { + position: absolute; + top: 0; + left: 0; + display: inline-block; + + width: 100%; + height: 100%; + + background-position: center; + background-size: calc(var(--button-size) * 3/4) calc(var(--button-size) * 3/4); + background-repeat: no-repeat; + + filter: var(--icon-filter); + } + + .hover-label { + position: relative; + inset-inline-start: var(--button-size); + padding: 4px 8px; + + visibility: hidden; + z-index: 101; + + white-space: pre; + + background-color: var(--button-hover-bg); + color: var(--text-fg); + } + + &:hover { + background-color: var(--button-hover-bg); + > .hover-label { + visibility: visible; + } + } +} + +button.theme-button, button.labelled-button { + &.active { + border-style: solid; + border-width: 2px; + border-color: var(--active) !important; + } +} + +button.theme-button { + padding: 6px; + + border-style: 2px solid; + border-radius: 5px; + + position: relative; + + &.theme-button-light, &.theme-button-system { + background-color: $light-text-bg; + border-color: darken($light-text-bg, 10%); + color: $light-text-fg; + } + + &.theme-button-dark { + background-color: $dark-text-bg; + border-color: $dark-text-bg; + color: $dark-text-fg; + } + + &:hover::after { + content: ""; + display: block; + border-bottom: 3px solid var(--primary); + position: absolute; + bottom: -8px; + inset-inline-start: -1px; + width: calc(100% + 2px); + } +} + +div.dropdown { + position: relative; + margin: 0; + border: 0; + list-style: none; + + div.dropdown-popup { + position: absolute; + top: 0; + inset-inline-start: (-1 * ($dropdown-popup-width + 4px)); + visibility: hidden; + + width: $dropdown-popup-width; + min-height: $button-size; + + padding: 0.75em 0; + + z-index: 100; + + background-color: var(--popup-bg); + color: var(--text-fg); + box-shadow: 2px 2px 2px var(--shadow); + + font-family: var(--sans-serif); + font-size: 13pt; + } + + &.open { + .hover-label { visibility: hidden; } + .dropdown-popup { visibility: visible; } + } +} + +div.button-row { + display: flex; + align-items: center; + justify-content: center; + gap: 1em; + + padding: 0.25em 1em; +} + +div.setting-switch { + display: flex; + align-items: center; + justify-content: space-between; + gap: 1em; + + padding: 0.25em 1em; +} + + +label.switch { + position: relative; + display: inline-block; + + height: 24px; + width: 48px; + + input { + opacity: 0; + width: 0; + height: 0; + } + + .switch-slider { + position: absolute; + cursor: pointer; + inset: 0; + background-color: #ccc; + border-radius: $button-size; + + transition: .3s; + transition-property: transform; + } + + .switch-slider:before { + position: absolute; + content: ""; + height: 16px; + width: 16px; + left: 4px; + bottom: 4px; + background-color: white; + border-radius: 50%; + + transition: .3s; + transition-property: transform; + } + + input:checked + .switch-slider { + background-color: var(--active); + } + + input:focus + .switch-slider { + box-shadow: 0 0 1px var(--active); + } + + input:checked + .switch-slider:before { + transform: translateX(24px); + } +} diff --git a/support/web/css/components/modal.scss b/support/web/css/components/modal.scss index f46d2bc43..f465ec1f2 100644 --- a/support/web/css/components/modal.scss +++ b/support/web/css/components/modal.scss @@ -1,22 +1,23 @@ @import "../mixins.scss"; +$modal-width: 820px; + .modal { position: fixed; width: 100vw; height: 100vh; opacity: 0; - visibility: hidden; transition: all 0.3s ease; top: 0; left: 0; - display: flex; + display: none; align-items: center; justify-content: center; &.open { - visibility: visible; + display: flex; opacity: 1; transition-delay: 0s; background-color: var(--modal-bg); @@ -24,11 +25,12 @@ } &-contents { - width: 60%; - height: 60%; + width: $modal-width; + height: ($modal-width * 9 / 16); + max-width: 80%; background-color: var(--text-bg); - padding: 1em 0em 0em 0em; + padding: 0em; box-shadow: 2px 2px 6px var(--shadow); text-align: center; diff --git a/support/web/css/components/search.scss b/support/web/css/components/search.scss index 67c087f3c..71fb45287 100644 --- a/support/web/css/components/search.scss +++ b/support/web/css/components/search.scss @@ -1,14 +1,9 @@ -.search-form > input { - box-sizing: border-box; - font-size: 0.55em; - padding: 0.5em; - margin: 0 0 1em 0; - width: 100%; -} - #search-wrapper > .modal-contents { align-items: stretch; text-align: left; + + font-family: var(--sans-serif); + --font-size: 18px; } #search-results { @@ -23,24 +18,35 @@ margin: 0; } } + + &::-webkit-scrollbar { + display: none; + } + -ms-overflow-style: none; + scrollbar-width: none; } input#search-box { width: 100%; - font-size: 125%; + font-size: 100%; border: none; caret-color: var(--search-selected); background-color: var(--text-bg); + padding: 1em 1.5em 1em 1.5em; + + box-sizing: border-box; + width: 100%; + &:focus { outline: none; } } a.search-result { - padding: 0.5em; - padding-right: 0.75em; + padding: 0.1em 0.75em 0.1em 0.75em; + margin: 0.3em 0; display: block; text-decoration: none; @@ -51,14 +57,34 @@ a.search-result { color: inherit; } - &:hover, &:focus, li.active > & { + &:focus, li.active > & { border-left: 3px solid var(--search-selected); } - & h3 { + &:hover { + cursor: pointer; + } + + h3 { + margin: 0; + font-size: 0.85em; + font-weight: bold; + + span.search-module { + font-weight: normal; + } + + &.search-identifier { + @include monospaced; + // our mono font is bulkier than our sans font so it needs a + // smaller size to look comparable + font-size: 0.75em; + margin-bottom: 5px; + } + } + + > p { margin: 0; - font-weight: normal; - font-size: 1em; } > .search-header { @@ -73,17 +99,27 @@ a.search-result { color: var(--text-fg-alt); font-style: italic; } - } - & .search-type, & .search-desc { - font-size: 0.65em; + span.search-match-key { + padding-left: 1em; + font-size: 0.8em; + @include monospaced; + } } + & .search-type { font-size: 0.55em; } + & .search-desc { font-size: 0.75em; } + & .search-match { text-decoration: 2px var(--primary) underline; } } +li.search-header { + font-size: 0.8em; + padding: 0.3em 0.75em 0.3em 0.75em; +} + .search-error { padding: 0.5em; diff --git a/support/web/css/default.scss b/support/web/css/default.scss index 040eba712..7ad9807e7 100644 --- a/support/web/css/default.scss +++ b/support/web/css/default.scss @@ -1,8 +1,11 @@ @import "vars.scss"; @import "mixins.scss"; +@import "theme.scss"; + @import "components/modal.scss"; @import "components/search.scss"; @import "components/unfolded-footnote.scss"; +@import "components/controls.scss"; @import "code.scss"; @@ -18,12 +21,9 @@ html { :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)); -} - -body { - font-family: var(--serif), "Inria Sans", -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif; &.sans-serif { --serif: ""; @@ -31,6 +31,23 @@ body { --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; + } +} + +body { + font-family: var(--serif), var(--sans-serif); + width: 100%; font-size: var(--font-size); @@ -40,17 +57,6 @@ body { margin: 0; } - &.show-equations { - span.reasoning-step { - .as-written { - display: inline; - } - .alternate { - display: none; - } - } - } - span.reasoning-step { .as-written { display: none; @@ -74,10 +80,12 @@ main { box-sizing: border-box; div#post-toc-container { - aside#toc { + aside { display: none; - a[href].header-link span.header-link-emoji { - display: none; + a[href].header-link { + span.header-link-emoji { + display: none; + } } } @@ -262,12 +270,19 @@ table { // The 0 minimum is required to avoid overflow, see https://css-tricks.com/preventing-a-grid-blowout/ grid-template-columns: 1fr minmax(0, 4fr) 1fr; - aside#toc { + aside { display: block !important; + } + + aside { margin-right: 1rem; h3 { @include centered-contents; } + font-family: var(--sans-serif); + --font-size: 1.3rem; + --code-font-size: calc(0.92 * var(--font-size)); + div#toc-container { box-sizing: border-box; overflow-x: hidden; @@ -289,6 +304,17 @@ table { background-color: unset; } + a[href].header-link { + &, &:visited { + color: var(--primary) + }; + + &.current-heading { + font-weight: bold; + color: var(--text-fg); + } + } + > hr { margin-top: 0.25rem; margin-bottom: 0.25rem; @@ -396,15 +422,14 @@ details { } .commented-out > pre.Agda { - margin-top: 1em; + margin-top: 1em; margin-bottom: 1em; } -body.show-hidden-code .commented-out { - display: revert; +.commented-out.first-comment > pre.Agda { + margin-top: 0; } - div.profile { &.pfp-left { flex-direction: row; @@ -585,3 +610,12 @@ span.enclosing.liesover { background-position: center center; } } + +input { + background-color: var(--input-bg); + border: 1px solid var(--input-border); + color: var(--text-fg); + border-radius: 3px; +} + +#post-toc-container { min-height: 90vh; } diff --git a/support/web/css/mixins.scss b/support/web/css/mixins.scss index 94aa3527a..febbfccde 100644 --- a/support/web/css/mixins.scss +++ b/support/web/css/mixins.scss @@ -50,3 +50,8 @@ } } + +@mixin monospaced { + font-family: 'Julia Mono', 'Iosevka', 'Fantasque Sans Mono', 'Roboto Mono', monospace; + font-weight: 400; +} diff --git a/support/web/css/theme.scss b/support/web/css/theme.scss new file mode 100644 index 000000000..c65253dc1 --- /dev/null +++ b/support/web/css/theme.scss @@ -0,0 +1,130 @@ +@import "vars.scss"; + +:root, :root.light-theme { + --text-bg: #{$light-text-bg}; + --text-fg: #{$light-text-fg}; + --text-fg-alt: #{$bluegray-800}; + --shadow: #000; + + --primary: #{$light-code-blue}; + --secondary: #{$light-code-purple}; + --active: #{$light-code-blue}; + + --modal-bg: #ccccccaa; + + --warning-bg: #{$yellow-400}; + --warning-icon: #{$yellow-700}; + + --note-bg: #{$violet-500}; + --note-icon: #{$violet-600}; + + --terminology-bg: #{$cyan-600}; + --terminology-icon: #{$cyan-900}; + + --code-bg: var(--text-bg); + --code-fg: var(--text-fg); + + --code-keyword: #{$light-code-orange}; + --code-string: #{$light-code-red}; + --code-number: #{$light-code-pink}; + --code-module: #{$light-code-pink}; + --code-field: #{$light-code-purple}; + --code-constructor: #{$light-code-green}; + --code-highlight: #F5DEB3; + + --search-selected: #{$violet-800}; + + --details-summary: #{$cyan-100}; + --details-open: #{$cyan-200}; + + --depgraph-edge: #eee; + --blockquote-bg: #{$purple-300}; + + --tooltip-bg: #{$zinc-300}; + --button-hover-bg: #{$light-button-hover-bg}; + + --input-bg: #{$light-text-bg}; + --input-border: #{lighten($light-text-fg, 30%)}; + + --popup-bg: #{$light-text-bg}; + --icon-filter: none; + + .diagram-dark { + display: none !important; + } + + .diagram-light { + display: block !important; + } +} + +@mixin dark-theme-vars { + --text-bg: #{$dark-text-bg}; + --text-fg: #{$dark-text-fg}; + --text-fg-alt: #{$bluegray-200}; + --shadow: black; + + --primary: #{$dark-code-blue}; + --secondary: #{$dark-code-pink}; + --active: #4267BD; + + --modal-bg: #282C34aa; + + --warning-bg: #{$yellow-500}; + --warning-icon: #{$yellow-400}; + + --note-bg: #{$violet-500}; + --note-icon: #{$violet-400}; + + --terminology-bg: #{$cyan-600}; + --terminology-icon: #{$cyan-700}; + + --code-bg: var(--text-bg); + --code-fg: var(--text-fg); + + --code-keyword: #{$dark-code-yellow}; + --code-string: #{$dark-code-red}; + --code-number: #{$dark-code-green}; + --code-module: #{$dark-code-cyan}; + --code-field: #{$dark-code-pink}; + --code-constructor: #{$dark-code-green}; + --code-highlight: #ef444499; + + --search-selected: #{$cyan-900}; + + --depgraph-edge: #{$bluegray-600}; + --blockquote-bg: #{$bluegray-600}; + + --input-bg: #{$bluegray-700}; + --input-border: #{$bluegray-600}; + + --popup-bg: #282C34; + --button-hover-bg: #3b4454; + --icon-filter: invert(79%) sepia(10%) saturate(306%) hue-rotate(181deg) brightness(89%) contrast(92%);; + + .diagram-dark { + display: block !important; + } + + .diagram-light { + display: none !important; + } + + div.warning { + --shadow: #{$red-900}; + } + + body { + scrollbar-color: #3b4454 #2b2e33; + } +} + +:root.dark-theme { + @include dark-theme-vars; +} + +@media (prefers-color-scheme: dark) { + :root { + @include dark-theme-vars; + } +} diff --git a/support/web/css/vars.scss b/support/web/css/vars.scss index ab3efa6f4..a27f81d60 100644 --- a/support/web/css/vars.scss +++ b/support/web/css/vars.scss @@ -1,3 +1,27 @@ +$nav-height: 48px; +$page-padding: 3rem; + +$light-code-red: #d52753; +$light-code-red-br: #AE3B36; +$light-code-green: #207B1D; +$light-code-yellow: #DEB468; +$light-code-orange: #BB3B13; +$light-code-blue: #0054F4; +$light-code-pink: #8A1060; +$light-code-purple: #9C1BD6; +$light-code-violet: #7A82DA; +$light-code-cyan: #48A8B5; +$light-code-white: #ABB2BF; +$light-code-grey: #7F848E; + +$dark-code-red: #E06C75; +$dark-code-green: #98C379; +$dark-code-yellow: #E5C07B; +$dark-code-blue: #61AFEF; +$dark-code-pink: #C878DD; +$dark-code-purple: #992eb4; +$dark-code-cyan: #56B6C2; + $purple-50: #faf5ff; $purple-100: #f3e8ff; $purple-200: #e9d5ff; @@ -63,127 +87,21 @@ $cyan-700: #0097a7; $cyan-800: #00838f; $cyan-900: #006064; -$nav-height: 48px; -$page-padding: 3rem; - -$light-code-red: #d52753; -$light-code-red-br: #AE3B36; -$light-code-green: #207B1D; -$light-code-yellow: #DEB468; -$light-code-orange: #BB3B13; -$light-code-blue: #0054F4; -$light-code-pink: #8A1060; -$light-code-purple: #9C1BD6; -$light-code-violet: #7A82DA; -$light-code-cyan: #48A8B5; -$light-code-white: #ABB2BF; -$light-code-grey: #7F848E; - -$dark-code-red: #E06C75; -$dark-code-green: #98C379; -$dark-code-yellow: #E5C07B; -$dark-code-blue: #61AFEF; -$dark-code-pink: #C878DD; -$dark-code-purple: #992eb4; -$dark-code-cyan: #56B6C2; - -:root { - --text-bg: #fff; - --text-fg: #222; - --text-fg-alt: #{$bluegray-800}; - --shadow: #000; - - --primary: #{$light-code-blue}; - --secondary: #{$light-code-purple}; - - --modal-bg: #ccccccaa; - - --warning-bg: #{$yellow-400}; - --warning-icon: #{$yellow-700}; - - --note-bg: #{$violet-500}; - --note-icon: #{$violet-600}; - - --terminology-bg: #{$cyan-600}; - --terminology-icon: #{$cyan-900}; - - --code-bg: var(--text-bg); - --code-fg: var(--text-fg); - - --code-keyword: #{$light-code-orange}; - --code-string: #{$light-code-red}; - --code-number: #{$light-code-pink}; - --code-module: #{$light-code-pink}; - --code-field: #{$light-code-purple}; - --code-constructor: #{$light-code-green}; - --code-highlight: #F5DEB3; - - --search-selected: #{$violet-800}; - - --details-summary: #{$cyan-100}; - --details-open: #{$cyan-200}; - - --depgraph-edge: #eee; - --blockquote-bg: #{$purple-300}; -} - -.diagram-dark { - display: none !important; -} - -@media (prefers-color-scheme: dark) { - :root { - --text-bg: #282C34; - --text-fg: #bfbfbf; - --text-fg-alt: #{$bluegray-200}; - --shadow: #{$bluegray-600}; - - --primary: #{$dark-code-blue}; - --secondary: #{$dark-code-pink}; - - --modal-bg: #282C34aa; - - --warning-bg: #{$yellow-500}; - --warning-icon: #{$yellow-400}; - - --note-bg: #{$violet-500}; - --note-icon: #{$violet-400}; - - --terminology-bg: #{$cyan-600}; - --terminology-icon: #{$cyan-700}; - - --code-keyword: #{$dark-code-yellow}; - --code-string: #{$dark-code-red}; - --code-number: #{$dark-code-green}; - --code-module: #{$dark-code-cyan}; - --code-field: #{$dark-code-pink}; - --code-constructor: #{$dark-code-green}; - --code-highlight: #ef444499; - - --search-selected: #{$cyan-900}; - - --depgraph-edge: #{$bluegray-600}; - --blockquote-bg: #{$bluegray-600}; - } - - div.warning { - --shadow: #{$red-900} - } - - input { - background-color: $bluegray-700; - border: 1px solid $bluegray-600; - color: var(--text-fg); - } - - body { - scrollbar-color: #3b4454 #2b2e33; - } - - .diagram-dark { - display: block !important; - } - .diagram-light { - display: none !important; - } -} +$zinc-50: #fafafa; +$zinc-100: #f4f4f5; +$zinc-200: #e4e4e7; +$zinc-300: #d4d4d8; +$zinc-400: #a1a1aa; +$zinc-500: #71717a; +$zinc-600: #52525b; +$zinc-700: #3f3f46; +$zinc-800: #27272a; +$zinc-900: #18181b; +$zinc-950: #09090b; + +$light-text-bg: #fff; +$light-text-fg: #222; +$light-button-hover-bg: $zinc-200; + +$dark-text-bg: #23272E; +$dark-text-fg: #ABB2BF; diff --git a/support/web/js/code-only.ts b/support/web/js/code-only.ts index 84d354b77..3fb5a7d63 100644 --- a/support/web/js/code-only.ts +++ b/support/web/js/code-only.ts @@ -4,3 +4,4 @@ import "./equations"; import "./highlight-hover"; import "./search"; +import "./prompt"; diff --git a/support/web/js/depgraph.tsx b/support/web/js/depgraph.tsx index 16470db44..1701d47b2 100644 --- a/support/web/js/depgraph.tsx +++ b/support/web/js/depgraph.tsx @@ -146,7 +146,7 @@ function render(nodes: d3.Selection d === undefined ? "" : `translate(${d.x as number + d.radius}, ${d.y as number - 5})`) .attr('visibility', d => { if (d.id === page || d.hover) { - return ''; + return 'visible'; } return 'hidden'; }); diff --git a/support/web/js/equations.ts b/support/web/js/equations.ts index e292eaf29..ba139694c 100644 --- a/support/web/js/equations.ts +++ b/support/web/js/equations.ts @@ -1,100 +1,59 @@ -const lsItem = "1lab.eqn_display"; -let equations_displayed = false; -if (window.localStorage.getItem(lsItem) === "displayed") { - equations_displayed = true; -} - -const sfItem = "1lab.serif_font"; -let serif_font = false; -if (window.localStorage.getItem(sfItem) === "displayed") { - serif_font = true; -} - -const saveEqnDisplay = () => { - window.localStorage.setItem(lsItem, equations_displayed ? "displayed" : "hidden"); -}; - -const saveFontDisplay = () => { - window.localStorage.setItem(sfItem, serif_font ? "displayed" : "hidden"); -}; +import { equationSetting, hiddenCodeSetting, serifFontSetting } from "./lib/settings"; window.addEventListener("DOMContentLoaded", () => { - const buttons: NodeListOf = document.querySelectorAll("input.equations"); - const body = document.body; - if (equations_displayed) { - body.classList.add("show-equations"); - } else { - body.classList.remove("show-equations"); - } + /* I tried really hard to do this with only CSS but :first-of-type is + * only for *type*, and there'll be a div before the first comment (the + * narrow screen navigation). So this bit of JS adds the + * `first-comment` class to the first commented-out block so we can get + * rid of its top margin. */ + const firstComment = Array.from(document.querySelector("article")?.children ?? []) + .filter(e => e instanceof HTMLDivElement && e.classList.contains("commented-out")); - if (serif_font) { - body.classList.remove("sans-serif"); - } else { - body.classList.add("sans-serif"); + if (firstComment.length >= 1) { + firstComment[0].classList.add("first-comment"); } + hiddenCodeSetting.onChange((t) => { + if (t) { + document.querySelectorAll("details").forEach(d => d.setAttribute("open", "true")) + } else { + document.querySelectorAll("details").forEach(d => d.removeAttribute("open")) + } + }); + + const buttons: NodeListOf = document.querySelectorAll("input.equations"); + buttons.forEach(button => { if (!button.classList.contains("narrow-only")) { button.style.display = "block"; } - if (button.checked !== undefined) button.checked = equations_displayed; + equationSetting.onChange((t) => { + if (button.checked !== undefined) button.checked = t; + button.innerText = t ? "Hide equations" : "Show equations"; + }); button.onclick = () => { - equations_displayed = !equations_displayed; - - if (equations_displayed) { - body.classList.add("show-equations"); - } else { - body.classList.remove("show-equations"); - } - - saveEqnDisplay(); - - buttons.forEach((button) => { - if (button.checked !== undefined) button.checked = equations_displayed; - - if (equations_displayed) { - button.innerText = "Hide equations"; - } else { - button.innerText = "Show equations"; - } - }); + equationSetting.toggle(); }; }); const toggleFont = document.getElementById("toggle-fonts") as HTMLInputElement | null; - if (toggleFont) { - toggleFont.checked = serif_font; - toggleFont.onclick = () => { - serif_font = toggleFont.checked; - - if (serif_font) { - body.classList.remove("sans-serif"); - } else { - body.classList.add("sans-serif"); - } - saveFontDisplay(); - }; + if (toggleFont) { + serifFontSetting.onChange((t) => { + window.requestAnimationFrame(() => { toggleFont.checked = t }); + }); + toggleFont.onclick = () => serifFontSetting.toggle(); } const showHiddenCode = document.getElementById("sidebar-hidden") as HTMLInputElement | null; if (showHiddenCode) { - showHiddenCode.onchange = () => { - if (showHiddenCode.checked) - body.classList.add("show-hidden-code"); - else - body.classList.remove("show-hidden-code"); - - document.querySelectorAll("details").forEach(d => { - if (showHiddenCode.checked) - d.setAttribute("open", ""); - else - d.removeAttribute("open"); - }); - }; + showHiddenCode.onclick = () => hiddenCodeSetting.toggle(); + hiddenCodeSetting.onChange((t) => { + window.requestAnimationFrame(() => { showHiddenCode.checked = t }); + }); } scrollToHash(); @@ -103,23 +62,22 @@ window.addEventListener("DOMContentLoaded", () => { window.addEventListener("hashchange", scrollToHash); function scrollToHash() { - if (window.location.hash != '') { - const id = window.location.hash.slice(1); - // #id doesn't work with numerical IDs - const elem = document.querySelector(`[id="${id}"]`) as HTMLInputElement | null; - if (elem) { - // If the element is in a commented-out block or a
tag, unhide it - // and scroll to it. - const commentedOut = elem.closest('.commented-out') as HTMLInputElement | null; - if (commentedOut) - commentedOut.style.display = 'revert'; - const details = elem.closest('details') as HTMLInputElement | null; - if (details) - details.setAttribute("open", ""); - if (commentedOut || details) - elem.scrollIntoView(); - } - } + if (window.location.hash === '') return; + + const id = window.location.hash.slice(1); + // #id doesn't work with numerical IDs + const elem = document.querySelector(`[id="${id}"]`); + if (!(elem instanceof HTMLInputElement)) return; + // If the element is in a commented-out block or a
tag, unhide it + // and scroll to it. + const commentedOut = elem.closest('.commented-out') as HTMLInputElement | null; + if (commentedOut) + commentedOut.style.display = 'revert'; + const details = elem.closest('details') as HTMLInputElement | null; + if (details) + details.setAttribute("open", ""); + if (commentedOut || details) + elem.scrollIntoView(); } export { }; diff --git a/support/web/js/highlight-hover.ts b/support/web/js/highlight-hover.ts index 23dff465e..59012dd62 100644 --- a/support/web/js/highlight-hover.ts +++ b/support/web/js/highlight-hover.ts @@ -29,7 +29,7 @@ document.addEventListener('highlight', (({ detail: { link, on } }: CustomEvent) if (on) { currentHover = document.createElement("div"); currentHover.innerText = type; - currentHover.classList.add("typeTooltip", "sourceCode"); + currentHover.classList.add("type-tooltip", "sourceCode"); document.body.appendChild(currentHover); const selfRect = link.getBoundingClientRect(); @@ -38,9 +38,9 @@ document.addEventListener('highlight', (({ detail: { link, on } }: CustomEvent) // 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 - 2em`; + currentHover.style.top = `calc(${link.offsetTop - hoverRect.height}px - 1em`; } else { - currentHover.style.top = `${link.offsetTop + link.offsetHeight}px`; + currentHover.style.top = `${link.offsetTop + (link.offsetHeight / 2)}px`; } currentHover.style.left = `${link.offsetLeft}px`; } diff --git a/support/web/js/lib/jsx.ts b/support/web/js/lib/jsx.ts index 4038dae8d..947b7fb48 100644 --- a/support/web/js/lib/jsx.ts +++ b/support/web/js/lib/jsx.ts @@ -1,6 +1,6 @@ export type Content = HTMLElement | string | Content[] | undefined; -const add = (element: HTMLElement, child: Content) => { +const add = (element: Node, child: Content) => { if (typeof child === "string") { element.appendChild(document.createTextNode(child.toString())); } else if (child instanceof Array) { @@ -28,12 +28,16 @@ export class JSX { ...content: Content[] ): Node { if (typeof name !== "string") { - return name(arg); + const elt = name(arg); + for (const c of content) { + add(elt, c); + } + return elt; } else { const element = document.createElement(name); const props = (arg as { [id: string]: string | boolean }) || {}; - for (let name in props) { + for (const name in props) { if (name && props.hasOwnProperty(name)) { let value = props[name]; if (value === true) { @@ -44,8 +48,8 @@ export class JSX { } } - for (let i = 0; i < content.length; i++) { - add(element, content[i]); + for (const c of content) { + add(element, c); } return element; } diff --git a/support/web/js/lib/settings.tsx b/support/web/js/lib/settings.tsx new file mode 100644 index 000000000..66517c9c6 --- /dev/null +++ b/support/web/js/lib/settings.tsx @@ -0,0 +1,76 @@ +export class Setting { + private readonly key: string; + private _value: T; + private readonly _onChange: ((value: T) => void)[]; + + public readonly name: string; + + constructor (name: string, def: T) { + this.name = name; + this.key = name.toLowerCase().replace(/[^a-z]/g, '_'); + console.log(this.key); + + let it = window.localStorage.getItem(this.key); + if (!it) { + this._value = def + } else { + this._value = JSON.parse(it) ?? def; + }; + + this._onChange = []; + } + + get value(): T { + return this._value; + } + + set value(to: T) { + if (this._value === to) return; + this._value = to; + window.localStorage.setItem(this.key, JSON.stringify(to)); + for (const listener of this._onChange) { + listener(to); + } + } + + public toggle(this: Setting): boolean { + return (this.value = !this.value); + } + + public onChange(listener: (value: T) => void) { + this._onChange.push(listener); + listener(this.value); + return this; + } +} + +const clz = document.documentElement.classList; + +export type Theme = 'light' | 'dark' | 'system'; + +export const equationSetting = new Setting("equations", false) + .onChange((v) => v ? clz.add("show-equations") : clz.remove("show-equations")); + +export const serifFontSetting = new Setting("sans_serif", false) + .onChange((v) => v ? clz.remove("sans-serif") : clz.add("sans-serif")); + +export const hiddenCodeSetting = new Setting("hidden_code", false) + .onChange((v) => v ? clz.add("show-hidden-code") : clz.remove("show-hidden-code")); + +export const footnoteSetting = new Setting("inline_footnotes", false) + +export const themeSetting = new Setting("prefer_theme", 'system').onChange((t) => { + switch(t) { + case "light": + clz.add("light-theme"); + clz.remove("dark-theme"); + break; + case "dark": + clz.remove("light-theme"); + clz.add("dark-theme"); + break; + case "system": + clz.remove("light-theme", "dark-theme"); + break; + } +}); diff --git a/support/web/js/main.ts b/support/web/js/main.ts index bfe2827ee..93aa61e5f 100644 --- a/support/web/js/main.ts +++ b/support/web/js/main.ts @@ -3,3 +3,6 @@ import "./equations"; import "./highlight-hover"; import "./search"; import "./unfold"; +import "./sidebar"; +import "./prompt"; +import "./theme"; diff --git a/support/web/js/prompt.tsx b/support/web/js/prompt.tsx new file mode 100644 index 000000000..5b45022bc --- /dev/null +++ b/support/web/js/prompt.tsx @@ -0,0 +1,363 @@ +import { JSX } from "./lib/jsx"; +import { isExact, type PromptItemResult, sortPromptItem } from "./prompt/items"; +import { allSections } from "./prompt/sections"; + +// Components of the search box. These are always in the DOM. +const searchInput = as HTMLInputElement; + +// Annoyingly, in addition to the input box itself, we need to keep +// track of all these bits. First, the result list, for.. adding search +// results; +const searchResults =
; + +// The actual search popup itself, to use for clipping later; +const searchContents = +
+ {searchInput} +
+ {searchResults} +
+
+ +// And the overall modal, which we need to control the visibility and +// also to attach the opening/closing event. +const searchWrapper = + ; + +/** Unmark an element as being active. */ +const removeActive = (elem: Element) => { + elem.classList.remove("active"); + elem.ariaSelected = "false"; +}; + +/** Mark an element as being active. */ +const addActive = (elem: Element) => { + elem.classList.add("active"); + elem.ariaSelected = "true"; + elem.scrollIntoView({ + block: "nearest", + }); +}; + +/** If an element is currently active, unmark it, and return the element; + * If nothing is selected, this function has no effect. */ +const unselect = (): Element | undefined => { + const active = searchResults.querySelector("li.active"); + if (!active) return; + removeActive(active); + return active; +} + +/** Indicates whether the mouse has been moved since the last time the + * user has used the keyboard to change the active item. */ +let mouseSelection = true; + +const itemAfter = (item: Node) => + document.evaluate("following-sibling::li[@class=\"search-item\"][1]", item, null, + XPathResult.FIRST_ORDERED_NODE_TYPE).singleNodeValue + +const itemBefore = (item: Node) => + document.evaluate("preceding-sibling::li[@class=\"search-item\"][1]", item, null, + XPathResult.FIRST_ORDERED_NODE_TYPE).singleNodeValue + +const sectionBefore = (item: Node) => + document.evaluate("preceding-sibling::li[@class=\"search-header\"][2]", item, null, + XPathResult.FIRST_ORDERED_NODE_TYPE).singleNodeValue + +const sectionAfter = (item: Node) => + document.evaluate("following-sibling::li[@class=\"search-header\"][1]", item, null, + XPathResult.FIRST_ORDERED_NODE_TYPE).singleNodeValue + +/** Select the next item. */ +const moveNext = () => { + const active = unselect(); + let next; + mouseSelection = false; + + const top = () => { + const elem = searchResults.querySelector("li.search-item"); + if (elem) addActive(elem); + }; + + if (!active) { + top(); + } else if ((next = itemAfter(active)) instanceof Element) { + addActive(next); + } +}; + +/** Select the previous item. */ +const movePrevious = () => { + const active = searchResults.querySelector("li.active"); + let next; + mouseSelection = false; + + if (active && (next = itemBefore(active)) instanceof Element) { + removeActive(active); + addActive(next); + } else if (active && !next) { + console.log("No previous item!"); + searchResults.parentElement?.scrollTo(0, 0); + } +}; + +const moveNextSection = () => { + const active = searchResults.querySelector("li.active"); + if (!active) return moveNext(); + let nexts, next; + mouseSelection = false; + + if ((nexts = sectionAfter(active)) instanceof Element && (next = itemAfter(nexts)) instanceof Element) { + removeActive(active); + addActive(next); + } +}; + +const movePreviousSection = () => { + const active = searchResults.querySelector("li.active"); + let nexts, next; + mouseSelection = false; + + if (active && (nexts = sectionBefore(active)) instanceof Element && (next = itemAfter(nexts)) instanceof Element) { + removeActive(active); + nexts.scrollIntoView(); + addActive(next); + } +}; + +/** Close the search box. Unsets the selected item, if any. */ +export const closeSearch = () => { + unselect(); + + searchWrapper.classList.remove("open") +}; + + +/** Create the element corresponding to a given {@link PromptItemResult}. + * Also connects the event handlers for selecting and activating this + * item. */ +const renderItem = ({ item, original, match }: PromptItemResult) => { + const li = +
  • + + {item.render(original, match)} + +
    • ; + + li.addEventListener("mouseover", () => { + if (!mouseSelection) return; + + unselect(); + addActive(li); + }); + + li.addEventListener("mousemove", () => { + mouseSelection = true; + + unselect(); + addActive(li); + }); + + li.onclick = () => { + if (item.activate() === 'close') { + closeSearch() + } else { + li.replaceChildren( + + {item.render(original, match)} + ); + }; + }; + + return li; +}; + +let searchTask: number = 0; + +class DeferredItems { + private readonly results: PromptItemResult[]; + private readonly task: number; + private readonly query: string; + private writeHead: HTMLElement; + + private readHead: number = 0; + private batchSize: number = 128; + + constructor (r: PromptItemResult[], h: HTMLElement, t: number, q: string) { + this.results = r; + this.writeHead = h; + this.task = t; + this.query = q; + } + + public trigger() { + let last: HTMLElement = this.writeHead; + if (this.task !== searchTask || this.readHead >= this.results.length) return + + const lim = Math.min(this.results.length, this.readHead + this.batchSize); + console.log(`Rendering deferred batch of ${lim - this.readHead} results for "${this.query}"`); + + for (let i = this.readHead; i < lim; i++) { + const elt = renderItem(this.results[i]); + last.insertAdjacentElement('afterend', elt); + last = elt; + } + + this.writeHead = last; + this.readHead = this.readHead + this.batchSize, this.batchSize = Math.min(512, this.batchSize * 2); + + window.requestAnimationFrame(() => { this.trigger() }); + } +} + +/** Perform and render the results of a query. */ +const doSearch = (search: string) => { + const rendered: HTMLElement[] = []; + const task = ++searchTask; + + if (search === "") { + allSections.forEach(s => { + const es = s.defaultEntries(); + if (es.length <= 0) return; + rendered.push(s.header); + es.forEach(i => rendered.push(renderItem(i))); + }); + } else { + const exacts: PromptItemResult[] = []; + + allSections.forEach(s => { + const results: PromptItemResult[] = []; + s.doSearch(search).forEach(e => isExact(search, e) ? exacts.push(e) : results.push(e)); + if (results.length === 0) return; + + rendered.push(s.header); + + let now = results.slice(0, 32).map(renderItem); + rendered.push(...now); + + const later = new DeferredItems(results.slice(32), now[now.length - 1], task, search); + window.setTimeout(() => later.trigger(), 200); + }); + + if (exacts.length > 0) { + rendered.unshift(...exacts.sort(sortPromptItem(search)).map(renderItem)); + rendered.unshift(
  • Exact matches
    • ); + } + } + + // We replace the children atomically down here to prevent flashing. + searchResults.replaceChildren(...rendered); + searchResults.parentElement?.scrollTo(0, 0); +} + +// That was the hard part, now we just need to connect some event +// handlers. + +searchInput.addEventListener("input", () => { + doSearch(searchInput.value); +}); + +let searchReady = false, searchPending = false; +document.addEventListener("searchready", () => { + searchReady = true; + if (searchPending) { + searchPending = false; + window.requestAnimationFrame(() => startSearch()); + } +}); + +const startSearch = () => { + if (!searchReady) { + searchPending = true; + return; + } + + mouseSelection = true; + searchInput.value = ''; + + searchWrapper.classList.add("open"); + searchInput.focus(); + + doSearch(searchInput.value); +}; + +const isSearching = () => searchWrapper.classList.contains("open"); + +searchWrapper.addEventListener("click", e => { + const cts = searchContents.getBoundingClientRect(); + let fake = e.clientX === 0 && e.clientY === 0; + let inside = + (e.clientX > cts.left && e.clientX < cts.right) && + (e.clientY > cts.top && e.clientY < cts.bottom); + if (!inside && !fake) { closeSearch(); return; } +}); + +document.addEventListener("DOMContentLoaded", () => { + document.body.appendChild(searchWrapper); + + searchInput.addEventListener("keydown", (e) => { + switch (e.key) { + case "Tab": + e.preventDefault(); + if (e.shiftKey) movePrevious(); else moveNext(); + break; + + case "Down": + case "ArrowDown": + e.preventDefault(); + moveNext(); + break; + + case "Up": + case "ArrowUp": + e.preventDefault(); + movePrevious(); + break; + + case "Left": + case "ArrowLeft": + if (!e.ctrlKey) return; + e.preventDefault(); + movePreviousSection(); + break; + + case "Right": + case "ArrowRight": + if (!e.ctrlKey) return; + e.preventDefault(); + moveNextSection(); + break; + + case "Enter": { + e.preventDefault(); + + const link: HTMLAnchorElement | null = searchResults.querySelector("li.active > a.search-result"); + link?.click(); + break; + } + } + }); + + const searchInputProxy = document.getElementById("search-box-proxy") as HTMLInputElement | null; + if (searchInputProxy) { + searchInputProxy.addEventListener("focus", () => startSearch()); + } + + document.addEventListener("keydown", e => { + if (e.key == "k" && e.ctrlKey && !e.altKey) { + e.preventDefault(); + if (isSearching()) { + closeSearch(); + } else { + startSearch(); + }; + } else if (e.key === "Escape" && isSearching()) { + e.preventDefault(); + closeSearch(); + } + }); +}); + +export { }; diff --git a/support/web/js/prompt/items.tsx b/support/web/js/prompt/items.tsx new file mode 100644 index 000000000..4f595b755 --- /dev/null +++ b/support/web/js/prompt/items.tsx @@ -0,0 +1,134 @@ +import { Searcher } from "fast-fuzzy"; +import { JSX, type Content } from "../lib/jsx"; + +export type MatchedSpan = { index: number, length: number }; +export type ActionAfter = 'keep' | 'close'; + +export interface PromptItem { + readonly selectors: string[]; + readonly priority: number; + + readonly onlySearch?: boolean; + + render(key: string, matched?: MatchedSpan): Content; + activate(): ActionAfter; +} + +export const highlight = (original: string, match?: MatchedSpan): Content => { + if (!match) return original; + const { index, length } = match; + + if (length == 0) return original; + if (index == 0 && length == original.length) return {original}; + + const out: Array = []; + + if (index > 0) out.push(original.substring(0, index)); + out.push({original.substring(index, index + length)}); + out.push(original.substring(index + length)); + + return out; +}; + +export const spanMaybe = (c: Content): Content => { + if (Array.isArray(c)) { + return {c} + } else { + return c + }; +} + +export type PromptItemResult = { item: PromptItem, match: MatchedSpan, original: string }; + +export interface Context { + renderItem(it: PromptItemResult): HTMLElement; + + rendered: HTMLElement[]; + pushLate(it: HTMLElement): void; +} + +export function isExact(q: string, e: PromptItemResult, sensitive?: boolean): boolean { + let pred; + if (sensitive) { + pred = (v: string) => v === q; + } else { + pred = (v: string) => v.toLowerCase() === q.toLowerCase(); + } + return e.item.selectors.findIndex(pred) >= 0; +} + +export function sortPromptItem(search: string) { + return (p1: PromptItemResult, p2: PromptItemResult): number => { + let aex = isExact(search, p1, true) + let bex = isExact(search, p2, true); + if (aex && !bex) { + return -1; + } else if (!aex && bex) { + return 1; + } + if (p1.item.priority === p2.item.priority) { + return p1.item.selectors[0].localeCompare(p2.item.selectors[0]); + } + return p2.item.priority - p1.item.priority; + } +}; + +export class Section { + private readonly entries: PromptItemResult[]; + private readonly searcher: Searcher; + + public readonly header: HTMLElement; + private sorted: boolean; + + constructor (header: HTMLElement) { + this.entries = []; + this.sorted = true; + + this.searcher = new Searcher([], { + returnMatchData: true, + ignoreSymbols: true, + ignoreCase: true, + useSellers: true, + keySelector: (x: PromptItem) => x.selectors, + }); + + this.header = header; + } + + private sort() { + if (this.sorted) return; + this.entries.sort(sortPromptItem("")); + this.sorted = true; + } + + public pushPromptItems(...i: PromptItem[]) { + let res = i.map(x => ({ item: x, match: { index: 0, length: 0 }, original: x.selectors[0] })); + + this.entries.push(...res); + this.searcher.add(...i); + + this.sorted = false; + } + + /** Insert a list of {@link PromptItem}s at the end of the {@link promptItems} list. + * + * When no search query is present, these will be the shown after any previously-added items. */ + public unshiftPromptItems(...i: PromptItem[]) { + let res = i.map(x => ({ item: x, match: { index: 0, length: 0 }, original: x.selectors[0] })); + + this.entries.unshift(...res); + this.searcher.add(...i); + + this.sorted = false; + } + + public defaultEntries(): PromptItemResult[] { + this.sort(); + + return this.entries.filter((e) => !e.item.onlySearch).slice(0, 512); + } + + public doSearch(search: string): PromptItemResult[] { + return this.searcher.search(search); + } +} diff --git a/support/web/js/prompt/sections.tsx b/support/web/js/prompt/sections.tsx new file mode 100644 index 000000000..63bedb3df --- /dev/null +++ b/support/web/js/prompt/sections.tsx @@ -0,0 +1,12 @@ +import { Section } from "./items"; +import { JSX } from "../lib/jsx"; + +export const Miscellanea: Section = new Section(
  • Search results
    • ); +export const InThisPage: Section = new Section(
  • In this page
    • ); +export const Settings: Section = new Section(
  • Settings
    • ); + +export const allSections: Section[] = [ + Settings, + InThisPage, + Miscellanea, +]; diff --git a/support/web/js/search.tsx b/support/web/js/search.tsx index 699ce9ff2..1f5019188 100644 --- a/support/web/js/search.tsx +++ b/support/web/js/search.tsx @@ -1,224 +1,76 @@ -import { Searcher, MatchData } from "fast-fuzzy"; -import { JSX, Content } from "./lib/jsx"; +import { JSX, type Content } from "./lib/jsx"; +import { type MatchedSpan, type PromptItem, highlight, spanMaybe } from "./prompt/items"; +import { InThisPage, Miscellanea } from "./prompt/sections"; type SearchItem = { idIdent: string, idAnchor: string, idType: string | null, - idDesc: string | null, idDefines: string[] | null, }; -const highlight = ({ match, original }: MatchData): Content => { - if (match.length == 0) return original; +const makeSearch = (e: SearchItem, thisp: boolean): PromptItem => { + const sel: string[] = [ e.idIdent, ...e.idDefines ?? [] ]; + const original = e.idIdent; - if (match.index == 0 && match.length == original.length) return {original}; - - const out: Array = []; - if (match.index > 0) out.push(original.substring(0, match.index)); - out.push({original.substring(match.index, match.index + match.length)}); - out.push(original.substring(match.index + match.length)); - return out; -}; - -let loadingIndex = false; -let index: Searcher | null; - -const startSearch = (mirrorInput: HTMLInputElement | null) => { - if (document.getElementById("search-wrapper")) return; - - const searchInput = as HTMLInputElement; - const searchResults =
    ; - const searchWrapper = ; - - const setError = (contents: string) => { - searchResults.innerHTML = ""; - searchResults.appendChild({contents}); - }; - - const doSearch = () => { - if (!index) return; - - const results = index.search(searchInput.value); - - if (results.length > 0) { - searchResults.scrollTo(0, 0); - searchResults.innerHTML = ""; - - const list = ; - - - searchResults.appendChild(list); - } else if (searchInput.value.length === 0) { - searchResults.innerHTML = ""; - } else { - searchResults.innerText = "No results found"; - } - }; - - // Input handlers - - searchInput.addEventListener("input", () => { - if (mirrorInput) mirrorInput.value = searchInput.value; - doSearch(); - }); - - // While searchInputProxy should never be focused for long, let's process those events anyway. - const syncMirrorInput = () => { - if (mirrorInput) searchInput.value = mirrorInput.value; - searchInput.focus(); - doSearch(); - }; - if (mirrorInput) mirrorInput.addEventListener("input", syncMirrorInput); - - const closeSearch = () => { - searchWrapper.remove() - if (mirrorInput) mirrorInput.removeEventListener("input", syncMirrorInput); - }; - - searchWrapper.addEventListener("click", e => { - if (e.target !== searchInput) closeSearch(); - }); - - // Keyboard navigation through search items - - const removeActive = (elem: Element) => { - elem.classList.remove("active"); - elem.ariaSelected = "false"; - }; - const addActive = (elem: Element) => { - elem.classList.add("active"); - elem.ariaSelected = "true"; - elem.scrollIntoView({ - block: "nearest", - }); + const desc: Content[] = []; + if (e.idType) { + desc.push(

    {e.idType}

    ) }; - const moveNext = () => { - const active = searchResults.querySelector("li.active"); - if (!active) { - const elem = searchResults.querySelector("li"); - if (elem) addActive(elem); - } else if (active.nextElementSibling) { - removeActive(active); - addActive(active.nextElementSibling); - } + return { + selectors: sel, + activate: () => { + window.location.href = e.idAnchor; + return 'close'; + }, + onlySearch: !thisp && (`${e.idIdent}.html` !== e.idAnchor), + priority: e.idType ? -1 : 1, + + render(key: string, matched?: MatchedSpan) { + let title; + if (original === key) { + title = highlight(original, matched) + } else { + title = + {original} + + {highlight(key, matched)} + + + }; + + return [ +

    + {spanMaybe(title)} + {e.idAnchor.replace(/.html(#.+)?$/, "")} +

    , + ...desc + ]; + }, }; +}; - const movePrevious = () => { - const active = searchResults.querySelector("li.active"); - if (active && active.previousElementSibling) { - removeActive(active); - addActive(active.previousElementSibling); - } - }; - - searchInput.addEventListener("keydown", (e) => { - switch (e.key) { - case "Tab": - e.preventDefault(); - if (e.shiftKey) movePrevious(); else moveNext(); - break; - - case "Down": - case "ArrowDown": - e.preventDefault(); - moveNext(); - break; - - case "Up": - case "ArrowUp": - e.preventDefault(); - movePrevious(); - break; - - case "Enter": { - e.preventDefault(); - - const link: HTMLAnchorElement | null = - searchResults.querySelector("li.active > a") || searchResults.querySelector("li > a"); - if (link) link.click(); - break; - } - - case "Escape": { - e.preventDefault(); - closeSearch(); - break; +let path = window.location.pathname.split('/'); +let page = path[path.length - 1]; +if (page.length === 0) { page = "index.html"; } + +let thisp = 0, done = false; + +fetch("static/search.json") + .then(r => r.json()) + .then(entries => { + entries.filter((e: SearchItem) => !e.idIdent.startsWith(".")).forEach((e: SearchItem) => { + if (e.idAnchor.startsWith(page)) { + if (e.idAnchor !== page) { + InThisPage.pushPromptItems(makeSearch(e, true)); + } + } else { + Miscellanea.pushPromptItems(makeSearch(e, false)); } - } - }); - - document.body.appendChild(searchWrapper); - searchInput.focus(); - - // Fetch the search index if not available and start searching - if (!loadingIndex) { - loadingIndex = true; - fetch("static/search.json") - .then(r => r.json()) - .then(entries => { - index = new Searcher(entries, { - returnMatchData: true, - ignoreSymbols: false, - keySelector: (x: SearchItem) => [x.idIdent].concat(x.idDefines ?? []), - }); - - doSearch(); - }) - .catch(e => { - console.error("Failed to load search index", e); - loadingIndex = false; - setError("Failed to load search index"); - }); - } - - doSearch(); -} - -document.addEventListener("DOMContentLoaded", () => { - // Default pages have a "search" box which, when clicked, opens the main search box. - const searchInputProxy = document.getElementById("search-box-proxy") as HTMLInputElement | null; - if (searchInputProxy) { - searchInputProxy.addEventListener("focus", () => startSearch(searchInputProxy)); - } - - // Allow pressing Ctrl+K to search anywhere. - document.addEventListener("keydown", e => { - if (e.key == "k" && e.ctrlKey && !e.altKey) { - e.preventDefault(); - startSearch(searchInputProxy); - } + if (!done && (done = thisp++ > 32)) document.dispatchEvent(new Event("searchready")); + }); + }) + .catch(e => { + console.error("Failed to load search index", e); }); -}); diff --git a/support/web/js/sidebar.tsx b/support/web/js/sidebar.tsx new file mode 100644 index 000000000..34ec2fad7 --- /dev/null +++ b/support/web/js/sidebar.tsx @@ -0,0 +1,40 @@ +document.addEventListener('DOMContentLoaded', () => { + const headers = Array.from(document.querySelectorAll("article a.header-link")) + .map(x => x.parentElement) + .filter((x): x is HTMLHeadingElement => !!x); + + const headerLinks = Array.from(document.querySelectorAll("aside#toc a.header-link")); + + const findHeader = () => { + let closest = headers[0]; + + for (const header of headers) { + let top = header.getBoundingClientRect().top; + if (top >= 25) break; + closest = header; + }; + + for (const link of headerLinks) { + if (link.getAttribute("href") === `#${closest.getAttribute("id")}`) { + link.classList.add("current-heading"); + } else { + link.classList.remove("current-heading"); + } + } + }; + + let waiting = false; + + document.addEventListener("scroll", () => { + if (!waiting) { + window.requestAnimationFrame(() => { + findHeader(); + waiting = false; + }); + waiting = true; + } + }); + + setTimeout(() => { findHeader() }, 200); +}); +export { }; diff --git a/support/web/js/start.ts b/support/web/js/start.ts new file mode 100644 index 000000000..20753d8a5 --- /dev/null +++ b/support/web/js/start.ts @@ -0,0 +1,5 @@ +// Much smaller entrypoint file that only knows how to apply the users' +// settings from localStorage. This file compiles to ~1KiB of JS; it's +// totally fine to block on, unlike the ever-growing main.js. + +import "./lib/settings"; diff --git a/support/web/js/theme.tsx b/support/web/js/theme.tsx new file mode 100644 index 000000000..319e7bc6f --- /dev/null +++ b/support/web/js/theme.tsx @@ -0,0 +1,138 @@ +import { JSX, type Content } from "./lib/jsx"; +import { type Theme, themeSetting, equationSetting, Setting, hiddenCodeSetting, footnoteSetting, serifFontSetting } from "./lib/settings"; + +// This is pretty evil, but a loose