Skip to content

Commit 3b0425d

Browse files
mr-ohmanmr-ohman
committed
Moved reducible application to its own file.
1 parent e93ef46 commit 3b0425d

File tree

6 files changed

+153
-132
lines changed

6 files changed

+153
-132
lines changed

‎Definition/LogicalRelation/Application.agda

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Definition.Typed.EqualityRelation
4+
5+
module Definition.LogicalRelation.Application {{eqrel : EqRelSet}} where
6+
open EqRelSet {{...}}
7+
8+
open import Definition.Untyped hiding (wk)
9+
import Definition.Untyped as U
10+
open import Definition.Untyped.Properties
11+
open import Definition.Typed
12+
import Definition.Typed.Weakening as T
13+
open import Definition.Typed.Properties
14+
open import Definition.Typed.RedSteps
15+
open import Definition.LogicalRelation
16+
open import Definition.LogicalRelation.EqView
17+
open import Definition.LogicalRelation.Irrelevance
18+
open import Definition.LogicalRelation.Properties
19+
20+
open import Tools.Empty
21+
open import Tools.Product
22+
23+
import Tools.PropositionalEquality as PE
24+
25+
26+
-- Helper function for application of specific type derivations.
27+
appTerm′ : ∀ {F G t u Γ l l′ l″}
28+
([F] : Γ ⊩⟨ l″ ⟩ F)
29+
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
30+
([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
31+
([t] : Γ ⊩⟨ l ⟩ t ∷ Π F ▹ G / Π-intr [ΠFG])
32+
([u] : Γ ⊩⟨ l″ ⟩ u ∷ F / [F])
33+
→ Γ ⊩⟨ l′ ⟩ t ∘ u ∷ G [ u ] / [G[u]]
34+
appTerm′ {t = t} {Γ = Γ} [F] [G[u]] (noemb (Π F G D ⊢F ⊢G A≡A [F′] [G′] G-ext))
35+
(Πₜ f d funcF f≡f [f] [f]₁) [u] =
36+
let ΠFG≡ΠF′G′ = whnfRed* (red D) Π
37+
F≡F′ , G≡G′ = Π-PE-injectivity ΠFG≡ΠF′G′
38+
F≡idF′ = PE.trans F≡F′ (PE.sym (wk-id _))
39+
idG′ᵤ≡Gᵤ = PE.cong (λ x → x [ _ ]) (PE.trans (wk-lift-id _) (PE.sym G≡G′))
40+
idf∘u≡f∘u = (PE.cong (λ x → x ∘ _) (wk-id _))
41+
⊢Γ = wf ⊢F
42+
[u]′ = irrelevanceTerm′ F≡idF′ [F] ([F′] T.id ⊢Γ) [u]
43+
[f∘u] = irrelevanceTerm″ idG′ᵤ≡Gᵤ idf∘u≡f∘u
44+
([G′] T.id ⊢Γ [u]′) [G[u]] ([f]₁ T.id ⊢Γ [u]′)
45+
⊢u = escapeTerm [F] [u]
46+
d′ = PE.subst (λ x → Γ ⊢ t ⇒* f ∷ x) (PE.sym ΠFG≡ΠF′G′) (redₜ d)
47+
in proj₁ (redSubst*Term (app-subst* d′ ⊢u) [G[u]] [f∘u])
48+
appTerm′ [F] [G[u]] (emb 0<1 x) [t] [u] = appTerm′ [F] [G[u]] x [t] [u]
49+
50+
-- Application of reducible terms.
51+
appTerm : ∀ {F G t u Γ l l′ l″}
52+
([F] : Γ ⊩⟨ l″ ⟩ F)
53+
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
54+
([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
55+
([t] : Γ ⊩⟨ l ⟩ t ∷ Π F ▹ G / [ΠFG])
56+
([u] : Γ ⊩⟨ l″ ⟩ u ∷ F / [F])
57+
→ Γ ⊩⟨ l′ ⟩ t ∘ u ∷ G [ u ] / [G[u]]
58+
appTerm [F] [G[u]] [ΠFG] [t] [u] =
59+
let [t]′ = irrelevanceTerm [ΠFG] (Π-intr (Π-elim [ΠFG])) [t]
60+
in appTerm′ [F] [G[u]] (Π-elim [ΠFG]) [t]′ [u]
61+
62+
-- Helper function for application congurence of specific type derivations.
63+
app-congTerm′ : ∀ {F G t t′ u u′ Γ l l′}
64+
([F] : Γ ⊩⟨ l′ ⟩ F)
65+
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
66+
([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
67+
([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Π F ▹ G / Π-intr [ΠFG])
68+
([u] : Γ ⊩⟨ l′ ⟩ u ∷ F / [F])
69+
([u′] : Γ ⊩⟨ l′ ⟩ u′ ∷ F / [F])
70+
([u≡u′] : Γ ⊩⟨ l′ ⟩ u ≡ u′ ∷ F / [F])
71+
→ Γ ⊩⟨ l′ ⟩ t ∘ u ≡ t′ ∘ u′ ∷ G [ u ] / [G[u]]
72+
app-congTerm′ {F′} {G′} {t = t} {t′ = t′} {Γ = Γ}
73+
[F] [G[u]] (noemb (Π F G D ⊢F ⊢G A≡A [F]₁ [G] G-ext))
74+
(Πₜ₌ f g [ ⊢t , ⊢f , d ] [ ⊢t′ , ⊢g , d′ ] funcF funcG t≡u
75+
(Πₜ f′ [ _ , ⊢f′ , d″ ] funcF′ f≡f [f] [f]₁)
76+
(Πₜ g′ [ _ , ⊢g′ , d‴ ] funcG′ g≡g [g] [g]₁) [t≡u])
77+
[a] [a′] [a≡a′] =
78+
let [ΠFG] = Π′ F G D ⊢F ⊢G A≡A [F]₁ [G] G-ext
79+
ΠFG≡ΠF′G′ = whnfRed* (red D) Π
80+
F≡F′ , G≡G′ = Π-PE-injectivity ΠFG≡ΠF′G′
81+
f≡f′ = whrDet*Term (d , functionWhnf funcF) (d″ , functionWhnf funcF′)
82+
g≡g′ = whrDet*Term (d′ , functionWhnf funcG) (d‴ , functionWhnf funcG′)
83+
F≡wkidF′ = PE.trans F≡F′ (PE.sym (wk-id _))
84+
t∘x≡wkidt∘x : {a b : Term} → U.wk id a Term.∘ b PE.≡ a ∘ b
85+
t∘x≡wkidt∘x {a} {b} = PE.cong (λ x → x ∘ b) (wk-id a)
86+
t∘x≡wkidt∘x′ : {a : Term} → U.wk id g′ Term.∘ a PE.≡ g ∘ a
87+
t∘x≡wkidt∘x′ {a} = PE.cong (λ x → x ∘ a) (PE.trans (wk-id _) (PE.sym g≡g′))
88+
wkidG₁[u]≡G[u] = PE.cong (λ x → x [ _ ])
89+
(PE.trans (wk-lift-id _) (PE.sym G≡G′))
90+
wkidG₁[u′]≡G[u′] = PE.cong (λ x → x [ _ ])
91+
(PE.trans (wk-lift-id _) (PE.sym G≡G′))
92+
⊢Γ = wf ⊢F
93+
[u]′ = irrelevanceTerm′ F≡wkidF′ [F] ([F]₁ T.id ⊢Γ) [a]
94+
[u′]′ = irrelevanceTerm′ F≡wkidF′ [F] ([F]₁ T.id ⊢Γ) [a′]
95+
[u≡u′]′ = irrelevanceEqTerm′ F≡wkidF′ [F] ([F]₁ T.id ⊢Γ) [a≡a′]
96+
[G[u′]] = irrelevance′ wkidG₁[u′]≡G[u′] ([G] T.id ⊢Γ [u′]′)
97+
[G[u≡u′]] = irrelevanceEq″ wkidG₁[u]≡G[u] wkidG₁[u′]≡G[u′]
98+
([G] T.id ⊢Γ [u]′) [G[u]]
99+
(G-ext T.id ⊢Γ [u]′ [u′]′ [u≡u′]′)
100+
[f′] : Γ ⊩⟨ _ ⟩ f′ ∷ Π F′ ▹ G′ / [ΠFG]
101+
[f′] = Πₜ f′ (idRedTerm:*: ⊢f′) funcF′ f≡f [f] [f]₁
102+
[g′] : Γ ⊩⟨ _ ⟩ g′ ∷ Π F′ ▹ G′ / [ΠFG]
103+
[g′] = Πₜ g′ (idRedTerm:*: ⊢g′) funcG′ g≡g [g] [g]₁
104+
[f∘u] = appTerm [F] [G[u]] [ΠFG]
105+
(irrelevanceTerm″ PE.refl (PE.sym f≡f′) [ΠFG] [ΠFG] [f′])
106+
[a]
107+
[g∘u′] = appTerm [F] [G[u′]] [ΠFG]
108+
(irrelevanceTerm″ PE.refl (PE.sym g≡g′) [ΠFG] [ΠFG] [g′])
109+
[a′]
110+
[tu≡t′u] = irrelevanceEqTerm″ t∘x≡wkidt∘x t∘x≡wkidt∘x wkidG₁[u]≡G[u]
111+
([G] T.id ⊢Γ [u]′) [G[u]]
112+
([t≡u] T.id ⊢Γ [u]′)
113+
[t′u≡t′u′] = irrelevanceEqTerm″ t∘x≡wkidt∘x′ t∘x≡wkidt∘x′ wkidG₁[u]≡G[u]
114+
([G] T.id ⊢Γ [u]′) [G[u]]
115+
([g] T.id ⊢Γ [u]′ [u′]′ [u≡u′]′)
116+
d₁ = PE.subst (λ x → Γ ⊢ t ⇒* f ∷ x) (PE.sym ΠFG≡ΠF′G′) d
117+
d₂ = PE.subst (λ x → Γ ⊢ t′ ⇒* g ∷ x) (PE.sym ΠFG≡ΠF′G′) d′
118+
[tu≡fu] = proj₂ (redSubst*Term (app-subst* d₁ (escapeTerm [F] [a]))
119+
[G[u]] [f∘u])
120+
[gu′≡t′u′] = convEqTerm₂ [G[u]] [G[u′]] [G[u≡u′]]
121+
(symEqTerm [G[u′]]
122+
(proj₂ (redSubst*Term (app-subst* d₂ (escapeTerm [F] [a′]))
123+
[G[u′]] [g∘u′])))
124+
in transEqTerm [G[u]] (transEqTerm [G[u]] [tu≡fu] [tu≡t′u])
125+
(transEqTerm [G[u]] [t′u≡t′u′] [gu′≡t′u′])
126+
app-congTerm′ [F] [G[u]] (emb 0<1 x) [t≡t′] [u] [u′] [u≡u′] =
127+
app-congTerm′ [F] [G[u]] x [t≡t′] [u] [u′] [u≡u′]
128+
129+
-- Application congurence of reducible terms.
130+
app-congTerm : ∀ {F G t t′ u u′ Γ l l′}
131+
([F] : Γ ⊩⟨ l′ ⟩ F)
132+
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
133+
([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
134+
([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Π F ▹ G / [ΠFG])
135+
([u] : Γ ⊩⟨ l′ ⟩ u ∷ F / [F])
136+
([u′] : Γ ⊩⟨ l′ ⟩ u′ ∷ F / [F])
137+
([u≡u′] : Γ ⊩⟨ l′ ⟩ u ≡ u′ ∷ F / [F])
138+
→ Γ ⊩⟨ l′ ⟩ t ∘ u ≡ t′ ∘ u′ ∷ G [ u ] / [G[u]]
139+
app-congTerm [F] [G[u]] [ΠFG] [t≡t′] =
140+
let [t≡t′]′ = irrelevanceEqTerm [ΠFG] (Π-intr (Π-elim [ΠFG])) [t≡t′]
141+
in app-congTerm′ [F] [G[u]] (Π-elim [ΠFG]) [t≡t′]′

‎Definition/LogicalRelation/Substitution/Introductions/Application.agda

Lines changed: 2 additions & 123 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,13 @@ open import Definition.Typed.EqualityRelation
55
module Definition.LogicalRelation.Substitution.Introductions.Application {{eqrel : EqRelSet}} where
66
open EqRelSet {{...}}
77

8-
open import Definition.Untyped hiding (wk)
9-
import Definition.Untyped as U
8+
open import Definition.Untyped
109
open import Definition.Untyped.Properties
1110
open import Definition.Typed
12-
import Definition.Typed.Weakening as T
13-
open import Definition.Typed.Properties
14-
open import Definition.Typed.RedSteps
1511
open import Definition.LogicalRelation
16-
open import Definition.LogicalRelation.EqView
1712
open import Definition.LogicalRelation.Irrelevance
1813
open import Definition.LogicalRelation.Properties
14+
open import Definition.LogicalRelation.Application
1915
open import Definition.LogicalRelation.Substitution
2016
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
2117

@@ -25,123 +21,6 @@ open import Tools.Product
2521
import Tools.PropositionalEquality as PE
2622

2723

28-
-- Helper function for application of specific type derivations.
29-
appTerm′ : ∀ {F G t u Γ l l′ l″}
30-
([F] : Γ ⊩⟨ l″ ⟩ F)
31-
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
32-
([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
33-
([t] : Γ ⊩⟨ l ⟩ t ∷ Π F ▹ G / Π-intr [ΠFG])
34-
([u] : Γ ⊩⟨ l″ ⟩ u ∷ F / [F])
35-
→ Γ ⊩⟨ l′ ⟩ t ∘ u ∷ G [ u ] / [G[u]]
36-
appTerm′ {t = t} {Γ = Γ} [F] [G[u]] (noemb (Π F G D ⊢F ⊢G A≡A [F′] [G′] G-ext))
37-
(Πₜ f d funcF f≡f [f] [f]₁) [u] =
38-
let ΠFG≡ΠF′G′ = whnfRed* (red D) Π
39-
F≡F′ , G≡G′ = Π-PE-injectivity ΠFG≡ΠF′G′
40-
F≡idF′ = PE.trans F≡F′ (PE.sym (wk-id _))
41-
idG′ᵤ≡Gᵤ = PE.cong (λ x → x [ _ ]) (PE.trans (wk-lift-id _) (PE.sym G≡G′))
42-
idf∘u≡f∘u = (PE.cong (λ x → x ∘ _) (wk-id _))
43-
⊢Γ = wf ⊢F
44-
[u]′ = irrelevanceTerm′ F≡idF′ [F] ([F′] T.id ⊢Γ) [u]
45-
[f∘u] = irrelevanceTerm″ idG′ᵤ≡Gᵤ idf∘u≡f∘u
46-
([G′] T.id ⊢Γ [u]′) [G[u]] ([f]₁ T.id ⊢Γ [u]′)
47-
⊢u = escapeTerm [F] [u]
48-
d′ = PE.subst (λ x → Γ ⊢ t ⇒* f ∷ x) (PE.sym ΠFG≡ΠF′G′) (redₜ d)
49-
in proj₁ (redSubst*Term (app-subst* d′ ⊢u) [G[u]] [f∘u])
50-
appTerm′ [F] [G[u]] (emb 0<1 x) [t] [u] = appTerm′ [F] [G[u]] x [t] [u]
51-
52-
-- Application of reducible terms.
53-
appTerm : ∀ {F G t u Γ l l′ l″}
54-
([F] : Γ ⊩⟨ l″ ⟩ F)
55-
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
56-
([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
57-
([t] : Γ ⊩⟨ l ⟩ t ∷ Π F ▹ G / [ΠFG])
58-
([u] : Γ ⊩⟨ l″ ⟩ u ∷ F / [F])
59-
→ Γ ⊩⟨ l′ ⟩ t ∘ u ∷ G [ u ] / [G[u]]
60-
appTerm [F] [G[u]] [ΠFG] [t] [u] =
61-
let [t]′ = irrelevanceTerm [ΠFG] (Π-intr (Π-elim [ΠFG])) [t]
62-
in appTerm′ [F] [G[u]] (Π-elim [ΠFG]) [t]′ [u]
63-
64-
-- Helper function for application congurence of specific type derivations.
65-
app-congTerm′ : ∀ {F G t t′ u u′ Γ l l′}
66-
([F] : Γ ⊩⟨ l′ ⟩ F)
67-
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
68-
([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ▹ G)
69-
([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Π F ▹ G / Π-intr [ΠFG])
70-
([u] : Γ ⊩⟨ l′ ⟩ u ∷ F / [F])
71-
([u′] : Γ ⊩⟨ l′ ⟩ u′ ∷ F / [F])
72-
([u≡u′] : Γ ⊩⟨ l′ ⟩ u ≡ u′ ∷ F / [F])
73-
→ Γ ⊩⟨ l′ ⟩ t ∘ u ≡ t′ ∘ u′ ∷ G [ u ] / [G[u]]
74-
app-congTerm′ {F′} {G′} {t = t} {t′ = t′} {Γ = Γ}
75-
[F] [G[u]] (noemb (Π F G D ⊢F ⊢G A≡A [F]₁ [G] G-ext))
76-
(Πₜ₌ f g [ ⊢t , ⊢f , d ] [ ⊢t′ , ⊢g , d′ ] funcF funcG t≡u
77-
(Πₜ f′ [ _ , ⊢f′ , d″ ] funcF′ f≡f [f] [f]₁)
78-
(Πₜ g′ [ _ , ⊢g′ , d‴ ] funcG′ g≡g [g] [g]₁) [t≡u])
79-
[a] [a′] [a≡a′] =
80-
let [ΠFG] = Π′ F G D ⊢F ⊢G A≡A [F]₁ [G] G-ext
81-
ΠFG≡ΠF′G′ = whnfRed* (red D) Π
82-
F≡F′ , G≡G′ = Π-PE-injectivity ΠFG≡ΠF′G′
83-
f≡f′ = whrDet*Term (d , functionWhnf funcF) (d″ , functionWhnf funcF′)
84-
g≡g′ = whrDet*Term (d′ , functionWhnf funcG) (d‴ , functionWhnf funcG′)
85-
F≡wkidF′ = PE.trans F≡F′ (PE.sym (wk-id _))
86-
t∘x≡wkidt∘x : {a b : Term} → U.wk id a Term.∘ b PE.≡ a ∘ b
87-
t∘x≡wkidt∘x {a} {b} = PE.cong (λ x → x ∘ b) (wk-id a)
88-
t∘x≡wkidt∘x′ : {a : Term} → U.wk id g′ Term.∘ a PE.≡ g ∘ a
89-
t∘x≡wkidt∘x′ {a} = PE.cong (λ x → x ∘ a) (PE.trans (wk-id _) (PE.sym g≡g′))
90-
wkidG₁[u]≡G[u] = PE.cong (λ x → x [ _ ])
91-
(PE.trans (wk-lift-id _) (PE.sym G≡G′))
92-
wkidG₁[u′]≡G[u′] = PE.cong (λ x → x [ _ ])
93-
(PE.trans (wk-lift-id _) (PE.sym G≡G′))
94-
⊢Γ = wf ⊢F
95-
[u]′ = irrelevanceTerm′ F≡wkidF′ [F] ([F]₁ T.id ⊢Γ) [a]
96-
[u′]′ = irrelevanceTerm′ F≡wkidF′ [F] ([F]₁ T.id ⊢Γ) [a′]
97-
[u≡u′]′ = irrelevanceEqTerm′ F≡wkidF′ [F] ([F]₁ T.id ⊢Γ) [a≡a′]
98-
[G[u′]] = irrelevance′ wkidG₁[u′]≡G[u′] ([G] T.id ⊢Γ [u′]′)
99-
[G[u≡u′]] = irrelevanceEq″ wkidG₁[u]≡G[u] wkidG₁[u′]≡G[u′]
100-
([G] T.id ⊢Γ [u]′) [G[u]]
101-
(G-ext T.id ⊢Γ [u]′ [u′]′ [u≡u′]′)
102-
[f′] : Γ ⊩⟨ _ ⟩ f′ ∷ Π F′ ▹ G′ / [ΠFG]
103-
[f′] = Πₜ f′ (idRedTerm:*: ⊢f′) funcF′ f≡f [f] [f]₁
104-
[g′] : Γ ⊩⟨ _ ⟩ g′ ∷ Π F′ ▹ G′ / [ΠFG]
105-
[g′] = Πₜ g′ (idRedTerm:*: ⊢g′) funcG′ g≡g [g] [g]₁
106-
[f∘u] = appTerm [F] [G[u]] [ΠFG]
107-
(irrelevanceTerm″ PE.refl (PE.sym f≡f′) [ΠFG] [ΠFG] [f′])
108-
[a]
109-
[g∘u′] = appTerm [F] [G[u′]] [ΠFG]
110-
(irrelevanceTerm″ PE.refl (PE.sym g≡g′) [ΠFG] [ΠFG] [g′])
111-
[a′]
112-
[tu≡t′u] = irrelevanceEqTerm″ t∘x≡wkidt∘x t∘x≡wkidt∘x wkidG₁[u]≡G[u]
113-
([G] T.id ⊢Γ [u]′) [G[u]]
114-
([t≡u] T.id ⊢Γ [u]′)
115-
[t′u≡t′u′] = irrelevanceEqTerm″ t∘x≡wkidt∘x′ t∘x≡wkidt∘x′ wkidG₁[u]≡G[u]
116-
([G] T.id ⊢Γ [u]′) [G[u]]
117-
([g] T.id ⊢Γ [u]′ [u′]′ [u≡u′]′)
118-
d₁ = PE.subst (λ x → Γ ⊢ t ⇒* f ∷ x) (PE.sym ΠFG≡ΠF′G′) d
119-
d₂ = PE.subst (λ x → Γ ⊢ t′ ⇒* g ∷ x) (PE.sym ΠFG≡ΠF′G′) d′
120-
[tu≡fu] = proj₂ (redSubst*Term (app-subst* d₁ (escapeTerm [F] [a]))
121-
[G[u]] [f∘u])
122-
[gu′≡t′u′] = convEqTerm₂ [G[u]] [G[u′]] [G[u≡u′]]
123-
(symEqTerm [G[u′]]
124-
(proj₂ (redSubst*Term (app-subst* d₂ (escapeTerm [F] [a′]))
125-
[G[u′]] [g∘u′])))
126-
in transEqTerm [G[u]] (transEqTerm [G[u]] [tu≡fu] [tu≡t′u])
127-
(transEqTerm [G[u]] [t′u≡t′u′] [gu′≡t′u′])
128-
app-congTerm′ [F] [G[u]] (emb 0<1 x) [t≡t′] [u] [u′] [u≡u′] =
129-
app-congTerm′ [F] [G[u]] x [t≡t′] [u] [u′] [u≡u′]
130-
131-
-- Application congurence of reducible terms.
132-
app-congTerm : ∀ {F G t t′ u u′ Γ l l′}
133-
([F] : Γ ⊩⟨ l′ ⟩ F)
134-
([G[u]] : Γ ⊩⟨ l′ ⟩ G [ u ])
135-
([ΠFG] : Γ ⊩⟨ l ⟩ Π F ▹ G)
136-
([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ Π F ▹ G / [ΠFG])
137-
([u] : Γ ⊩⟨ l′ ⟩ u ∷ F / [F])
138-
([u′] : Γ ⊩⟨ l′ ⟩ u′ ∷ F / [F])
139-
([u≡u′] : Γ ⊩⟨ l′ ⟩ u ≡ u′ ∷ F / [F])
140-
→ Γ ⊩⟨ l′ ⟩ t ∘ u ≡ t′ ∘ u′ ∷ G [ u ] / [G[u]]
141-
app-congTerm [F] [G[u]] [ΠFG] [t≡t′] =
142-
let [t≡t′]′ = irrelevanceEqTerm [ΠFG] (Π-intr (Π-elim [ΠFG])) [t≡t′]
143-
in app-congTerm′ [F] [G[u]] (Π-elim [ΠFG]) [t≡t′]′
144-
14524
-- Application of valid terms.
14625
appᵛ : ∀ {F G t u Γ l}
14726
([Γ] : ⊩ᵛ Γ)

‎Definition/LogicalRelation/Substitution/Introductions/Lambda.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,10 @@ open import Definition.LogicalRelation.EqView
1616
open import Definition.LogicalRelation.Irrelevance
1717
open import Definition.LogicalRelation.Weakening
1818
open import Definition.LogicalRelation.Properties
19+
open import Definition.LogicalRelation.Application
1920
open import Definition.LogicalRelation.Substitution
2021
open import Definition.LogicalRelation.Substitution.Properties
2122
open import Definition.LogicalRelation.Substitution.Introductions.Pi
22-
open import Definition.LogicalRelation.Substitution.Introductions.Application
2323

2424
open import Tools.Nat
2525
open import Tools.Product

‎Definition/LogicalRelation/Substitution/Introductions/Natrec.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,12 @@ open import Definition.LogicalRelation
1515
open import Definition.LogicalRelation.EqView
1616
open import Definition.LogicalRelation.Irrelevance
1717
open import Definition.LogicalRelation.Properties
18+
open import Definition.LogicalRelation.Application
1819
open import Definition.LogicalRelation.Substitution
1920
open import Definition.LogicalRelation.Substitution.Properties
2021
import Definition.LogicalRelation.Substitution.Irrelevance as S
2122
open import Definition.LogicalRelation.Substitution.Reflexivity
2223
open import Definition.LogicalRelation.Substitution.Weakening
23-
open import Definition.LogicalRelation.Substitution.Introductions.Application
2424
open import Definition.LogicalRelation.Substitution.Introductions.Nat
2525
open import Definition.LogicalRelation.Substitution.Introductions.Pi
2626
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

‎Everything.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ import Definition.LogicalRelation.EqView
3636
import Definition.LogicalRelation.Irrelevance
3737
import Definition.LogicalRelation.Weakening
3838
import Definition.LogicalRelation.Properties
39+
import Definition.LogicalRelation.Application
3940

4041
import Definition.LogicalRelation.Substitution
4142
import Definition.LogicalRelation.Substitution.Properties

‎README.agda

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -105,11 +105,8 @@ import Definition.LogicalRelation.Properties.Neutral
105105
-- Weak head expansion of the logical relation.
106106
import Definition.LogicalRelation.Properties.Reduction
107107

108-
-- Universe introduction in the logical relation.
109-
import Definition.LogicalRelation.Properties.Universe
110-
111-
-- Successor of natural numbers in the logical relation.
112-
import Definition.LogicalRelation.Properties.Successor
108+
-- Application in the logical relation.
109+
import Definition.LogicalRelation.Application
113110

114111
-- Validity judgements definitions
115112
import Definition.LogicalRelation.Substitution
@@ -130,6 +127,11 @@ import Definition.LogicalRelation.Substitution.Properties
130127
-- Single term substitution of validity judgements.
131128
import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
132129

130+
-- The fundamental theorem.
131+
import Definition.LogicalRelation.Fundamental
132+
133+
-- Certain cases of the logical relation:
134+
133135
-- Validity of Π-types.
134136
import Definition.LogicalRelation.Substitution.Introductions.Pi
135137

@@ -142,8 +144,6 @@ import Definition.LogicalRelation.Substitution.Introductions.Lambda
142144
-- Validity of natural recursion of natural numbers.
143145
import Definition.LogicalRelation.Substitution.Introductions.Natrec
144146

145-
-- The fundamental theorem.
146-
import Definition.LogicalRelation.Fundamental
147147

148148
-- Reducibility of well-formedness.
149149
import Definition.LogicalRelation.Fundamental.Reducibility

0 commit comments

Comments
 (0)