Prove reducibility is reflexive.

1 files changed, 83 insertions, 0 deletions

diff --git a/src/Core/Reducible.idr b/src/Core/Reducible.idr
index 0bb4027..33f7121 100644
--- a/src/Core/Reducible.idr
+++ b/src/Core/Reducible.idr
@@ -417,3 +417,86 @@ LogRelRec eq Large Small LTSmall = LogRelKit eq Small (\_, prf => absurd prf)
 public export
 LogRel : (eq : Equality) -> Level -> LogicalRelation eq
 LogRel eq l = LogRelKit eq l (LogRelRec eq l)
+
+-- Reflexivity -----------------------------------------------------------------
+
+export
+typeEqRefl :
+  IsEq eq =>
+  (l : Level) ->
+  (red : (LogRel eq l).TypeRed env a) ->
+  (LogRel eq l).TypeEq env a a red
+typeEqRefl l (RedNtrlTy red) =
+  EqNtrlTy $ MkNtrlTyEq
+    { tyWf = red.tyWf
+    , steps = red.steps
+    , tyWf' = red.tyWf'
+    , ntrl = red.ntrl
+    , prf = red.prf
+    }
+typeEqRefl l (RedSetTy red) =
+  EqSetTy $ MkSetTyEq
+    { tyWf = red.tyWf
+    , steps = red.steps
+    , tyWf' = red.tyWf'
+    }
+typeEqRefl l (RedPiTy (MkPiTyRed tyWf steps tyWf' prf domRed codRed codEq)) =
+  EqPiTy $ MkPiTyEq
+    { tyWf = tyWf
+    , steps = steps
+    , tyWf' = tyWf'
+    , prf = prf
+    , domEq = \thinWf => typeEqRefl l (domRed thinWf)
+    , codEq = \thinWf, red' => typeEqRefl l (codRed thinWf red')
+    }
+
+export
+termEqRefl :
+  IsEq eq =>
+  (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
+termEqRefl l (RedNtrlTy red) (RedNtrlTm redTm) =
+  EqNtrlTm $ MkNtrlTmEq
+    { tmWf1 = redTm.tmWf
+    , tmWf2 = redTm.tmWf
+    , steps1 = redTm.steps
+    , steps2 = redTm.steps
+    , tmWf1' = redTm.tmWf'
+    , tmWf2' = redTm.tmWf'
+    , ntrl1 = redTm.ntrl
+    , 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
+    , tmWf2 = redTm.tmWf
+    , steps1 = redTm.steps
+    , steps2 = redTm.steps
+    , tmWf1' = redTm.tmWf'
+    , tmWf2' = redTm.tmWf'
+    , whnf1 = redTm.whnf
+    , whnf2 = redTm.whnf
+    , prf = redTm.prf
+    , tyRed1 = redTm.tyRed
+    , tyRed2 = redTm.tyRed
+    , tyEq = typeEqRefl {eq} Small redTm.tyRed
+    }
+termEqRefl l (RedPiTy red@(MkPiTyRed _ _ _ _ domRed _ _)) (RedPiTm redTm) =
+  EqPiTm $ MkPiTmEq
+    { tmWf1 = redTm.tmWf
+    , tmWf2 = redTm.tmWf
+    , steps1 = redTm.steps
+    , steps2 = redTm.steps
+    , tmWf1' = redTm.tmWf'
+    , tmWf2' = redTm.tmWf'
+    , whnf1 = redTm.whnf
+    , whnf2 = redTm.whnf
+    , prf = redTm.prf
+    , red1 = redTm
+    , red2 = redTm
+    , codEq = \thinWf, red' => redTm.codEq thinWf red' red' (termEqRefl l (domRed thinWf) red')
+    }