blob: 64e6c97213c1706093d328900f8e160b8ae83442 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.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.stepsWf.steps tyEq.stepsWf.steps Set Pi
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)
|
