Hofmann-Streicher universes for graphs and globular types

references.bib

@@ -44,6 +44,17 @@ @article{AL19
   langid      = {english}
 }
 
+@misc{Awodey22,
+       author = {{Awodey}, Steve},
+        title = "{On Hofmann-Streicher universes}",
+     keywords = {Mathematics - Category Theory, Mathematics - Logic},
+         year = 2022,
+        month = may,
+archivePrefix = {arXiv},
+       eprint = {2205.10917},
+ primaryClass = {math.CT}
+}
+
 @online{BCDE21,
   title  = {Free groups in HoTT/UF in Agda},
   author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escardó, Martín},

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -155,6 +155,20 @@ tr-eq-pair-Σ :
 tr-eq-pair-Σ C refl refl u = refl
 ```
 
+### The action of `pr1` on identifcations of the form `eq-pair-Σ`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  ap-pr1-eq-pair-Σ :
+    {x x' : A} {y : B x} {y' : B x'}
+    (p : x ＝ x') (q : dependent-identification B p y y') →
+    ap pr1 (eq-pair-Σ p q) ＝ p
+  ap-pr1-eq-pair-Σ refl refl = refl
+```
+
 ## See also
 
 - Equality proofs in cartesian product types are characterized in

src/foundation-core/torsorial-type-families.lagda.md

@@ -99,5 +99,5 @@ module _
 
 ### See also
 
-- [Discrete relations](foundation.discrete-relations.md) are binary torsorial
-  type families.
+- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) are
+  binary torsorial type families.

src/foundation.lagda.md

@@ -20,6 +20,7 @@ open import foundation.action-on-equivalences-type-families public
 open import foundation.action-on-equivalences-type-families-over-subuniverses public
 open import foundation.action-on-higher-identifications-functions public
 open import foundation.action-on-homotopies-functions public
+open import foundation.action-on-identifications-binary-dependent-functions public
 open import foundation.action-on-identifications-binary-functions public
 open import foundation.action-on-identifications-dependent-functions public
 open import foundation.action-on-identifications-functions public
@@ -31,6 +32,7 @@ open import foundation.axiom-of-choice public
 open import foundation.bands public
 open import foundation.base-changes-span-diagrams public
 open import foundation.bicomposition-functions public
+open import foundation.binary-dependent-identifications public
 open import foundation.binary-embeddings public
 open import foundation.binary-equivalences public
 open import foundation.binary-equivalences-unordered-pairs-of-types public
@@ -130,7 +132,8 @@ open import foundation.diagonal-maps-of-types public
 open import foundation.diagonal-span-diagrams public
 open import foundation.diagonals-of-maps public
 open import foundation.diagonals-of-morphisms-arrows public
-open import foundation.discrete-relations public
+open import foundation.discrete-binary-relations public
+open import foundation.discrete-reflexive-relations public
 open import foundation.discrete-relaxed-sigma-decompositions public
 open import foundation.discrete-sigma-decompositions public
 open import foundation.discrete-types public
@@ -207,6 +210,8 @@ open import foundation.functoriality-truncation public
 open import foundation.fundamental-theorem-of-identity-types public
 open import foundation.global-choice public
 open import foundation.global-subuniverses public
+open import foundation.globular-type-of-dependent-functions public
+open import foundation.globular-type-of-functions public
 open import foundation.higher-homotopies-morphisms-arrows public
 open import foundation.hilberts-epsilon-operators public
 open import foundation.homotopies public

src/foundation/action-on-identifications-binary-dependent-functions.lagda.md

@@ -0,0 +1,53 @@
+# The binary action on identifications of binary dependent functions
+
+```agda
+module foundation.action-on-identifications-binary-dependent-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.binary-dependent-identifications
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+Given a binary dependent function `f : (x : A) (y : B) → C x y` and
+[identifications](foundation-core.identity-types.md) `p : x ＝ x'` in `A` and
+`q : y ＝ y'` in `B`, we obtain a
+[binary dependent identification](foundation.binary-dependent-identifications.md)
+
+```text
+  apd-binary f p q : binary-dependent-identification p q (f x y) (f x' y')
+```
+
+we call this the
+{{#concept "binary action on identifications of dependent binary functions" Agda=apd-binary}}.
+
+## Definitions
+
+### The binary action on identifications of binary dependent functions
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : A → B → UU l3}
+  (f : (x : A) (y : B) → C x y)
+  where
+
+  apd-binary :
+    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
+    binary-dependent-identification C p q (f x y) (f x' y')
+  apd-binary refl refl = refl
+```
+
+## See also
+
+- [Action of functions on identifications](foundation.action-on-identifications-functions.md)
+- [Action of functions on higher identifications](foundation.action-on-higher-identifications-functions.md).
+- [Action of dependent functions on identifications](foundation.action-on-identifications-dependent-functions.md).

src/foundation/action-on-identifications-binary-functions.lagda.md

@@ -198,6 +198,7 @@ module _
 
 ## See also
 
+- [Action of binary dependent functions on identifications](foundation.action-on-identifications-binary-dependent-functions.md)
 - [Action of functions on identifications](foundation.action-on-identifications-functions.md)
 - [Action of functions on higher identifications](foundation.action-on-higher-identifications-functions.md).
 - [Action of dependent functions on identifications](foundation.action-on-identifications-dependent-functions.md).

src/foundation/binary-dependent-identifications.lagda.md

@@ -0,0 +1,43 @@
+# Binary dependent identifications
+
+```agda
+module foundation.binary-dependent-identifications where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-transport
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a family of types `C x y` indexed by `x : A` and `y : B`, and consider
+[identifications](foundation-core.identity-types.md) `p : x ＝ x'` and
+`q : y ＝ y'` in `A` and `B`, respectively. A
+{{#concept "binary dependent identification" Agda=binary-dependent-identification}}
+from `c : C x y` to `c' : C x' y'` over `p` and `q` is a
+[dependent identification](foundation.dependent-identifications.md)
+
+```text
+  r : dependent-identification (C x') p (tr (λ t → C t y) p c) c'.
+```
+
+## Definitions
+
+### Binary dependent identifications
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (C : A → B → UU l3)
+  where
+
+  binary-dependent-identification :
+    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
+    C x y → C x' y' → UU l3
+  binary-dependent-identification p q c c' = binary-tr C p q c ＝ c'
+```

src/foundation/binary-relations.lagda.md

@@ -154,6 +154,9 @@ module _
 
   is-transitive : UU (l1 ⊔ l2)
   is-transitive = (x y z : A) → R y z → R x y → R x z
+
+  is-transitive' : UU (l1 ⊔ l2)
+  is-transitive' = {x y z : A} → R y z → R x y → R x z
 ```
 
 ### The predicate of being a transitive relation valued in propositions

src/foundation/binary-transport.lagda.md

@@ -37,7 +37,7 @@ module _
   where
 
   binary-tr : (p : x ＝ x') (q : y ＝ y') → C x y → C x' y'
-  binary-tr refl refl = id
+  binary-tr p q c = tr (C _) q (tr (λ u → C u _) p c)
 
   is-equiv-binary-tr : (p : x ＝ x') (q : y ＝ y') → is-equiv (binary-tr p q)
   is-equiv-binary-tr refl refl = is-equiv-id

src/foundation/dependent-function-types.lagda.md

@@ -79,3 +79,7 @@ module _
         ( span-type-family-Π B)
         ( universal-property-dependent-function-types-Π B)
 ```
+
+## See also
+
+- [The globular type of dependent functions](foundation.globular-type-of-dependent-functions.md)

src/foundation/dependent-identifications.lagda.md

@@ -298,3 +298,7 @@ module _
         ( inv-dependent-identification B p p'))
   distributive-inv-concat-dependent-identification refl refl refl refl = refl
 ```
+
+## See also
+
+- [Binary dependent identifications](foundation.binary-dependent-identifications.md)

src/foundation/discrete-binary-relations.lagda.md

@@ -0,0 +1,75 @@
+# Discrete binary relations
+
+```agda
+module foundation.discrete-binary-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.empty-types
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [binary relation](foundation.binary-relations.md) `R` on `A` is said to be
+{{#concept "discrete" Disambiguation="binary relation" Agda=is-discrete-Relation}}
+if it does not relate any elements, i.e., if the type `R x y` is empty for all
+`x y : A`. In other words, a binary relation is discrete if and only if it is
+the initial binary relation. This definition ensures that the inclusion of
+[discrete directed graphs](graph-theory.discrete-directed-graphs.md) is a left
+adjoint to the forgetful functor `(V , E) ↦ (V , ∅)`.
+
+The condition of discreteness of binary relations compares to the condition of
+[discreteness](foundation.discrete-reflexive-relations.md) of
+[reflexive relations](foundation.reflexive-relations.md) in the sense that both
+conditions imply initiality. Nevertheless, the condition of discreteness on
+reflexive relations asserts that the type family `R x` is
+[torsorial](foundation-core.torsorial-type-families.md) for every `x : A`, which
+looks quite differently.
+
+The condition of torsoriality is not adequate as a condition for discreteness
+for arbitrary binary relations. For example, the binary relation on
+[natural numbers](elementary-number-theory.natural-numbers.md) given by
+`R m n := (m + 1 ＝ n)`, relating natural numbers as follows
+
+```text
+  0 ---> 1 ---> 2 ---> ⋯,
+```
+
+satisfies the condition that the type family `R m` is torsorial for every
+`m : ℕ`, simply because the relation `R` is a
+[functional correspondence](foundation.functional-correspondences.md). Since
+this relation relates distinct elements, it is typically not considered to be
+discrete.
+
+## Definitions
+
+### The predicate on relations of being discrete
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-discrete-prop-Relation : Prop (l1 ⊔ l2)
+  is-discrete-prop-Relation =
+    Π-Prop A (λ x → Π-Prop A (λ y → is-empty-Prop (R x y)))
+
+  is-discrete-Relation : UU (l1 ⊔ l2)
+  is-discrete-Relation = type-Prop is-discrete-prop-Relation
+
+  is-prop-is-discrete-Relation : is-prop is-discrete-Relation
+  is-prop-is-discrete-Relation = is-prop-type-Prop is-discrete-prop-Relation
+```
+
+## See also
+
+- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md)
+- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md)
+- [Discrete-reflexive graphs](graph-theory.discrete-reflexive-graphs.md)

src/foundation/discrete-relations.lagda.md → src/foundation/discrete-reflexive-relations.lagda.md

@@ -1,7 +1,7 @@
-# Discrete relations
+# Discrete reflexive relations
 
 ```agda
-module foundation.discrete-relations where
+module foundation.discrete-reflexive-relations where
 ```
 
 <details><summary>Imports</summary>
@@ -22,41 +22,22 @@ open import foundation-core.propositions
 
 ## Idea
 
-A [relation](foundation.binary-relations.md) `R` on `A` is said to be
-{{#concept "discrete" Disambiguation="binary relations valued in types" Agda=is-discrete-Relation}}
+A [reflexive relation](foundation.binary-relations.md) `R` on `A` is said to be
+{{#concept "discrete" Disambiguation="reflexive relations valued in types" Agda=is-discrete-Reflexive-Relation}}
 if, for every element `x : A`, the type family `R x` is
 [torsorial](foundation-core.torsorial-type-families.md). In other words, the
 [dependent sum](foundation.dependent-pair-types.md) `Σ (y : A), (R x y)` is
-[contractible](foundation-core.contractible-types.md) for every `x`. The
-{{#concept "standard discrete relation" Disambiguation="binary relations valued in types"}}
-on a type `X` is the relation defined by
-[identifications](foundation-core.identity-types.md),
+[contractible](foundation-core.contractible-types.md) for every `x`.
+
+The {{#concept "standard discrete reflexive relation"}} on a type `X` is the
+relation defined by [identifications](foundation-core.identity-types.md),
 
 ```text
   R x y := (x ＝ y).
 ```
 
 ## Definitions
 
-### The predicate on relations of being discrete
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
-  where
-
-  is-discrete-prop-Relation : Prop (l1 ⊔ l2)
-  is-discrete-prop-Relation = Π-Prop A (λ x → is-torsorial-Prop (R x))
-
-  is-discrete-Relation : UU (l1 ⊔ l2)
-  is-discrete-Relation =
-    type-Prop is-discrete-prop-Relation
-
-  is-prop-is-discrete-Relation : is-prop is-discrete-Relation
-  is-prop-is-discrete-Relation =
-    is-prop-type-Prop is-discrete-prop-Relation
-```
-
 ### The predicate on reflexive relations of being discrete
 
 ```agda
@@ -66,7 +47,7 @@ module _
 
   is-discrete-prop-Reflexive-Relation : Prop (l1 ⊔ l2)
   is-discrete-prop-Reflexive-Relation =
-    is-discrete-prop-Relation (rel-Reflexive-Relation R)
+    Π-Prop A (λ a → is-torsorial-Prop (rel-Reflexive-Relation R a))
 
   is-discrete-Reflexive-Relation : UU (l1 ⊔ l2)
   is-discrete-Reflexive-Relation =
@@ -78,13 +59,22 @@ module _
     is-prop-type-Prop is-discrete-prop-Reflexive-Relation
 ```
 
-### The standard discrete relation on a type
+## Properties
+
+### The identity relation is discrete
 
 ```agda
 module _
   {l : Level} (A : UU l)
   where
 
-  is-discrete-Id-Relation : is-discrete-Relation (Id {A = A})
-  is-discrete-Id-Relation = is-torsorial-Id
+  is-discrete-Id-Reflexive-Relation :
+    is-discrete-Reflexive-Relation (Id-Reflexive-Relation A)
+  is-discrete-Id-Reflexive-Relation = is-torsorial-Id
 ```
+
+## See also
+
+- [Discrete binary relations](foundation.discrete-binary-relations.md)
+- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md)
+- [Discrete reflexive graphs](graph-theory.discrete-reflexive-graphs.md)