diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-23 14:57:22 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-23 14:57:22 +0100 |
| commit | dddc8083b56f265e1e53cd3e6d2e374b25f42cb3 (patch) | |
| tree | fcc4b0068862d91ff2b9d2161a4a051af70d5aed /src/Core/LogRel.idr | |
| parent | 8baf4268940277164f1462187501225033ec93c4 (diff) | |
Construct shape views reflexively.
Diffstat (limited to 'src/Core/LogRel.idr')
| -rw-r--r-- | src/Core/LogRel.idr | 5 |
1 files changed, 2 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 |