Hofmann-Streicher universes for graphs and globular types

references.bib

@@ -16,6 +16,23 @@ @article{AKS15
   langid      = {english}
 }
 
+@ARTICLE{Awodey22,
+       author = {{Awodey}, Steve},
+        title = "{On Hofmann-Streicher universes}",
+      journal = {arXiv e-prints},
+     keywords = {Mathematics - Category Theory, Mathematics - Logic},
+         year = 2022,
+        month = may,
+          eid = {arXiv:2205.10917},
+        pages = {arXiv:2205.10917},
+          doi = {10.48550/arXiv.2205.10917},
+archivePrefix = {arXiv},
+       eprint = {2205.10917},
+ primaryClass = {math.CT},
+       adsurl = {https://ui.adsabs.harvard.edu/abs/2022arXiv220510917A},
+      adsnote = {Provided by the SAO/NASA Astrophysics Data System}
+}
+
 @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/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/wild-category-of-types.lagda.md

@@ -46,78 +46,147 @@ consists of types and functions and homotopies.
 
 ## Definitions
 
-### The globular structure on dependent function types
+### The globular type of dependent function types
 
 ```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)
+
 globular-structure-Π :
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
   globular-structure (l1 ⊔ l2) ((x : A) → B x)
-globular-structure-Π =
-  λ where
-  .1-cell-globular-structure → _~_
-  .globular-structure-1-cell-globular-structure f g → globular-structure-Π
+globular-structure-Π {A = A} {B = B} =
+  globular-structure-0-cell-Globular-Type
+    ( dependent-function-type-Globular-Type A B)
 
-is-reflexive-globular-structure-Π :
+is-reflexive-dependent-function-type-Globular-Type :
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
-  is-reflexive-globular-structure (globular-structure-Π {A = A} {B})
-is-reflexive-globular-structure-Π =
-  λ where
-  .is-reflexive-1-cell-is-reflexive-globular-structure f → refl-htpy
-  .is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure f g →
-    is-reflexive-globular-structure-Π
-
-is-transitive-globular-structure-Π :
+  is-reflexive-Globular-Type (dependent-function-type-Globular-Type A B)
+is-reflexive-1-cell-is-reflexive-globular-structure
+  is-reflexive-dependent-function-type-Globular-Type f = refl-htpy
+is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure
+  is-reflexive-dependent-function-type-Globular-Type f g =
+  is-reflexive-dependent-function-type-Globular-Type
+
+is-transitive-dependent-function-type-Globular-Type :
   {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
-  is-transitive-globular-structure (globular-structure-Π {A = A} {B})
-is-transitive-globular-structure-Π =
-  λ where
-  .comp-1-cell-is-transitive-globular-structure H K → K ∙h H
-  .is-transitive-globular-structure-1-cell-is-transitive-globular-structure
-    H K →
-    is-transitive-globular-structure-Π
+  is-transitive-Globular-Type (dependent-function-type-Globular-Type A B)
+comp-1-cell-is-transitive-globular-structure
+  is-transitive-dependent-function-type-Globular-Type K H =
+  H ∙h K
+is-transitive-globular-structure-1-cell-is-transitive-globular-structure
+  is-transitive-dependent-function-type-Globular-Type f g =
+  is-transitive-dependent-function-type-Globular-Type
 ```
 
-### The large globular structure on types
+### The globular type of function types
 
 ```agda
-large-globular-structure-Type : large-globular-structure (_⊔_) (λ l → UU l)
-large-globular-structure-Type =
-  λ where
-  .1-cell-large-globular-structure X Y → (X → Y)
-  .globular-structure-1-cell-large-globular-structure X Y → globular-structure-Π
-
-is-reflexive-large-globular-structure-Type :
-  is-reflexive-large-globular-structure large-globular-structure-Type
-is-reflexive-large-globular-structure-Type =
-  λ where
-  .is-reflexive-1-cell-is-reflexive-large-globular-structure X → id
-  .is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure
-    X Y →
-    is-reflexive-globular-structure-Π
-
-is-transitive-large-globular-structure-Type :
-  is-transitive-large-globular-structure large-globular-structure-Type
-is-transitive-large-globular-structure-Type =
-  λ where
-  .comp-1-cell-is-transitive-large-globular-structure g f → g ∘ f
-  .is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure
-    X Y →
-    is-transitive-globular-structure-Π
+function-type-Globular-Type :
+  {l1 l2 : Level} (A : UU l1) (B : UU l2) →
+  Globular-Type (l1 ⊔ l2) (l1 ⊔ l2)
+function-type-Globular-Type A B = dependent-function-type-Globular-Type A (λ _ → B)
+
+globular-structure-function-type :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} → globular-structure (l1 ⊔ l2) (A → B)
+globular-structure-function-type = globular-structure-Π
+
+is-reflexive-function-type-Globular-Type :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  is-reflexive-Globular-Type (function-type-Globular-Type A B)
+is-reflexive-function-type-Globular-Type {l1} {l2} {A} {B} =
+  is-reflexive-dependent-function-type-Globular-Type
+
+is-transitive-function-type-Globular-Type :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  is-transitive-Globular-Type (function-type-Globular-Type A B)
+is-transitive-function-type-Globular-Type =
+  is-transitive-dependent-function-type-Globular-Type
 ```
 
-### The noncoherent large wild higher precategory of types
+### The large globular type of types
 
 ```agda
-Type-Noncoherent-Large-Wild-Higher-Precategory :
-  Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_)
-Type-Noncoherent-Large-Wild-Higher-Precategory =
-  λ where
-  .obj-Noncoherent-Large-Wild-Higher-Precategory l →
-    UU l
-  .hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
-    large-globular-structure-Type
-  .id-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
-    is-reflexive-large-globular-structure-Type
-  .comp-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
-    is-transitive-large-globular-structure-Type
+Type-Large-Globular-Type : Large-Globular-Type lsuc (_⊔_)
+0-cell-Large-Globular-Type Type-Large-Globular-Type l =
+  UU l
+1-cell-globular-type-Large-Globular-Type Type-Large-Globular-Type A B =
+  function-type-Globular-Type A B
+
+is-reflexive-Type-Large-Globular-Type :
+  is-reflexive-Large-Globular-Type Type-Large-Globular-Type
+refl-0-cell-is-reflexive-Large-Globular-Type
+  is-reflexive-Type-Large-Globular-Type X =
+  id
+is-reflexive-1-cell-globular-type-is-reflexive-Large-Globular-Type
+  is-reflexive-Type-Large-Globular-Type =
+  is-reflexive-function-type-Globular-Type
+
+Type-Large-Reflexive-Globular-Type : Large-Reflexive-Globular-Type lsuc (_⊔_)
+Type-Large-Reflexive-Globular-Type = ?
 ```
+
+-- ```agda
+-- large-globular-structure-Type : large-globular-structure (_⊔_) (λ l → UU l)
+-- large-globular-structure-Type =
+--   λ where
+--   .1-cell-large-globular-structure X Y → (X → Y)
+--   .globular-structure-1-cell-large-globular-structure X Y → globular-structure-Π
+
+-- is-reflexive-large-globular-structure-Type :
+--   is-reflexive-large-globular-structure large-globular-structure-Type
+-- is-reflexive-large-globular-structure-Type =
+--   λ where
+--   .is-reflexive-1-cell-is-reflexive-large-globular-structure X → id
+--   .is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure
+--     X Y →
+--     is-reflexive-globular-structure-Π
+
+-- is-transitive-large-globular-structure-Type :
+--   is-transitive-large-globular-structure large-globular-structure-Type
+-- is-transitive-large-globular-structure-Type =
+--   λ where
+--   .comp-1-cell-is-transitive-large-globular-structure g f → g ∘ f
+--   .is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure
+--     X Y →
+--     is-transitive-globular-structure-Π
+-- ```
+
+-- ### The noncoherent large wild higher precategory of types
+
+-- ```agda
+-- Type-Large-Globular-Type :
+--   Large-Globular-Type lsuc (_⊔_)
+-- 0-cell-Large-Globular-Type Type-Large-Globular-Type l1 = UU l1
+-- 1-cell-globular-type-Large-Globular-Type Type-Large-Globular-Type X Y =
+--   {!!}
+
+-- Type-Noncoherent-Large-Wild-Higher-Precategory :
+--   Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_)
+-- large-globular-type-Noncoherent-Large-Wild-Precategory
+--   Type-Noncoherent-Large-Wild-Higher-Precategory =
+--   {!Type-Large-Globular-Type!}
+-- id-structure-Noncoherent-Large-Wild-Higher-Precategory
+--   Type-Noncoherent-Large-Wild-Higher-Precategory =
+--   {!!}
+-- comp-structure-Noncoherent-Large-Wild-Higher-Precategory
+--   Type-Noncoherent-Large-Wild-Higher-Precategory =
+--   {!!}
+
+
+-- --   λ where
+-- --   .obj-Noncoherent-Large-Wild-Higher-Precategory l →
+-- --     UU l
+-- --   .hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+-- --     large-globular-structure-Type
+-- --   .id-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+-- --     is-reflexive-large-globular-structure-Type
+-- --   .comp-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+-- --     is-transitive-large-globular-structure-Type
+-- -- ```

src/graph-theory.lagda.md

@@ -6,13 +6,16 @@
 module graph-theory where
 
 open import graph-theory.acyclic-undirected-graphs public
+open import graph-theory.cartesian-products-directed-graphs public
 open import graph-theory.circuits-undirected-graphs public
 open import graph-theory.closed-walks-undirected-graphs public
 open import graph-theory.complete-bipartite-graphs public
 open import graph-theory.complete-multipartite-graphs public
 open import graph-theory.complete-undirected-graphs public
 open import graph-theory.connected-undirected-graphs public
 open import graph-theory.cycles-undirected-graphs public
+open import graph-theory.dependent-directed-graphs public
+open import graph-theory.dependent-products-directed-graphs public
 open import graph-theory.directed-graph-structures-on-standard-finite-sets public
 open import graph-theory.directed-graphs public
 open import graph-theory.discrete-graphs public
@@ -25,6 +28,7 @@ open import graph-theory.equivalences-directed-graphs public
 open import graph-theory.equivalences-enriched-undirected-graphs public
 open import graph-theory.equivalences-undirected-graphs public
 open import graph-theory.eulerian-circuits-undirected-graphs public
+open import graph-theory.exponents-directed-graphs public
 open import graph-theory.faithful-morphisms-undirected-graphs public
 open import graph-theory.fibers-directed-graphs public
 open import graph-theory.finite-graphs public
@@ -41,17 +45,22 @@ open import graph-theory.neighbors-undirected-graphs public
 open import graph-theory.orientations-undirected-graphs public
 open import graph-theory.paths-undirected-graphs public
 open import graph-theory.polygons public
+open import graph-theory.pullbacks-dependent-directed-graphs public
 open import graph-theory.raising-universe-levels-directed-graphs public
 open import graph-theory.reflecting-maps-undirected-graphs public
 open import graph-theory.reflexive-graphs public
 open import graph-theory.regular-undirected-graphs public
+open import graph-theory.sections-dependent-directed-graphs public
 open import graph-theory.simple-undirected-graphs public
 open import graph-theory.stereoisomerism-enriched-undirected-graphs public
+open import graph-theory.terminal-directed-graphs public
 open import graph-theory.totally-faithful-morphisms-undirected-graphs public
 open import graph-theory.trails-directed-graphs public
 open import graph-theory.trails-undirected-graphs public
 open import graph-theory.undirected-graph-structures-on-standard-finite-sets public
 open import graph-theory.undirected-graphs public
+open import graph-theory.universal-directed-graph public
+open import graph-theory.universal-reflexive-graph public
 open import graph-theory.vertex-covers public
 open import graph-theory.voltage-graphs public
 open import graph-theory.walks-directed-graphs public

src/graph-theory/cartesian-products-directed-graphs.lagda.md

@@ -0,0 +1,104 @@
+# Cartesian products of directed graphs
+
+```agda
+module graph-theory.cartesian-products-directed-graphs where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import graph-theory.directed-graphs
+open import graph-theory.morphisms-directed-graphs
+```
+
+</details>
+
+## Idea
+
+Consider two [directed graphs](graph-theory.directed-graphs.md) `A := (A₀ , A₁)`
+and `B := (B₀ , B₁)`. The cartesian product of `A` and `B` is the directed graph
+`A × B` given by
+
+```text
+  (A × B)₀ := A₀ × B₀
+  (A × B)₁ (x , y) (x' , y') := A₁ x x' × B₁ y y'.
+```
+
+## Definitions
+
+### The cartesian product of directed graphs
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (A : Directed-Graph l1 l2) (B : Directed-Graph l3 l4)
+  where
+
+  vertex-product-Directed-Graph : UU (l1 ⊔ l3)
+  vertex-product-Directed-Graph =
+    vertex-Directed-Graph A × vertex-Directed-Graph B
+
+  edge-product-Directed-Graph :
+    (x y : vertex-product-Directed-Graph) → UU (l2 ⊔ l4)
+  edge-product-Directed-Graph (x , y) (x' , y') =
+    edge-Directed-Graph A x x' × edge-Directed-Graph B y y'
+
+  product-Directed-Graph : Directed-Graph (l1 ⊔ l3) (l2 ⊔ l4)
+  pr1 product-Directed-Graph = vertex-product-Directed-Graph
+  pr2 product-Directed-Graph = edge-product-Directed-Graph
+```
+
+### The projections out of cartesian products of directed graphs
+
+#### The first projection out of the cartesian product of directed graphs
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (A : Directed-Graph l1 l2) (B : Directed-Graph l3 l4)
+  where
+
+  vertex-pr1-product-Directed-Graph :
+    vertex-product-Directed-Graph A B → vertex-Directed-Graph A
+  vertex-pr1-product-Directed-Graph = pr1
+
+  edge-pr1-product-Directed-Graph :
+    {x y : vertex-product-Directed-Graph A B} →
+    edge-product-Directed-Graph A B x y →
+    edge-Directed-Graph A
+      ( vertex-pr1-product-Directed-Graph x)
+      ( vertex-pr1-product-Directed-Graph y)
+  edge-pr1-product-Directed-Graph = pr1
+
+  pr1-product-Directed-Graph :
+    hom-Directed-Graph (product-Directed-Graph A B) A
+  pr1 pr1-product-Directed-Graph = vertex-pr1-product-Directed-Graph
+  pr2 pr1-product-Directed-Graph _ _ = edge-pr1-product-Directed-Graph
+```
+
+#### The second projection out of the cartesian product of two directed graphs
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (A : Directed-Graph l1 l2) (B : Directed-Graph l3 l4)
+  where
+
+  vertex-pr2-product-Directed-Graph :
+    vertex-product-Directed-Graph A B → vertex-Directed-Graph B
+  vertex-pr2-product-Directed-Graph = pr2
+
+  edge-pr2-product-Directed-Graph :
+    {x y : vertex-product-Directed-Graph A B} →
+    edge-product-Directed-Graph A B x y →
+    edge-Directed-Graph B
+      ( vertex-pr2-product-Directed-Graph x)
+      ( vertex-pr2-product-Directed-Graph y)
+  edge-pr2-product-Directed-Graph = pr2
+
+  pr2-product-Directed-Graph :
+    hom-Directed-Graph (product-Directed-Graph A B) B
+  pr1 pr2-product-Directed-Graph = vertex-pr2-product-Directed-Graph
+  pr2 pr2-product-Directed-Graph _ _ = edge-pr2-product-Directed-Graph
+```