Skip to content

Commit

Permalink
clean up some stuff int the IF files
Browse files Browse the repository at this point in the history
  • Loading branch information
@javra
javra committed Apr 4, 2019
1 parent 20a2935 commit c3a9c0f
Show file tree
Hide file tree
Showing 4 changed files with 46 additions and 43 deletions.
38 changes: 19 additions & 19 deletions IFA.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,40 +6,40 @@ open import IF

_ᵃS : ∀{ℓ} → TyS → Set (suc ℓ)
_ᵃS {ℓ} U = Set ℓ
_ᵃS {ℓ} (Π̂S T A) = (α : T) → _ᵃS {ℓ} (A α)
_ᵃS {ℓ} (Π̂S T B) = (τ : T) → _ᵃS {ℓ} (B τ)

_ᵃc : ∀{ℓ} → SCon → Set (suc ℓ)
∙c ᵃc = Lift _ ⊤
_ᵃc {ℓ} (Γ ▶c A) = (_ᵃc {ℓ} Γ) × _ᵃS {ℓ} A
∙c ᵃc = Lift _ ⊤
_ᵃc {ℓ} (Γc ▶c B) = (_ᵃc {ℓ} Γc) × _ᵃS {ℓ} B

_ᵃt : ∀{ℓ}{Γ : SCon}{A : TyS} → Tm Γ A → _ᵃc {ℓ} Γ → _ᵃS {ℓ} A
_ᵃt : ∀{ℓ Γc B} → Tm Γc B → _ᵃc {ℓ} Γc → _ᵃS {ℓ} B
(var vvz ᵃt) (γ , α) = α
(var (vvs t) ᵃt) (γ , α) = (var t ᵃt) γ
((t $S α) ᵃt) γ = (t ᵃt) γ α

_ᵃP : ∀{ℓ}{Γc} → TyP Γc → (γ : _ᵃc {ℓ} Γc) → Set ℓ
(Π̂P T A ᵃP) γ = (α : T) → ((A α) ᵃP) γ
(El a ᵃP) γ = (a ᵃt) γ
((a ⇒P B) ᵃP) γ = (a ᵃt) γ → (B ᵃP) γ
_ᵃP : ∀{ℓ Γc} → TyP Γc → _ᵃc {ℓ} Γc → Set ℓ
(El a ᵃP) γ = (a ᵃt) γ
(Π̂P T A ᵃP) γ = (τ : T) → ((A τ) ᵃP) γ
((a ⇒P A) ᵃP) γ = (a ᵃt) γ → (A ᵃP) γ

_ᵃC : ∀{ℓ}{Γc} → Con Γc → _ᵃc {ℓ} Γc → Set (suc ℓ)
(∙ ᵃC) γ = Lift _ ⊤
((Γ ▶P A) ᵃC) γ = (Γ ᵃC) γ × (A ᵃP) γ
_ᵃC : ∀{ℓ Γc} → Con Γc → _ᵃc {ℓ} Γc → Set (suc ℓ)
(∙ ᵃC) γ = Lift _ ⊤
((Γ ▶P A) ᵃC) γ = (Γ ᵃC) γ × (A ᵃP) γ

_ᵃs : ∀{ℓ}{Γc Δc} → Sub Γc Δc → _ᵃc {ℓ} Γc → _ᵃc {ℓ} Δc
(ε ᵃs) γ = lift tt
((σ , t) ᵃs) γ = (σ ᵃs) γ , (t ᵃt) γ

[]Tᵃ : ∀{ℓ}{Γc Δc A}{δ : Sub Γc Δc} → (γc : _ᵃc {ℓ} Γc) → ((A [ δ ]T) ᵃP) γc ≡ (A ᵃP) ((δ ᵃs) γc)
[]tᵃ : ∀{ℓ}{Γc Δc A}{a : Tm Δc A}{δ : Sub Γc Δc} → (γc : _ᵃc {ℓ} Γc) → ((a [ δ ]t) ᵃt) γc ≡ (a ᵃt) ((δ ᵃs) γc)
[]Tᵃ : ∀{ℓ Γc Δc A}{σ : Sub Γc Δc} → (γc : _ᵃc {ℓ} Γc) → ((A [ σ ]T) ᵃP) γc ≡ (A ᵃP) ((σ ᵃs) γc)
[]tᵃ : ∀{ℓ Γc Δc B}{t : Tm Δc B}{σ : Sub Γc Δc} → (γc : _ᵃc {ℓ} Γc) → ((t [ σ ]t) ᵃt) γc ≡ (t ᵃt) ((σ ᵃs) γc)

[]Tᵃ {A = Π̂P T x} γc = Π≡ refl λ α → []Tᵃ {A = x α} γc
[]Tᵃ {A = El x} γc = []tᵃ {a = x} γc
[]Tᵃ {A = x ⇒P A} γc = Π≡ ([]tᵃ {a = x} γc) λ α → []Tᵃ {A = A} γc
[]Tᵃ {A = El a} γc = []tᵃ {t = a} γc
[]Tᵃ {A = Π̂P T A} γc = Π≡ refl λ τ → []Tᵃ {A = A τ} γc
[]Tᵃ {A = a ⇒P A} γc = Π≡ ([]tᵃ {t = a} γc) λ α → []Tᵃ {A = A} γc

[]tᵃ {a = var vvz} {δ , x} γc = refl
[]tᵃ {a = var (vvs a)}{δ , x} γc = []tᵃ {a = var a} γc
[]tᵃ {a = a $S α} {δ} γc = happly ([]tᵃ {a = a} {δ = δ} γc) α
[]tᵃ {t = var vvz} {σ , x} γc = refl
[]tᵃ {t = var (vvs a)}{σ , x} γc = []tᵃ {t = var a} γc
[]tᵃ {t = t $S α} {σ} γc = happly ([]tᵃ {t = t} γc) α
{-# REWRITE []Tᵃ #-}
{-# REWRITE []tᵃ #-}

Expand Down
31 changes: 17 additions & 14 deletions IFD.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,32 +7,33 @@ open import IFA

ᵈS : ∀{ℓ' ℓ}(B : TyS)(α : _ᵃS {ℓ} B) → Set (suc ℓ' ⊔ ℓ)
ᵈS {ℓ'} U α = α → Set ℓ'
ᵈS {ℓ'} (Π̂S T B) π = (x : T) → ᵈS {ℓ'} (B x) (π x)
ᵈS {ℓ'} (Π̂S T B) π = (τ : T) → ᵈS {ℓ'} (B τ) (π τ)

ᵈc : ∀{ℓ' ℓ}(Γc : SCon)(γc : _ᵃc {ℓ} Γc) → Set (suc ℓ' ⊔ ℓ)
ᵈc ∙c γc = Lift _ ⊤
ᵈc {ℓ'} (Γc ▶c B) (γc , α) = ᵈc {ℓ'} Γc γc × ᵈS {ℓ'} B α

ᵈt : ∀{ℓ'}{ℓ}{Γc : SCon}{B : TyS}(t : Tm Γc B)(γc : _ᵃc {ℓ} Γc) → ᵈc {ℓ'} Γc γc → ᵈS {ℓ'} B ((t ᵃt) γc)
ᵈt (var vvz) (γc , α) (γcᵈ , αᵈ) = αᵈ
ᵈt (var (vvs t)) (γc , α) (γcᵈ , αᴾ) = ᵈt (var t) γc γcᵈ
ᵈt (t $S α) γc γcᵈ = ᵈt t γc γcᵈ α
ᵈt : ∀{ℓ' ℓ Γc B}(t : Tm Γc B){γc : _ᵃc {ℓ} Γc} → ᵈc {ℓ'} Γc γc → ᵈS {ℓ'} B ((t ᵃt) γc)
ᵈt (var vvz) (γcᵈ , αᵈ) = αᵈ
ᵈt (var (vvs t)) (γcᵈ , αᵈ) = ᵈt (var t) γcᵈ
ᵈt (t $S α) γcᵈ = ᵈt t γcᵈ α

ᵈP : ∀{ℓ' ℓ}{Γc}(A : TyP Γc){γc : _ᵃc {ℓ} Γc}(γcᵈ : ᵈc {ℓ'} Γc γc)(α : (A ᵃP) γc) → Set (ℓ' ⊔ ℓ)
ᵈP {ℓ'} (Π̂P T B) γcᵈ π = (α : T) → ᵈP {ℓ'} (B α) γcᵈ (π α)
ᵈP {ℓ'}{ℓ} (El a) {γc} γcᵈ α = Lift (ℓ' ⊔ ℓ) (ᵈt a γc γcᵈ α)
ᵈP {ℓ'} (t ⇒P A) {γc} γcᵈ π = (α : (t ᵃt) γc) (αᵈ : ᵈt t γc γcᵈ α) → ᵈP A γcᵈ (π α)
ᵈP {ℓ'}{ℓ} (El a) γcᵈ α = Lift (ℓ' ⊔ ℓ) (ᵈt a γcᵈ α)
ᵈP {ℓ'} (Π̂P T A) γcᵈ π = (τ : T) → ᵈP {ℓ'} (A τ) γcᵈ (π τ)
ᵈP {ℓ'} (a ⇒P A) γcᵈ π = (α : (a ᵃt) _) (αᵈ : ᵈt a γcᵈ α) → ᵈP A γcᵈ (π α)

ᵈC : ∀{ℓ' ℓ}{Γc}(Γ : Con Γc){γc : _ᵃc {ℓ} Γc}(γcᵈ : ᵈc {ℓ'} Γc γc)(γ : (Γ ᵃC) γc) → Set (suc ℓ' ⊔ ℓ)
ᵈC ∙ γcᵈ γ = Lift _ ⊤
ᵈC {ℓ'} (Γ ▶P A) γcᵈ (γ , α) = (ᵈC Γ γcᵈ γ) × (ᵈP A γcᵈ α)
ᵈC ∙ γcᵈ γ = Lift _ ⊤
ᵈC (Γ ▶P A) γcᵈ (γ , α) = (ᵈC Γ γcᵈ γ) × (ᵈP A γcᵈ α)

ᵈs : ∀{ℓ' ℓ Γc Δc}(σ : Sub Γc Δc)(γc : _ᵃc {ℓ} Γc) → ᵈc {ℓ'} Γc γc → ᵈc {ℓ'} Δc ((σ ᵃs) γc)
ᵈs ε γc γcᵈ = lift tt
ᵈs (σ , t) γc γcᵈ = ᵈs σ γc γcᵈ , ᵈt t γc γcᵈ
ᵈs (σ , t) γc γcᵈ = ᵈs σ γc γcᵈ , ᵈt t γcᵈ

[]Tᵈ : ∀{ℓ' ℓ Γc Δc A}{σ : Sub Γc Δc}{γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc}(α : _) → ᵈP (A [ σ ]T) γcᵈ α ≡ ᵈP A (ᵈs σ γc γcᵈ) α
[]tᵈ : ∀{ℓ' ℓ Γc Δc A}{a : Tm Δc A}{σ : Sub Γc Δc}{γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc} → ᵈt (a [ σ ]t) γc γcᵈ ≡ ᵈt a ((σ ᵃs) γc) (ᵈs σ γc γcᵈ)
[]tᵈ : ∀{ℓ' ℓ Γc Δc A}{a : Tm Δc A}{σ : Sub Γc Δc}{γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc}
→ ᵈt (a [ σ ]t) γcᵈ ≡ ᵈt a (ᵈs σ γc γcᵈ)

[]Tᵈ {A = Π̂P T x} π = Π≡ refl λ α → []Tᵈ {A = x α} (π α)
[]Tᵈ {A = El a} α = Lift _ & happly ([]tᵈ {a = a}) α
Expand All @@ -44,7 +45,8 @@ open import IFA
{-# REWRITE []Tᵈ #-}
{-# REWRITE []tᵈ #-}

vs,ᵈ : ∀{ℓ' ℓ Γc B B'}{x : Tm Γc B}{γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc}{α}{αᵈ : ᵈS {ℓ'}{ℓ} B' α} → ᵈt (vs x) (γc , α) (γcᵈ , αᵈ) ≡ ᵈt x γc γcᵈ
vs,ᵈ : ∀{ℓ' ℓ Γc B B'}{x : Tm Γc B}{γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc}{α}{αᵈ : ᵈS {ℓ'}{ℓ} B' α}
→ ᵈt (vs x) (γcᵈ , αᵈ) ≡ ᵈt x γcᵈ
vs,ᵈ {x = var x} = refl
vs,ᵈ {x = x $S α} = happly (vs,ᵈ {x = x}) α
{-# REWRITE vs,ᵈ #-}
Expand All @@ -68,7 +70,8 @@ idᵈ {Γc = Γc ▶c x} = ,≡ idᵈ refl
π₁ᵈ {σ = σ , x} = refl
{-# REWRITE π₁ᵈ #-}

π₂ᵈ : ∀{ℓ' ℓ Γc Δc A}{σ : Sub Γc (Δc ▶c A)}{γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc} → ᵈt (π₂ σ) γc γcᵈ ≡ ₂ (ᵈs σ γc γcᵈ)
π₂ᵈ : ∀{ℓ' ℓ Γc Δc A}{σ : Sub Γc (Δc ▶c A)}{γc}{γcᵈ : ᵈc {ℓ'}{ℓ} Γc γc}
→ ᵈt (π₂ σ) γcᵈ ≡ ₂ (ᵈs σ γc γcᵈ)
π₂ᵈ {σ = σ , x} = refl
{-# REWRITE π₂ᵈ #-}

Expand Down
17 changes: 9 additions & 8 deletions IFS.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,27 +6,28 @@ open import IF
open import IFA
open import IFD

ˢS : ∀{ℓ' ℓ}(B : TyS)(α : _ᵃS {ℓ} B) → ᵈS {ℓ'} B α → Set (ℓ' ⊔ ℓ)
ˢS U T Tᵈ = (α : T) → Tᵈ α
ˢS (Π̂S T B) π πᵈ = (α : T) → ˢS (B α) (π α) (πᵈ α)
ˢS : ∀{ℓ' ℓ}(B : TyS){α : _ᵃS {ℓ} B} → ᵈS {ℓ'} B α → Set (ℓ' ⊔ ℓ)
ˢS U {α} αᵈ = (x : α) → αᵈ x
ˢS (Π̂S T B) πᵈ = (τ : T) → ˢS (B τ) (πᵈ τ)

ˢc : ∀{ℓ' ℓ}(Γc : SCon){γc : _ᵃc {ℓ} Γc} → ᵈc {ℓ'} Γc γc → Set (ℓ' ⊔ ℓ)
ˢc ∙c γcᵈ = Lift _ ⊤
ˢc (Γc ▶c B) (γcᵈ , αcᵈ) = ˢc Γc γcᵈ × ˢS B _ αcᵈ
ˢc (Γc ▶c B) (γcᵈ , αcᵈ) = ˢc Γc γcᵈ × ˢS B αcᵈ

ˢt : ∀{ℓ' ℓ}{Γc : SCon}{B : TyS}(t : Tm Γc B){γc : _ᵃc {ℓ} Γc}{γcᵈ : ᵈc {ℓ'} Γc γc}(γcˢ : ˢc Γc γcᵈ) → ˢS B ((t ᵃt) γc) (ᵈt t γc γcᵈ)
ˢt : ∀{ℓ' ℓ}{Γc : SCon}{B : TyS}(t : Tm Γc B){γc : _ᵃc {ℓ} Γc}{γcᵈ : ᵈc {ℓ'} Γc γc}(γcˢ : ˢc Γc γcᵈ)
→ ˢS B (ᵈt t γcᵈ)
ˢt (var vvz) (γcˢ , αcˢ) = αcˢ
ˢt (var (vvs t)) (γcˢ , αcˢ) = ˢt (var t) γcˢ
ˢt (t $S α) γcˢ = ˢt t γcˢ α

ˢP : ∀{ℓ' ℓ}{Γc : SCon}(A : TyP Γc){γc : _ᵃc {ℓ} Γc}{γcᵈ : ᵈc {ℓ'} Γc γc}(γcˢ : ˢc Γc γcᵈ)(α : (A ᵃP) γc)(αᵈ : ᵈP A γcᵈ α) → Set (ℓ' ⊔ ℓ)
ˢP (Π̂P T A) γcˢ π πᵈ = (α : T) → ˢP (A α) γcˢ (π α) (πᵈ α)
ˢP (Π̂P T A) γcˢ π πᵈ = (τ : T) → ˢP (A τ) γcˢ (π τ) (πᵈ τ)
ˢP (El a) γcˢ α αᵈ = lift (ˢt a γcˢ α) ≡ αᵈ
ˢP (t ⇒P A) {γc} γcˢ α αᵈ = (x : (t ᵃt) γc) → ˢP A γcˢ (α x) (αᵈ x (ˢt t γcˢ x))

ˢC : ∀{ℓ' ℓ}{Γc}(Γ : Con Γc){γc : _ᵃc {ℓ} Γc}{γcᵈ : ᵈc {ℓ'} Γc γc}(γcˢ : ˢc Γc γcᵈ){γ : (Γ ᵃC) γc}(γᵈ : ᵈC Γ γcᵈ γ) → Set (suc ℓ' ⊔ ℓ)
ˢC ∙ γcˢ γᵈ = Lift _ ⊤
ˢC (Γ ▶P A) γcˢ (γᵈ , αᵈ) = Σ (ˢC Γ γcˢ γᵈ) λ γˢ → ˢP A γcˢ _ αᵈ
ˢC ∙ γcˢ γᵈ = Lift _ ⊤
ˢC (Γ ▶P A) γcˢ (γᵈ , αᵈ) = Σ (ˢC Γ γcˢ γᵈ) λ γˢ → ˢP A γcˢ _ αᵈ

ˢs : ∀{ℓ' ℓ}{Γc Δc}(σ : Sub Γc Δc){γc : _ᵃc {ℓ} Γc}(γcᵈ : ᵈc {ℓ'} Γc γc) → ˢc Γc γcᵈ → ˢc Δc (ᵈs σ γc γcᵈ)
ˢs ε γcᵈ γcˢ = lift tt
Expand Down
3 changes: 1 addition & 2 deletions II2IF.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,9 @@ open import EWRSg
open import IFA
open import IFD
open import IFS
open import IFEx using (concᵃ; conᵃ)

module II2IF
(concᵃ : ∀{ℓ}{Δc}(Δ : s.Con Δc) → _ᵃc {ℓ} Δc)
(conᵃ : ∀{ℓ}{Δc}(Δ : s.Con Δc) → _ᵃC {ℓ} Δ (concᵃ Δ))
(elimcᵃ : ∀{ℓ ℓ'}{Δc}(Δ : s.Con Δc){δcᵈ}(δᵈ : ᵈC {ℓ'} Δ δcᵈ (conᵃ {ℓ} Δ)) → ˢc Δc δcᵈ)
(elimᵃ : ∀{ℓ ℓ'}{Δc}(Δ : s.Con Δc){δcᵈ}(δᵈ : ᵈC {ℓ'} Δ δcᵈ (conᵃ {ℓ} Δ)) → ˢC Δ (elimcᵃ Δ δᵈ) δᵈ) where

Expand Down

0 comments on commit c3a9c0f

Please sign in to comment.