-
Notifications
You must be signed in to change notification settings - Fork 0
/
Syntax.agda
121 lines (82 loc) · 3.7 KB
/
Syntax.agda
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
{-# OPTIONS --safe #-}
module ROmega.Equivalence.Syntax where
open import Agda.Primitive
open import Level
open import ROmega.Kinds
open import ROmega.Types
open import ROmega.Types.Substitution
--------------------------------------------------------------------------------
-- Generalized vars.
private
variable
ℓτ ℓΔ ℓκ ℓκ' ℓκ₁ ℓκ₂ ℓL ι : Level
Δ : KEnv ℓΔ
κ : Kind ℓκ
κ' : Kind ℓκ'
κ₁ : Kind ℓκ₁
κ₂ : Kind ℓκ₂
--------------------------------------------------------------------------------
-- Type & Predicate equivalence.
data _≡p_ : (π₁ π₂ : Pred Δ κ) → Set
data _≡t_ : (τ υ : Type Δ κ) → Set
infix 0 _≡p_
infix 0 _≡t_
data _≡p_ where
peq-≲ : ∀ {τ₁ τ₂ υ₁ υ₂ : Type Δ R[ κ ]} →
τ₁ ≡t υ₁ → τ₂ ≡t υ₂ →
------------------------
(τ₁ ≲ τ₂) ≡p υ₁ ≲ υ₂
peq-· : ∀ {τ₁ τ₂ τ₃ υ₁ υ₂ υ₃ : Type Δ R[ κ ]} →
τ₁ ≡t υ₁ → τ₂ ≡t υ₂ → τ₃ ≡t υ₃ →
----------------------------------
τ₁ · τ₂ ~ τ₃ ≡p υ₁ · υ₂ ~ υ₃
data _≡t_ where
teq-refl : {τ : Type Δ κ} →
---------------
τ ≡t τ
teq-sym : ∀ {τ₁ τ₂ : Type Δ κ} →
τ₁ ≡t τ₂ →
---------------
τ₂ ≡t τ₁
teq-trans : ∀ {τ₁ τ₂ τ₃ : Type Δ κ} →
τ₁ ≡t τ₂ → τ₂ ≡t τ₃ →
----------------------
τ₁ ≡t τ₃
teq-⇒ : ∀ {τ₁ τ₂ : Type Δ (★ ℓτ)} {π₁ π₂ : Pred Δ κ} →
π₁ ≡p π₂ → τ₁ ≡t τ₂ →
-----------------------
π₁ ⇒ τ₁ ≡t π₂ ⇒ τ₂
teq-∀ : ∀ {τ υ : Type (Δ , κ) (★ ℓτ)} →
τ ≡t υ →
----------------
`∀ κ τ ≡t `∀ κ υ
teq-β : ∀ {τ : Type (Δ , κ) κ'} {υ : Type Δ κ} →
------------------------------
((`λ κ τ) ·[ υ ]) ≡t (τ β[ υ ])
teq-· : ∀ {τ₁ υ₁ : Type Δ (κ `→ κ')} {τ₂ υ₂ : Type Δ κ} →
τ₁ ≡t υ₁ → τ₂ ≡t υ₂ →
------------------------
τ₁ ·[ τ₂ ] ≡t υ₁ ·[ υ₂ ]
teq-sing : ∀ {l₁ l₂ : Type Δ (L {ℓL})} →
{τ₁ τ₂ : Type Δ κ₁} →
l₁ ≡t l₂ → τ₁ ≡t τ₂ →
--------------------------------------
(l₁ R▹ τ₁) ≡t (l₂ R▹ τ₂)
teq-lift₁ : ∀ {l : Type Δ (L {ℓL})} {υ : Type Δ κ} {τ : Type Δ (κ `→ κ')} →
--------------------------------------
(l R▹ τ) ·⌈ υ ⌉ ≡t (l R▹ (τ ·[ υ ]))
teq-lift₂ : ∀ {l : Type Δ (L {ℓL})} {υ : Type Δ (κ₁ `→ κ₂)} {τ : Type Δ κ₁} →
--------------------------------------
⌈ υ ⌉· (l R▹ τ) ≡t (l R▹ (υ ·[ τ ]))
teq-⌊⌋ : ∀ {τ υ : Type Δ (L {ℓL})} →
τ ≡t υ →
-------------
⌊_⌋ {ι = ι} τ ≡t ⌊_⌋ {ι = ι} υ
teq-Π : ∀ {ρ₁ ρ₂ : Type Δ R[ ★ ℓκ ] } →
ρ₁ ≡t ρ₂ →
-------------
Π ρ₁ ≡t Π ρ₂
teq-Σ : ∀ {ρ₁ ρ₂ : Type Δ R[ ★ ℓκ ] } →
ρ₁ ≡t ρ₂ →
-------------
Σ ρ₁ ≡t Σ ρ₂