From dddc8083b56f265e1e53cd3e6d2e374b25f42cb3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 23 Apr 2023 14:57:22 +0100
Subject: Construct shape views reflexively.

---
 src/Core/LogRel.idr | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'src/Core/LogRel.idr')

diff --git a/src/Core/LogRel.idr b/src/Core/LogRel.idr
index 19a7071..f7e2e06 100644
--- a/src/Core/LogRel.idr
+++ b/src/Core/LogRel.idr
@@ -422,7 +422,7 @@ LogRel eq l = LogRelKit eq l (LogRelRec eq l)
 
 export
 typeEqRefl :
-  (l : Level) ->
+  (0 l : Level) ->
   (red : (LogRel eq l).TypeRed env a) ->
   (LogRel eq l).TypeEq env a a red
 typeEqRefl l (RedNtrlTy red) =
@@ -451,7 +451,7 @@ typeEqRefl l (RedPiTy (MkPiTyRed tyWf steps tyWf' prf domRed codRed codEq)) =
 
 export
 termEqRefl :
-  (l : Level) ->
+  (0 l : Level) ->
   (red : (LogRel eq l).TypeRed env a) ->
   (LogRel eq l).TermRed env t a red ->
   (LogRel eq l).TermEq env t t a red
@@ -467,7 +467,6 @@ termEqRefl l (RedNtrlTy red) (RedNtrlTm redTm) =
     , ntrl2 = redTm.ntrl
     , prf = redTm.prf
     }
-termEqRefl Small (RedSetTy (MkSetTyRed tyWf steps tyWf' prf)) (RedSetTm redTm) = absurd prf
 termEqRefl Large (RedSetTy (MkSetTyRed tyWf steps tyWf' LTSmall)) (RedSetTm redTm) =
   EqSetTm $ MkSetTmEq
     { tmWf1 = redTm.tmWf
-- 
cgit v1.2.3