diff options
| -rw-r--r-- | src/Core/LogRel.idr | 5 | ||||
| -rw-r--r-- | src/Core/LogRel/View.idr | 7 |
2 files changed, 9 insertions, 3 deletions
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 diff --git a/src/Core/LogRel/View.idr b/src/Core/LogRel/View.idr index ecb6cc2..1790c9f 100644 --- a/src/Core/LogRel/View.idr +++ b/src/Core/LogRel/View.idr @@ -83,3 +83,10 @@ view (RedPiTy red1) (RedSetTy red2) (EqPiTy tyEq) = in absurd det view (RedPiTy red1) (RedPiTy red2) (EqPiTy tyEq) = Pi red1 red2 + +public export +viewRefl : + (red1 : (LogRel eq l1).TypeRed env a) -> + (red2 : (LogRel eq l2).TypeRed env a) -> + ShapeView red1 red2 +viewRefl red1 red2 = view red1 red2 (typeEqRefl _ red1) |