-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathCastTpEq.ced
125 lines (93 loc) · 5.34 KB
/
CastTpEq.ced
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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
module cast-tpeq.
Unit : ★ = ∀ X: ★. X ➔ X.
unit : Unit = Λ X. λ x. x.
{- A Cast is an identity function between types, used in the papers
[1] Efficient Mendler-Style Lambda Encodings in Cedille
[2] Course-of-Value Induction in Cedille
then renamed to Id in the papers
[3] Efficient Lambda Encodings for Mendler-Style Coinductive Types in Cedille
[4] Simulating Large Eliminations in Cedille
with the CoVI and Coinductives papers casting type families. -}
Cast : Π I: ★. (I ➔ ★) ➔ (I ➔ ★) ➔ ★
= λ I: ★. λ S: I ➔ ★. λ T: I ➔ ★. ι f: ∀ i: I. S i ➔ T i. {f ≃ Λ i. λ x. x}.
introCast : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★. ∀ f: ∀ i: I. S i ➔ T i.
(∀ i: I. Π x: S i. {f x ≃ x}) ➾ Cast ·I ·S ·T
= Λ I. Λ S. Λ T. Λ f. Λ p. [Λ i. λ x. φ (p -i x) - (f -i x) {|x|}, β].
elimCast : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★. Cast ·I ·S ·T ➾ ∀ i: I. S i ➔ T i
= Λ I. Λ S. Λ T. Λ c. Λ i. λ x. φ (ρ c.2 - β) - (c.1 -i x) {|x|}.
castRefl : ∀ I: ★. ∀ S: I ➔ ★. Cast ·I ·S ·S
= Λ I. Λ S. introCast -(Λ i. λ x. x) -(Λ i. λ x. β).
castTrans : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★. ∀ U: I ➔ ★.
Cast ·I ·S ·T ➾ Cast ·I ·T ·U ➾ Cast ·I ·S ·U
= Λ I. Λ S. Λ T. Λ U. Λ cst. Λ ctu.
introCast -(Λ i. λ x. elimCast -ctu -i (elimCast -cst -i x))
-(Λ i. λ x. β).
introCastId : {introCast ≃ λ x. x} = β.
elimCastId : {elimCast ≃ λ x. x} = β.
castReflId : {castRefl ≃ λ x. x} = β.
castTransId : {castTrans ≃ λ x. x} = β.
{- Nondependent version of Cast -}
Cast' : ★ ➔ ★ ➔ ★
= λ S: ★. λ T: ★. Cast ·Unit ·(λ _: Unit. S) ·(λ _: Unit. T).
introCast' : ∀ S: ★. ∀ T: ★. ∀ f: S ➔ T. (Π x: S. {f x ≃ x}) ➾ Cast' ·S ·T
= Λ S. Λ T. Λ f. Λ p. introCast ·Unit ·(λ _: Unit. S) ·(λ _: Unit. T) -(Λ _: Unit. f) -(Λ _: Unit. p).
elimCast' : ∀ S: ★. ∀ T: ★. Cast' ·S ·T ➾ S ➔ T
= Λ S. Λ T. Λ c. elimCast ·Unit ·(λ _: Unit. S) ·(λ _: Unit. T) -c -unit.
castRefl' : ∀ S: ★. Cast' ·S ·S
= Λ S. castRefl ·Unit ·(λ _: Unit. S).
castTrans' : ∀ S: ★. ∀ T: ★. ∀ U: ★. Cast' ·S ·T ➾ Cast' ·T ·U ➾ Cast' ·S ·U
= Λ S. Λ T. Λ U. Λ cst. Λ ctu. castTrans ·Unit ·(λ _: Unit. S) ·(λ _: Unit. T) ·(λ _: Unit. U) -cst -ctu.
{- A "type equality" is a Cast in both directions,
satisfying the properties of an equivalence relation,
but not truly an equality since it has no substitutive principle;
originally introduced in the Large Eliminations paper. -}
TpEq : Π I: ★. (I ➔ ★) ➔ (I ➔ ★) ➔ ★
= λ I: ★. λ S: I ➔ ★. λ T: I ➔ ★. ι _: Cast ·I ·S ·T. Cast ·I ·T ·S.
introTpEq : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★.
Cast ·I ·S ·T ➾ Cast ·I ·T ·S ➾ TpEq ·I ·S ·T
= Λ I. Λ S. Λ T. Λ cst. Λ cts.
[introCast -(elimCast -cst) -(Λ i. λ x. β),
introCast -(elimCast -cts) -(Λ i. λ x. β)].
elimTpEqL : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★. TpEq ·I ·S ·T ➾ ∀ i: I. S i ➔ T i
= Λ I. Λ S. Λ T. Λ tpeq. elimCast -tpeq.1.
elimTpEqR : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★. TpEq ·I ·S ·T ➾ ∀ i: I. T i ➔ S i
= Λ I. Λ S. Λ T. Λ tpeq. elimCast -tpeq.2.
tpEqRefl : ∀ I: ★. ∀ S: I ➔ ★. TpEq ·I ·S ·S
= Λ I. Λ S. introTpEq -(castRefl ·I ·S) -(castRefl ·I ·S).
tpEqSym : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★. TpEq ·I ·S ·T ➾ TpEq ·I ·T ·S
= Λ I. Λ S. Λ T. Λ tpeq. introTpEq -tpeq.2 -tpeq.1.
tpEqTrans : ∀ I: ★. ∀ S: I ➔ ★. ∀ T: I ➔ ★. ∀ U: I ➔ ★.
TpEq ·I ·S ·T ➾ TpEq ·I ·T ·U ➾ TpEq ·I ·S ·U
= Λ I. Λ S. Λ T. Λ U. Λ tpeqst. Λ tpeqtu.
introTpEq -(castTrans -tpeqst.1 -tpeqtu.1) -(castTrans -tpeqtu.2 -tpeqst.2).
introTpEqId : {introTpEq ≃ λ x. x} = β.
elimTpEqLId : {elimTpEqL ≃ λ x. x} = β.
elimTpEqRId : {elimTpEqR ≃ λ x. x} = β.
tpEqReflId : {tpEqRefl ≃ λ x. x} = β.
tpEqSymId : {tpEqSym ≃ λ x. x} = β.
tpEqTransId : {tpEqTrans ≃ λ x. x} = β.
{- Nondependent version of TpEq -}
TpEq' : ★ ➔ ★ ➔ ★
= λ S: ★. λ T: ★. TpEq ·Unit ·(λ _: Unit. S) ·(λ _: Unit. T).
introTpEq' : ∀ S: ★. ∀ T: ★. Cast' ·S ·T ➾ Cast' ·T ·S ➾ TpEq' ·S ·T
= Λ S. Λ T. Λ cst. Λ cts. introTpEq -cst -cts.
elimTpEqL' : ∀ S: ★. ∀ T: ★. TpEq' ·S ·T ➾ S ➔ T
= Λ S. Λ T. Λ tpeq. elimTpEqL -tpeq -unit.
elimTpEqR' : ∀ S: ★. ∀ T: ★. TpEq' ·S ·T ➾ T ➔ S
= Λ S. Λ T. Λ tpeq. elimTpEqR -tpeq -unit.
tpEqRefl' : ∀ S: ★. TpEq' ·S ·S
= Λ S. tpEqRefl ·Unit ·(λ _: Unit. S).
tpEqSym' : ∀ S: ★. ∀ T: ★. TpEq' ·S ·T ➾ TpEq' ·T ·S
= Λ S. Λ T. Λ tpeq. tpEqSym -tpeq.
tpEqTrans' : ∀ S: ★. ∀ T: ★. ∀ U: ★. TpEq' ·S ·T ➾ TpEq' ·T ·U ➾ TpEq' ·S ·U
= Λ S. Λ T. Λ U. Λ tpeqst. Λ tpeqtu. tpEqTrans -tpeqst -tpeqtu.
{- References
[1] https://arxiv.org/abs/1803.02473
[2] https://arxiv.org/abs/1811.11961
[3] https://arxiv.org/abs/2005.00199
[4] https://arxiv.org/abs/2112.07817
Other
* Elaborating Inductive Definitions and Course-of-Values Induction In Cedille
https://arxiv.org/abs/1903.08233
* Monotone Recursive Types and Recursive Data Representations in Cedille
https://arxiv.org/abs/2001.02828 -}