-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathII.agda
108 lines (80 loc) · 4.07 KB
/
II.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
module II where
open import Lib hiding (id; _∘_)
data PS : Set where P S : PS
infixl 7 _[_]T
infixl 5 _,s_
infix 6 _∘_
infixl 8 _[_]t
infixl 3 _▶_
postulate
Con : Set
Ty : Con → PS → Set
Tm : ∀ Γ → ∀ {k} → Ty Γ k → Set
Sub : Con → Con → Set
∙ : Con
_▶_ : ∀{k}(Γ : Con) → Ty Γ k → Con
_[_]T : ∀{k Γ Δ} → Ty Δ k → Sub Γ Δ → Ty Γ k
id : ∀{Γ} → Sub Γ Γ
_∘_ : ∀{Γ Δ Σ} → Sub Δ Σ → Sub Γ Δ → Sub Γ Σ
ε : ∀{Γ} → Sub Γ ∙
_,s_ : ∀{k Γ Δ}(σ : Sub Γ Δ){A : Ty Δ k} → Tm Γ (A [ σ ]T) → Sub Γ (Δ ▶ A)
π₁ : ∀{k Γ Δ}{A : Ty Δ k} → Sub Γ (Δ ▶ A) → Sub Γ Δ
_[_]t : ∀{k Γ Δ}{A : Ty Δ k} → Tm Δ A → (σ : Sub Γ Δ) → Tm Γ (A [ σ ]T)
π₂ : ∀{k Γ Δ}{A : Ty Δ k}(σ : Sub Γ (Δ ▶ A)) → Tm Γ (A [ π₁ σ ]T)
[id]T : ∀{k Γ}{A : Ty Γ k} → A [ id ]T ≡ A
[][]T : ∀{k Γ Δ Σ}{A : Ty Σ k}{σ : Sub Γ Δ}{δ : Sub Δ Σ}
→ A [ δ ]T [ σ ]T ≡ A [ δ ∘ σ ]T
idl : ∀{Γ Δ}{σ : Sub Γ Δ} → (id ∘ σ) ≡ σ
idr : ∀{Γ Δ}{σ : Sub Γ Δ} → (σ ∘ id) ≡ σ
ass : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
→ (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
,∘ : ∀{k Γ Δ Σ}{δ : Sub Γ Δ}{σ : Sub Σ Γ}{A : Ty Δ k}{t : Tm Γ (A [ δ ]T)}
→ ((δ ,s t) ∘ σ) ≡ ((δ ∘ σ) ,s tr (Tm Σ) [][]T (t [ σ ]t))
π₁β : ∀{k Γ Δ}{A : Ty Δ k}{σ : Sub Γ Δ}{t : Tm Γ (A [ σ ]T)}
→ (π₁ (σ ,s t)) ≡ σ
πη : ∀{k Γ Δ}{A : Ty Δ k}{σ : Sub Γ (Δ ▶ A)}
→ (π₁ σ ,s π₂ σ) ≡ σ
εη : ∀{Γ}{σ : Sub Γ ∙}
→ σ ≡ ε
π₂β : ∀{k Γ Δ}{A : Ty Δ k}{σ : Sub Γ Δ}{t : Tm Γ (A [ σ ]T)}
→ π₂ (σ ,s t) ≡ tr (λ σ → Tm Γ (A [ σ ]T)) (π₁β ⁻¹) t
wk : ∀{k Γ}{A : Ty Γ k} → Sub (Γ ▶ A) Γ
wk = π₁ id
vz : ∀{k Γ}{A : Ty Γ k} → Tm (Γ ▶ A) (A [ wk ]T)
vz = π₂ id
vs : ∀{k l Γ}{A : Ty Γ k}{B : Ty Γ l} → Tm Γ A → Tm (Γ ▶ B) (A [ wk ]T)
vs x = x [ wk ]t
<_> : ∀{k Γ}{A : Ty Γ k} → Tm Γ A → Sub Γ (Γ ▶ A)
< t > = id ,s tr (Tm _) ([id]T ⁻¹) t
infix 4 <_>
_^_ : ∀ {k}{Γ Δ : Con}(σ : Sub Γ Δ)(A : Ty Δ k) → Sub (Γ ▶ (A [ σ ]T)) (Δ ▶ A)
_^_ {k}{Γ} {Δ} σ A = σ ∘ wk ,s coe (Tm _ & [][]T) (vz {k}{Γ}{A [ σ ]T})
infixl 5 _^_
-- Universe
--------------------------------------------------------------------------------
postulate
U : ∀{Γ} → Ty Γ S
U[] : ∀{Γ Δ}{σ : Sub Γ Δ} → (U [ σ ]T) ≡ U
El : ∀{Γ}(a : Tm Γ U) → Ty Γ P
El[] : ∀{Γ Δ}{σ : Sub Γ Δ}{a : Tm Δ U}
→ (El a [ σ ]T) ≡ (El (coe (Tm Γ & U[]) (a [ σ ]t)))
-- Inductive functions
--------------------------------------------------------------------------------
postulate
Π : ∀{k Γ}(a : Tm Γ U)(B : Ty (Γ ▶ El a) k) → Ty Γ k
Π[] : ∀{k Γ Δ}{σ : Sub Γ Δ}{a : Tm Δ U}{B : Ty (Δ ▶ El a) k}
→ (Π a B) [ σ ]T ≡ Π (tr (Tm Γ) U[] (a [ σ ]t))
(tr (λ x → Ty (Γ ▶ x) k) El[] (B [ σ ^ El a ]T))
app : ∀{k Γ}{a : Tm Γ U}{B : Ty (Γ ▶ El a) k} → Tm Γ (Π a B) → Tm (Γ ▶ El a) B
app[] : ∀{k Γ Δ}{σ : Sub Γ Δ}{a : Tm Δ U}{B : Ty (Δ ▶ El a) k}{t : Tm Δ (Π a B)}
→ tr2 (λ A → Tm (Γ ▶ A)) El[] refl (app t [ σ ^ El a ]t)
≡ app (tr (Tm _) Π[] (t [ σ ]t))
-- External functions
------------------------------------------------------------------------------
postulate
Π̂ : ∀{k Γ}(T : Set)(B : T → Ty Γ k) → Ty Γ k
Π̂[] : ∀{k Γ Δ}{σ : Sub Γ Δ}{T : Set}{B : T → Ty Δ k}
→ (Π̂ T B) [ σ ]T ≡ Π̂ T λ τ → B τ [ σ ]T
âpp : ∀{k Γ T}{B : T → Ty Γ k}(f : Tm Γ (Π̂ T B))(τ : T) → Tm Γ (B τ)
âpp[] : ∀{k Γ Δ}{σ : Sub Γ Δ}{T}{B : T → Ty Δ k}{f : Tm Δ (Π̂ T B)}{τ : T}
→ âpp {B = λ τ → B τ [ σ ]T} (tr (Tm Γ) Π̂[] (f [ σ ]t)) τ ≡ (âpp f τ) [ σ ]t