From ec6eec821d66721c656da6f4b0510442f47b7fee Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Tue, 5 Nov 2024 14:28:37 -0500 Subject: [PATCH] some review comments --- .../fibers-directed-graphs.lagda.md | 2 +- .../universal-directed-graph.lagda.md | 2 +- .../binary-globular-maps.lagda.md | 25 +------------------ src/structured-types/globular-maps.lagda.md | 14 ++++++----- ...large-lax-reflexive-globular-maps.lagda.md | 2 +- ...arge-lax-transitive-globular-maps.lagda.md | 2 +- .../lax-transitive-globular-maps.lagda.md | 2 +- 7 files changed, 14 insertions(+), 35 deletions(-) diff --git a/src/graph-theory/fibers-directed-graphs.lagda.md b/src/graph-theory/fibers-directed-graphs.lagda.md index 690c5ab2eb..ed82be7273 100644 --- a/src/graph-theory/fibers-directed-graphs.lagda.md +++ b/src/graph-theory/fibers-directed-graphs.lagda.md @@ -39,7 +39,7 @@ nodes consists of vertices `y` equipped with a of edges from `(y , w)` to `(z , v)` consist of an edge `e : y → z` such that `w ＝ cons e v`. -**Note:** The fiber of a directed graphs should not be confused with the +**Note:** The fiber of a directed graph should not be confused with the [fiber of a morphism of directed graphs](graph-theory.fibers-morphisms-directed-graphs.md), which is the [dependent directed graph](graph-theory.dependent-directed-graphs.md) consisting diff --git a/src/graph-theory/universal-directed-graph.lagda.md b/src/graph-theory/universal-directed-graph.lagda.md index 6b09622b11..e212b2a121 100644 --- a/src/graph-theory/universal-directed-graph.lagda.md +++ b/src/graph-theory/universal-directed-graph.lagda.md @@ -46,7 +46,7 @@ The Hofmann–Streicher universe of presheaves on a category `𝒞` is the presh where `*` is the terminal object of `𝒞/I`, i.e., the identity morphism on `I`. -We compute a the instances of the slice category `⇉/I`: +We compute the instances of the slice category `⇉/I`: - The slice category `⇉/0` is the terminal category. - The slice category `⇉/1` is the representing cospan diff --git a/src/structured-types/binary-globular-maps.lagda.md b/src/structured-types/binary-globular-maps.lagda.md index fb6e8702ea..6c7e436885 100644 --- a/src/structured-types/binary-globular-maps.lagda.md +++ b/src/structured-types/binary-globular-maps.lagda.md @@ -11,6 +11,7 @@ module structured-types.binary-globular-maps where ```agda open import foundation.universe-levels +open import structured-types.globular-maps open import structured-types.globular-types ``` @@ -60,27 +61,3 @@ record ( 0-cell-binary-globular-map x y) ( 0-cell-binary-globular-map x' y')) ``` - -### Commuting squares of binary globular maps - -Consider three [globular maps](structured-types.globular-maps.md) `g : G → G'`, -`h : H → H'`, and `k : K → K'`, and consider two binary globular maps - -```text - μ : G → H → K - μ' : G' → H' → K'. -``` - -A {{#concept "commuting square of binary globular maps"}} - -```text - μ - G H ----> K - | | | - g | | h | k - ∨ ∨ ∨ - G' H' ----> K' - μ' -``` - -consists of a diff --git a/src/structured-types/globular-maps.lagda.md b/src/structured-types/globular-maps.lagda.md index f77bf9d42a..d1141ce730 100644 --- a/src/structured-types/globular-maps.lagda.md +++ b/src/structured-types/globular-maps.lagda.md @@ -104,7 +104,6 @@ module _ (F : globular-map A B) where -{- 3-cell-globular-map-globular-map : {x y : 0-cell-Globular-Type A} {f g : 1-cell-Globular-Type A x y} @@ -114,11 +113,10 @@ module _ ( 3-cell-globular-type-Globular-Type B ( 2-cell-globular-map F s) ( 2-cell-globular-map F t)) - 3-cell-globular-map-globular-map s t = + 3-cell-globular-map-globular-map = 2-cell-globular-map-globular-map ( 1-cell-globular-map-globular-map F) --} - + 3-cell-globular-map : {x y : 0-cell-Globular-Type A} {f g : 1-cell-Globular-Type A x y} → @@ -136,11 +134,15 @@ module _ ```agda id-globular-map : {l1 l2 : Level} (A : Globular-Type l1 l2) → globular-map A A -id-globular-map A = +0-cell-globular-map (id-globular-map A) = id +1-cell-globular-map-globular-map (id-globular-map A) = + id-globular-map (1-cell-globular-type-Globular-Type A _ _) + +{- λ where .0-cell-globular-map → id .1-cell-globular-map-globular-map {x} {y} → - id-globular-map (1-cell-globular-type-Globular-Type A x y) + id-globular-map (1-cell-globular-type-Globular-Type A x y) -} ``` ### Composition of maps of globular types diff --git a/src/structured-types/large-lax-reflexive-globular-maps.lagda.md b/src/structured-types/large-lax-reflexive-globular-maps.lagda.md index 7ab4b658b9..0ad31e0840 100644 --- a/src/structured-types/large-lax-reflexive-globular-maps.lagda.md +++ b/src/structured-types/large-lax-reflexive-globular-maps.lagda.md @@ -30,7 +30,7 @@ between two `f : G → H` equipped with a family of 2-cells ```text - (x : G₀) → H₂ (f₁ (Gᵣ x)) (Hᵣ (f₀ x)) + (x : G₀) → H₂ (Hᵣ (f₀ x)) (f₁ (Gᵣ x)) ``` from the image of the reflexivity cell at `x` in `G` to the reflexivity cell at diff --git a/src/structured-types/large-lax-transitive-globular-maps.lagda.md b/src/structured-types/large-lax-transitive-globular-maps.lagda.md index 103002d0d7..bdbbc7308c 100644 --- a/src/structured-types/large-lax-transitive-globular-maps.lagda.md +++ b/src/structured-types/large-lax-transitive-globular-maps.lagda.md @@ -30,7 +30,7 @@ between two `f : G → H` equipped with a family of 2-cells ```text - H₂ (f₁ (q ∘G p)) (f₁ q ∘H f₁ p) + H₂ (f₁ q ∘H f₁ p) (f₁ (q ∘G p)) ``` from the image of the composite of two 1-cells `q` and `p` in `G` to the diff --git a/src/structured-types/lax-transitive-globular-maps.lagda.md b/src/structured-types/lax-transitive-globular-maps.lagda.md index 6a4341e5d1..7ef7aea679 100644 --- a/src/structured-types/lax-transitive-globular-maps.lagda.md +++ b/src/structured-types/lax-transitive-globular-maps.lagda.md @@ -26,7 +26,7 @@ and `H` is a [globular map](structured-types.globular-maps.md) `f : G → H` equipped with a family of 2-cells ```text - H₂ (f₁ (q ∘G p)) (f₁ q ∘H f₁ p) + H₂ (f₁ q ∘H f₁ p) (f₁ (q ∘G p)) ``` from the image of the composite of two 1-cells `q` and `p` in `G` to the