From ac738dd602cb0f8a0bb0301dc1380fd97bb75655 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 11 Jul 2023 17:11:23 -0400
Subject: [PATCH] Additions to Common.agda

---
 .../guarded-cubical/Common/Common.agda        | 20 ++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/formalizations/guarded-cubical/Common/Common.agda b/formalizations/guarded-cubical/Common/Common.agda
index 9c08594..b4235a6 100644
--- a/formalizations/guarded-cubical/Common/Common.agda
+++ b/formalizations/guarded-cubical/Common/Common.agda
@@ -1,4 +1,4 @@
-{-# 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)
+
+
-- 
GitLab