From 803a6935d52b256210dce0d7d87757f90bf5e9c2 Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Fri, 7 Feb 2025 15:43:12 +0000 Subject: [PATCH 1/4] Add some facts about the parallel arrow category --- src/Cat/Instances/Shape/Parallel.lagda.md | 79 +++++++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/src/Cat/Instances/Shape/Parallel.lagda.md b/src/Cat/Instances/Shape/Parallel.lagda.md index 23eb71651..2f9f5167e 100644 --- a/src/Cat/Instances/Shape/Parallel.lagda.md +++ b/src/Cat/Instances/Shape/Parallel.lagda.md @@ -1,5 +1,9 @@ # The "parallel arrows" category {defines="parallel-arrows"} @@ -70,12 +81,49 @@ parallel arrows between them. It is the shape of [[equaliser]] and ``` --> +The parallel category is isomorphic to its opposite through the involution `not : Bool → Bool`. + +```agda +·⇇· = ·⇉· ^op + +·⇇·≡·⇉· : ·⇇· ≡ ·⇉· +·⇇·≡·⇉· = Precategory-path F F-is-iso where + F : Functor ·⇇· ·⇉· + F .F₀ x = not x + F .F₁ {true} {true} tt = tt + F .F₁ {true} {false} f = f + F .F₁ {false} {false} tt = tt + F .F-id {true} = refl + F .F-id {false} = refl + F .F-∘ {true} {true} {true} f g = refl + F .F-∘ {true} {true} {false} f g = refl + F .F-∘ {true} {false} {false} f g = refl + F .F-∘ {false} {false} {false} f g = refl + + F-is-iso : is-precat-iso F + F-is-iso .has-is-ff {true} {true} .is-eqv _ = hlevel 0 + F-is-iso .has-is-ff {true} {false} = id-equiv + F-is-iso .has-is-ff {false} {false} .is-eqv y = hlevel 0 + F-is-iso .has-is-iso = not-is-equiv +``` + + + +Paralell pairs of morphisms in a category $\cC$ are equivalent to functors from the +walking parallel arrow category to $\cC$. +```agda Fork : ∀ {a b} (f g : Hom a b) → Functor ·⇉· C Fork f g = funct where funct : Functor _ _ @@ -91,6 +139,37 @@ module _ {o ℓ} {C : Precategory o ℓ} where funct .F-∘ {false} {false} {true} f g = sym (idr _) funct .F-∘ {false} {true} {true} tt _ = sym (idl _) funct .F-∘ {true} {true} {true} tt tt = sym (idl _) +``` + +A natural transformation between two diagrams +$A \stackrel{\overset{f}{\longrightarrow}}{\underset{g}{\longrightarrow}} B$ and +$C \stackrel{\overset{f'}{\longrightarrow}}{\underset{g'}{\longrightarrow}} D$ +is given by a pair of commutative squares + +~~~{.quiver} +\begin{tikzcd} + A & B && A & B \\ + C & D && C & D + \arrow["f", from=1-1, to=1-2] + \arrow["u"', from=1-1, to=2-1] + \arrow["v", from=1-2, to=2-2] + \arrow["g", from=1-4, to=1-5] + \arrow["u"', from=1-4, to=2-4] + \arrow["v", from=1-5, to=2-5] + \arrow["{f'}", from=2-1, to=2-2] + \arrow["{g'}", from=2-4, to=2-5] +\end{tikzcd}. +~~~ + +```agda + Fork-nt : ∀ {A B C D} {f g : Hom A B} {f' g' : Hom C D} {u : Hom A C} {v : Hom B D} → + (α : v ∘ f ≡ f' ∘ u) (β : v ∘ g ≡ g' ∘ u) → (Fork f g) => (Fork f' g') + Fork-nt {u = u} _ _ ._=>_.η false = u + Fork-nt {v = v} _ _ ._=>_.η true = v + Fork-nt _ _ .is-natural true true _ = id-comm + Fork-nt _ _ .is-natural false false _ = id-comm + Fork-nt _ β .is-natural false true true = β + Fork-nt α _ .is-natural false true false = α forkl : (F : Functor ·⇉· C) → Hom (F .F₀ false) (F .F₀ true) forkl F = F .F₁ {false} {true} false From 75f2b085cb5917919192082153a77f709d2b39c8 Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Sat, 8 Feb 2025 19:07:06 +0000 Subject: [PATCH 2/4] spelling and slight refactor --- src/Cat/Instances/Shape/Parallel.lagda.md | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/Cat/Instances/Shape/Parallel.lagda.md b/src/Cat/Instances/Shape/Parallel.lagda.md index 2f9f5167e..ee44d0018 100644 --- a/src/Cat/Instances/Shape/Parallel.lagda.md +++ b/src/Cat/Instances/Shape/Parallel.lagda.md @@ -81,7 +81,8 @@ parallel arrows between them. It is the shape of [[equaliser]] and ``` --> -The parallel category is isomorphic to its opposite through the involution `not : Bool → Bool`. +The parallel category is isomorphic to its opposite through the +involution `not`{.Agda}. ```agda ·⇇· = ·⇉· ^op @@ -101,10 +102,11 @@ The parallel category is isomorphic to its opposite through the involution `not F .F-∘ {false} {false} {false} f g = refl F-is-iso : is-precat-iso F - F-is-iso .has-is-ff {true} {true} .is-eqv _ = hlevel 0 - F-is-iso .has-is-ff {true} {false} = id-equiv - F-is-iso .has-is-ff {false} {false} .is-eqv y = hlevel 0 F-is-iso .has-is-iso = not-is-equiv + F-is-iso .has-is-ff {true} {true} = id-equiv + F-is-iso .has-is-ff {true} {false} = id-equiv + F-is-iso .has-is-ff {false} {false} = id-equiv + F-is-iso .has-is-ff {false} {true} .is-eqv () ``` -Paralell pairs of morphisms in a category $\cC$ are equivalent to functors from the +Parallel pairs of morphisms in a category $\cC$ are equivalent to functors from the walking parallel arrow category to $\cC$. ```agda @@ -142,14 +144,14 @@ walking parallel arrow category to $\cC$. ``` A natural transformation between two diagrams -$A \stackrel{\overset{f}{\longrightarrow}}{\underset{g}{\longrightarrow}} B$ and -$C \stackrel{\overset{f'}{\longrightarrow}}{\underset{g'}{\longrightarrow}} D$ -is given by a pair of commutative squares +$A\ \overset{f}{\underset{g}{\tto}}\ B$ and +$C\ \overset{f'}{\underset{g'}{\tto}}\ D$ is given by a pair of +commutative squares ~~~{.quiver} \begin{tikzcd} A & B && A & B \\ - C & D && C & D + C & D && C & D. \arrow["f", from=1-1, to=1-2] \arrow["u"', from=1-1, to=2-1] \arrow["v", from=1-2, to=2-2] @@ -158,7 +160,7 @@ is given by a pair of commutative squares \arrow["v", from=1-5, to=2-5] \arrow["{f'}", from=2-1, to=2-2] \arrow["{g'}", from=2-4, to=2-5] -\end{tikzcd}. +\end{tikzcd} ~~~ ```agda From 554a93e77edc00c3e2fc144f76e4ac1134f58bc5 Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Sat, 8 Feb 2025 19:08:46 +0000 Subject: [PATCH 3/4] remove useless dependency --- src/Cat/Instances/Shape/Parallel.lagda.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Cat/Instances/Shape/Parallel.lagda.md b/src/Cat/Instances/Shape/Parallel.lagda.md index ee44d0018..2b96cb073 100644 --- a/src/Cat/Instances/Shape/Parallel.lagda.md +++ b/src/Cat/Instances/Shape/Parallel.lagda.md @@ -1,7 +1,5 @@