Pour Commutativity into Morphism

Author: anshwad10

Cubical/Categories/Commutativity.agda

@@ -78,7 +78,28 @@ 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
+    ∎
+
 
   open areInv