Hofmann-Streicher universes for graphs and globular types (#1196)

This pull request is part of the formalization of higher category theory
project with Ivan. Here we construct Hofmann-Streicher universes for:
- directed graphs
- reflexive directed graphs
- globular types
- reflexive globular types

Additionally, we add some computations for dependent Pi-types in those
toposes, and some infrastructure is streamlined.

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.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
@@ -208,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/globular-type-of-dependent-functions.lagda.md

@@ -0,0 +1,109 @@
+# The globular type of dependent functions
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module foundation.globular-type-of-dependent-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.homotopies
+
+open import globular-types.globular-types
+open import globular-types.reflexive-globular-types
+open import globular-types.transitive-globular-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "globular type of dependent functions" Agda=dependent-function-type-Globular-Type}}
+is the [globular type](globular-types.globular-types.md) consisting of
+[dependent functions](foundation.dependent-function-types.md) and
+[homotopies](foundation-core.homotopies.md) between them. Since homotopies are
+themselves defined to be certain dependent functions, they directly provide a
+globular structure on dependent function types.
+
+The globular type of dependent functions of a type family `B` over `A` is
+[reflexive](globular-types.reflexive-globular-types.md) and
+[transitive](globular-types.transitive-globular-types.md), so it is a
+[noncoherent wild higher precategory](wild-category-theory.noncoherent-wild-higher-precategories.md).
+
+The structures defined in this file are used to define the
+[noncoherent large wild higher precategory of types](foundation.wild-category-of-types.md).
+
+## Definitions
+
+### The globular type of dependent functions
+
+```agda
+dependent-function-type-Globular-Type :
+  {l1 l2 : Level} (A : UU l1) (B : A → UU l2) →
+  Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
+0-cell-Globular-Type (dependent-function-type-Globular-Type A B) =
+  (x : A) → B x
+1-cell-globular-type-Globular-Type
+  ( dependent-function-type-Globular-Type A B) f g =
+  dependent-function-type-Globular-Type A (eq-value f g)
+```
+
+## Properties
+
+### The globular type of dependent functions is reflexive
+
+```agda
+is-reflexive-dependent-function-type-Globular-Type :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-reflexive-Globular-Type (dependent-function-type-Globular-Type A B)
+is-reflexive-1-cell-is-reflexive-Globular-Type
+  is-reflexive-dependent-function-type-Globular-Type f =
+  refl-htpy
+is-reflexive-1-cell-globular-type-is-reflexive-Globular-Type
+  is-reflexive-dependent-function-type-Globular-Type =
+  is-reflexive-dependent-function-type-Globular-Type
+
+dependent-function-type-Reflexive-Globular-Type :
+  {l1 l2 : Level} (A : UU l1) (B : A → UU l2) →
+  Reflexive-Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
+globular-type-Reflexive-Globular-Type
+  ( dependent-function-type-Reflexive-Globular-Type A B) =
+  dependent-function-type-Globular-Type A B
+refl-Reflexive-Globular-Type
+  ( dependent-function-type-Reflexive-Globular-Type A B) =
+  is-reflexive-dependent-function-type-Globular-Type
+```
+
+### The globular type of dependent functions is transitive
+
+```agda
+is-transitive-dependent-function-type-Globular-Type :
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
+  is-transitive-Globular-Type (dependent-function-type-Globular-Type A B)
+comp-1-cell-is-transitive-Globular-Type
+  is-transitive-dependent-function-type-Globular-Type K H =
+  H ∙h K
+is-transitive-1-cell-globular-type-is-transitive-Globular-Type
+  is-transitive-dependent-function-type-Globular-Type =
+  is-transitive-dependent-function-type-Globular-Type
+
+dependent-function-type-Transitive-Globular-Type :
+  {l1 l2 : Level} (A : UU l1) (B : A → UU l2) →
+  Transitive-Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
+globular-type-Transitive-Globular-Type
+  ( dependent-function-type-Transitive-Globular-Type A B) =
+  dependent-function-type-Globular-Type A B
+is-transitive-Transitive-Globular-Type
+  ( dependent-function-type-Transitive-Globular-Type A B) =
+  is-transitive-dependent-function-type-Globular-Type
+```
+
+## See also
+
+- [The globular type of functions](foundation.globular-type-of-functions.md)
+- [The wild category of types](foundation.wild-category-of-types.md)