1 files changed, 85 insertions, 0 deletions
diff --git a/src/Core/LogRel/View.idr b/src/Core/LogRel/View.idr
new file mode 100644
index 0000000..ecb6cc2
--- /dev/null
+++ b/src/Core/LogRel/View.idr
@@ -0,0 +1,85 @@
+module Core.LogRel.View
+
+import Core.Environment
+import Core.Generic
+import Core.LogRel
+import Core.Reduction
+import Core.Term
+import Core.Term.NormalForm
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data ShapeView : (LogRel eq l1).TypeRed env a -> (LogRel eq l2).TypeRed env b -> Type where
+  Ntrl :
+    (red1 : NeutralTyRed eq l1 (LogRelRec eq l1) env a) ->
+    (red2 : NeutralTyRed eq l2 (LogRelRec eq l2) env b) ->
+    ShapeView (RedNtrlTy red1) (RedNtrlTy red2)
+  Set :
+    (red1 : SetTyRed eq l1 (LogRelRec eq l1) env a) ->
+    (red2 : SetTyRed eq l2 (LogRelRec eq l2) env b) ->
+    ShapeView (RedSetTy red1) (RedSetTy red2)
+  Pi :
+    (red1 : PiTyRed eq l1 (LogRelRec eq l1) env a) ->
+    (red2 : PiTyRed eq l2 (LogRelRec eq l2) env b) ->
+    ShapeView (RedPiTy red1) (RedPiTy red2)
+
+-- Construction ----------------------------------------------------------------
+
+export
+view :
+  (red1 : (LogRel eq l1).TypeRed {n} env a) ->
+  (red2 : (LogRel eq l2).TypeRed env b) ->
+  (LogRel eq l1).TypeEq env a b red1 ->
+  ShapeView red1 red2
+view (RedNtrlTy red1) (RedNtrlTy red2) (EqNtrlTy tyEq) = Ntrl red1 red2
+view (RedNtrlTy red1) (RedSetTy red2) (EqNtrlTy tyEq) =
+  let
+    det : (Set = tyEq.b')
+    det = typeRedDeterministic red2.steps tyEq.steps Set (Ntrl tyEq.ntrl)
+
+    ntrl : Neutral (Set {n})
+    ntrl = rewrite det in tyEq.ntrl
+  in
+  absurd ntrl
+view (RedNtrlTy red1) (RedPiTy red2) (EqNtrlTy tyEq) =
+  let
+    det : (Pi red2.f red2.g = tyEq.b')
+    det = typeRedDeterministic red2.steps tyEq.steps Pi (Ntrl tyEq.ntrl)
+
+    ntrl : Neutral (Pi red2.f red2.g)
+    ntrl = rewrite det in tyEq.ntrl
+  in
+  absurd ntrl
+view (RedSetTy red1) (RedNtrlTy red2) (EqSetTy tyEq) =
+  let
+    det : (red2.a' = Set)
+    det = typeRedDeterministic red2.steps tyEq.steps (Ntrl red2.ntrl) Set
+
+    ntrl : Neutral (Set {n})
+    ntrl = rewrite sym det in red2.ntrl
+  in
+  absurd ntrl
+view (RedSetTy red1) (RedSetTy red2) (EqSetTy tyEq) = Set red1 red2
+view (RedSetTy red1) (RedPiTy red2) (EqSetTy tyEq) =
+  let
+    det : (Pi red2.f red2.g = Set)
+    det = typeRedDeterministic red2.steps tyEq.steps Pi Set
+  in
+  absurd det
+view (RedPiTy red1) (RedNtrlTy red2) (EqPiTy tyEq) =
+  let
+    det : (red2.a' = Pi tyEq.f tyEq.g)
+    det = typeRedDeterministic red2.steps tyEq.steps (Ntrl red2.ntrl) Pi
+
+    ntrl : Neutral (Pi tyEq.f tyEq.g)
+    ntrl = rewrite sym det in red2.ntrl
+  in
+  absurd ntrl
+view (RedPiTy red1) (RedSetTy red2) (EqPiTy tyEq) =
+  let
+    det : (Set = Pi tyEq.f tyEq.g)
+    det = typeRedDeterministic red2.steps tyEq.steps Set Pi
+  in
+  absurd det
+view (RedPiTy red1) (RedPiTy red2) (EqPiTy tyEq) = Pi red1 red2