Pour Categories.Commutativity into Categories.Morphism

Cubical/Categories/Morphism.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 module Cubical.Categories.Morphism where
 
 open import Cubical.Foundations.HLevels
@@ -16,7 +17,27 @@ module _ (C : Category ℓ ℓ') where
 
   private
     variable
-      x y z v w : ob
+      x y z v u w : ob
+
+  compSq : ∀ {f : C [ x , y ]} {g h} {k : C [ z , w ]} {l} {m} {n : C [ u , v ]}
+         -- square 1
+         → f ⋆ g ≡ h ⋆ k
+         -- square 2 (sharing g)
+         → k ⋆ l ≡ m ⋆ n
+         → f ⋆ (g ⋆ l) ≡ (h ⋆ m) ⋆ n
+  compSq {f = f} {g} {h} {k} {l} {m} {n} p q
+    = f ⋆ (g ⋆ l)
+    ≡⟨ sym (⋆Assoc _ _ _) ⟩
+      (f ⋆ g) ⋆ l
+    ≡⟨ cong (_⋆ l) p ⟩
+      (h ⋆ k) ⋆ l
+    ≡⟨ ⋆Assoc _ _ _ ⟩
+      h ⋆ (k ⋆ l)
+    ≡⟨ cong (h ⋆_) q ⟩
+      h ⋆ (m ⋆ n)
+    ≡⟨ sym (⋆Assoc _ _ _) ⟩
+      (h ⋆ m) ⋆ n
+    ∎
 
   isMonic : Hom[ x , y ] → Type (ℓ-max ℓ ℓ')
   isMonic {x} {y} f =

Cubical/Categories/NaturalTransformation/Base.agda

@@ -8,7 +8,6 @@ open import Cubical.Data.Sigma
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Functor.Properties
-open import Cubical.Categories.Commutativity
 open import Cubical.Categories.Morphism
 open import Cubical.Categories.Isomorphism
 
@@ -117,19 +116,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
   -- vertical sequencing
   seqTrans : {F G H : Functor C D} (α : NatTrans F G) (β : NatTrans G H) → NatTrans F H
   seqTrans α β .N-ob x = (α .N-ob x) ⋆ᴰ (β .N-ob x)
-  seqTrans {F} {G} {H} α β .N-hom f =
-    (F .F-hom f) ⋆ᴰ ((α .N-ob _) ⋆ᴰ (β .N-ob _))
-      ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
-    ((F .F-hom f) ⋆ᴰ (α .N-ob _)) ⋆ᴰ (β .N-ob _)
-      ≡[ i ]⟨ (α .N-hom f i) ⋆ᴰ (β .N-ob _) ⟩
-    ((α .N-ob _) ⋆ᴰ (G .F-hom f)) ⋆ᴰ (β .N-ob _)
-      ≡⟨ D .⋆Assoc _ _ _ ⟩
-    (α .N-ob _) ⋆ᴰ ((G .F-hom f) ⋆ᴰ (β .N-ob _))
-      ≡[ i ]⟨ (α .N-ob _) ⋆ᴰ (β .N-hom f i) ⟩
-    (α .N-ob _) ⋆ᴰ ((β .N-ob _) ⋆ᴰ (H .F-hom f))
-      ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
-    ((α .N-ob _) ⋆ᴰ (β .N-ob _)) ⋆ᴰ (H .F-hom f)
-      ∎
+  seqTrans α β .N-hom f = compSq D (α .N-hom f) (β .N-hom f)
 
   compTrans : {F G H : Functor C D} (β : NatTrans G H) (α : NatTrans F G) → NatTrans F H
   compTrans β α = seqTrans α β
@@ -154,7 +141,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
     -- compose the two commuting squares
     -- 1. α's commuting square
     -- 2. β's commuting square, but extended to G since β is only G' ≡> H
-    = compSq {C = D} (α .N-hom f) βSq
+    = compSq D (α .N-hom f) βSq
     where
       -- functor equality implies equality of actions on objects and morphisms
       Gx≡G'x : G ⟅ x ⟆ ≡ G' ⟅ x ⟆