chore: Concepts in structured-types (#1658)

Author: fredrik-bakke

src/structured-types/cartesian-products-types-equipped-with-endomorphisms.lagda.md

@@ -19,8 +19,10 @@ open import structured-types.types-equipped-with-endomorphisms
 
 ## Idea
 
-The **cartesian product** of two
-[types equipped with an endomorphism](structured-types.types-equipped-with-endomorphisms.md)
+The
+{{#concept "cartesian product" Disambiguation="of two types equipped with endomorphisms" Agda=product-Type-With-Endomorphism}}
+of two
+[types equipped with endomorphisms](structured-types.types-equipped-with-endomorphisms.md)
 `(A , f)` and `(B , g)` is defined as `(A × B , f × g)`
 
 ## Definitions

src/structured-types/central-h-spaces.lagda.md

@@ -24,9 +24,9 @@ as the type of [pointed sections](structured-types.pointed-types.md) of the
 pointed evaluation map `(A → A) →∗ A`. If the type `A` is
 [connected](foundation.connected-types.md), then the section maps to the
 [connected component](foundation.connected-components.md) of `(A ≃ A)` at the
-identity [equivalence](foundation-core.equivalences.md). An **evaluative
-H-space** is a pointed type such that the map `ev_pt : (A ≃ A)_{(id)} → A` is an
-equivalence.
+identity [equivalence](foundation-core.equivalences.md). An
+{{#concept "evaluative H-space" Agda=is-central-h-space}} is a pointed type such
+that the map `ev_pt : (A ≃ A)_{(id)} → A` is an equivalence.
 
 ## Definition
 

src/structured-types/conjugation-pointed-types.lagda.md

@@ -27,12 +27,12 @@ open import synthetic-homotopy-theory.loop-spaces
 
 ## Idea
 
-Conjugation on a [pointed type](structured-types.pointed-types.md) `(B,b)` is
-defined as a family of [pointed maps](structured-types.pointed-maps.md)
-`conj u p : (B,b) →∗ (B,u)` indexed by `u : B` and `p : b ＝ u`, such that
-`conj b ω` acts on the [loop space](synthetic-homotopy-theory.loop-spaces.md)
-`Ω (B , b)` by conjugation, i.e., it maps a loop `α : b ＝ b` to the loop
-`ω⁻¹αω`.
+{{#concept "Conjugation" Agda=conjugation-Pointed-Type}} on a
+[pointed type](structured-types.pointed-types.md) `(B,b)` is defined as a family
+of [pointed maps](structured-types.pointed-maps.md) `conj u p : (B,b) →∗ (B,u)`
+indexed by `u : B` and `p : b ＝ u`, such that `conj b ω` acts on the
+[loop space](synthetic-homotopy-theory.loop-spaces.md) `Ω (B , b)` by
+conjugation, i.e., it maps a loop `α : b ＝ b` to the loop `ω⁻¹αω`.
 
 ## Definition
 

src/structured-types/constant-pointed-maps.lagda.md

@@ -20,7 +20,7 @@ open import structured-types.pointed-types
 
 ## Idea
 
-Given two [pointed types](structured-types.pointed-types.md) `A` and `B` the
+Given two [pointed types](structured-types.pointed-types.md) `A` and `B`, the
 {{#concept "constant pointed map" Agda=constant-pointed-map}} from `A` to `B` is
 the [pointed map](structured-types.pointed-maps.md)
 `constant-pointed-map : A →∗ B` mapping every element in `A` to the base point

src/structured-types/contractible-pointed-types.lagda.md

@@ -16,6 +16,12 @@ open import structured-types.pointed-types
 
 </details>
 
+## Idea
+
+A {{#concept "contractible pointed type" Agda=is-contr-Pointed-Type}} is a
+[pointed type](structured-types.pointed-types.md) that is
+[contractible](foundation-core.contractible-types.md).
+
 ## Definition
 
 ```agda

src/structured-types/cyclic-types.lagda.md

@@ -23,7 +23,8 @@ open import structured-types.sets-equipped-with-automorphisms
 
 ## Idea
 
-A **cyclic set** consists of a [set](foundation.sets.md) `A` equipped with an
+A {{#concept "cyclic set" Agda=Cyclic-Set}} consists of a
+[set](foundation.sets.md) `A` [equipped](foundation.structure.md) with an
 [automorphism](foundation.automorphisms.md) `e : A ≃ A` which is _cyclic_ in the
 sense that its underlying set is [inhabited](foundation.inhabited-types.md) and
 the map

src/structured-types/dependent-products-h-spaces.lagda.md

@@ -24,9 +24,11 @@ open import structured-types.pointed-types
 ## Idea
 
 Given a family of [H-spaces](structured-types.h-spaces.md) `Mᵢ` indexed by
-`i : I`, the dependent product `Π(i : I), Mᵢ` is a H-space consisting of
-dependent functions taking `i : I` to an element of the underlying type of `Mᵢ`.
-The multiplicative operation and the unit are given pointwise.
+`i : I`, the
+{{#concept "dependent product" Disambiguation="H-space" Agda=Π-H-Space}}
+`Π(i : I), Mᵢ` is an H-space consisting of dependent functions taking `i : I` to
+an element of the underlying type of `Mᵢ`. The multiplicative operation and the
+unit are given pointwise.
 
 ## Definition
 

src/structured-types/dependent-products-pointed-types.lagda.md

@@ -18,9 +18,11 @@ open import structured-types.pointed-types
 ## Idea
 
 Given a family of [pointed types](structured-types.pointed-types.md) `Mᵢ`
-indexed by `i : I`, the dependent product `Π(i : I), Mᵢ` is a pointed type
-consisting of dependent functions taking `i : I` to an element of the underlying
-type of `Mᵢ`. The base point is given pointwise.
+indexed by `i : I`, the
+{{#concept "dependent product" Disambiguation="pointed type" Agda=Π-Pointed-Type}}
+`Π(i : I), Mᵢ` is a pointed type consisting of dependent functions taking
+`i : I` to an element of the underlying type of `Mᵢ`. The base point is given
+pointwise.
 
 ## Definition
 

src/structured-types/dependent-products-wild-monoids.lagda.md

@@ -26,9 +26,11 @@ open import structured-types.wild-monoids
 ## Idea
 
 Given a family of [wild monoids](structured-types.wild-monoids.md) `Mᵢ` indexed
-by `i : I`, the dependent product `Π(i : I), Mᵢ` is a wild monoid consisting of
-dependent functions taking `i : I` to an element of the underlying type of `Mᵢ`.
-Every component of the structure is given pointwise.
+by `i : I`, the
+{{#concept "dependent product" Disambiguation="wild monoid" Agda=Π-Wild-Monoid}}
+`Π(i : I), Mᵢ` is a wild monoid consisting of dependent functions taking `i : I`
+to an element of the underlying type of `Mᵢ`. Every component of the structure
+is given pointwise.
 
 ## Definition
 

src/structured-types/dependent-types-equipped-with-automorphisms.lagda.md

@@ -30,8 +30,9 @@ open import structured-types.types-equipped-with-automorphisms
 
 Consider a
 [type equipped with an automorphism](structured-types.types-equipped-with-automorphisms.md)
-`(X,e)`. A **dependent type equipped with an automorphism** over `(X,e)`
-consists of a dependent type `Y` over `X` and for each `x : X` an
+`(X, e)`. A
+{{#concept "dependent type equipped with an automorphism" Agda=Dependent-Type-With-Automorphism}}
+over `(X, e)` consists of a dependent type `Y` over `X` and for each `x : X` an
 [equivalence](foundation-core.equivalences.md) `Y x ≃ Y (e x)`.
 
 ## Definitions