Add box types.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 28a3c18..0e65790 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -105,6 +105,9 @@ convertCnstr
 convertCnstr Bool Bool = pure True
 convertCnstr True True = pure True
 convertCnstr False False = pure True
+convertCnstr (Box {prop}) (Box {prop = prop'}) =
+  convert {rel = Relevant, type = cast Prop, left = prop, right = prop'}
+convertCnstr MkBox MkBox = pure True
 convertCnstr Top Top = pure True
 convertCnstr Bottom Bottom = pure True
 convertCnstr left right = pure False
@@ -200,6 +203,7 @@ convertEta (Pair {indexRel = Relevant, elementRel = Irrelevant, prf, first, seco
 convertEta (Pair {indexRel = Irrelevant, elementRel = Relevant, prf, first, second}) right = do
   let rightSecond = Second {firstRel = Relevant, arg = right}
   convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
+convertEta MkBox right = pure True
 convertEta left right = pure False
 
 convertUntyped Irrelevant left right = pure True