Additions to Common.agda

formalizations/guarded-cubical/Common/Common.agda

-{-# OPTIONS --cubical --rewriting --guarded #-}
+{-# OPTIONS --cubical #-}
 
  -- to allow opening this module in other files while there are still holes
 {-# OPTIONS --allow-unsolved-metas #-}
@@ -14,6 +14,12 @@ open import Cubical.Data.Empty
 open import Cubical.Data.Unit renaming (Unit to ⊤)
 
 
+private
+  variable
+    ℓ ℓ' : Level
+    ℓA ℓB ℓC ℓD : Level
+    ℓR ℓS : Level
+
 id : {ℓ : Level} -> {A : Type ℓ} -> A -> A
 id x = x
 
@@ -32,3 +38,15 @@ inl≠inr {_} {_} {A} {B} a b eq = transport (cong (diagonal ⊤ ⊥) eq) tt
     diagonal : (Left Right : Type) -> (A ⊎ B) -> Type
     diagonal Left Right (inl a) = Left
     diagonal Left Right (inr b) = Right
+
+TwoCell : {A : Type ℓA} {B : Type ℓB} {C : Type ℓC} {D : Type ℓD} ->
+-- {A C : Type ℓ} -> {B D : Type ℓ'}
+  (R : A -> B -> Type ℓR) ->
+  (S : C -> D -> Type ℓS)
+  (f : A -> C) ->
+  (g : B -> D) ->
+  Type (ℓ-max (ℓ-max (ℓ-max ℓA ℓB) ℓR) ℓS)
+-- Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓR) ℓS)
+TwoCell R S f g = ∀ a b -> R a b -> S (f a) (g b)
+
+