module Common.Context where
import Level
open import Data.Nat as Nat
open import Data.List as List
import Level
open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Relation.Binary -- using (Setoid; Rel; IsEquivalence)
open ≡-Reasoning
open import Function as Fun hiding (_∘′_)
open import Data.Sum as Sum hiding ([_,_])
-- open import Categories.Category using (Category)
-- open import Common.SumProperties
-------------------------
---- Type contexts
Ctx : Set → Set
Ctx Ty = List Ty
_↑_ : ∀{U} → Ctx U → U → Ctx U
Γ ↑ a = Γ ++ a ∷ []
-- | De Bruijn variable indexing
data Var {Ty : Set} : (Γ : Ctx Ty) (a : Ty) → Set where
zero : ∀{Γ a} → Var (a ∷ Γ) a
succ : ∀{Γ b} (a : Ty) → (x : Var Γ a) → Var (b ∷ Γ) a
data _≅V_ {Ty} : ∀ {Γ Γ' : Ctx Ty} {a a' : Ty} → Var Γ a → Var Γ' a' → Set where
zero : ∀ {Γ Γ'} {a a'}
→ zero {Γ = Γ} {a} ≅V zero {Γ = Γ'} {a'}
succ : ∀ {Γ Γ'} {a a'}
→ ∀ {x : Var Γ a} {x' : Var Γ' a'} {b b' : Ty}
→ x ≅V x'
→ succ {b = b} a x ≅V succ {b = b'} a' x'
Vrefl : ∀ {Ty} {Γ} {a : Ty} {x : Var Γ a} → x ≅V x
Vrefl {x = zero} = zero
Vrefl {x = succ _ t} = succ Vrefl
Vsym : ∀ {Ty} {Γ Γ'} {a a' : Ty} {x : Var Γ a} {x' : Var Γ' a'}
→ x ≅V x' → x' ≅V x
Vsym zero = zero
Vsym {Ty} (succ [x]) = succ (Vsym [x])
Vtrans : ∀ {Ty} {Γ Γ' Γ''} {a a' a'' : Ty}
{x : Var Γ a} {x' : Var Γ' a'} {x'' : Var Γ'' a''}
→ x ≅V x' → x' ≅V x'' → x ≅V x''
Vtrans zero zero = zero
Vtrans (succ eq) (succ eq') = succ (Vtrans eq eq')
-- Note: makes the equality homogeneous in Γ and a
≅V-setoid : ∀ {Ty} {Γ} {a : Ty} → Setoid _ _
≅V-setoid {Ty} {Γ} {a} = record
{ Carrier = Var Γ a
; _≈_ = _≅V_
; isEquivalence = record
{ refl = Vrefl ; sym = Vsym ; trans = Vtrans }
}
arr : ∀ {Ty} → (Γ Δ : Ctx Ty) → Set
arr {Ty} Γ Δ = ∀ (a : Ty) → Var Γ a → Var Δ a
_►_ = arr
-- _▹_ = arr
infix 4 _≡C_
record _≡C_ {Ty} {Γ Δ : Ctx Ty} (ρ : arr Γ Δ) (γ : arr Γ Δ) : Set where
field
≡C-proof : ∀ {a} {x} → ρ a x ≡ γ a x
open _≡C_
_≈_ = _≡C_
Crefl : ∀ {Ty} {Γ Δ : Ctx Ty} → Reflexive (_≡C_ {Γ = Γ} {Δ})
Crefl = record { ≡C-proof = PE.refl }
Csym : ∀ {Ty} {Γ Δ : Ctx Ty} → Symmetric (_≡C_ {Γ = Γ} {Δ})
Csym p = record { ≡C-proof = PE.sym (≡C-proof p) }
Ctrans : ∀ {Ty} {Γ Δ : Ctx Ty} → Transitive (_≡C_ {Γ = Γ} {Δ})
Ctrans p₁ p₂ = record { ≡C-proof = PE.trans (≡C-proof p₁) (≡C-proof p₂) }
≡C-equiv : ∀ {Ty} {Γ Δ : Ctx Ty} → IsEquivalence (_≡C_ {Γ = Γ} {Δ})
≡C-equiv =
record
{ refl = Crefl
; sym = Csym
; trans = Ctrans
}
≡C-setoid : ∀ {Ty} {Γ Δ : Ctx Ty} → Setoid _ _
≡C-setoid {_} {Γ} {Δ} = record
{ Carrier = arr Γ Δ
; _≈_ = _≡C_
; isEquivalence = ≡C-equiv
}
_∘′_ : ∀ {Ty} {Γ Δ Ξ : Ctx Ty} (ρ : Δ ► Ξ) (γ : Γ ► Δ) → Γ ► Ξ
_∘′_ ρ γ = λ a x → ρ a (γ a x)
_●_ = _∘′_
ctx-id : ∀ {Ty} {Γ : Ctx Ty} → arr Γ Γ
ctx-id = λ _ x → x
comp-resp-≡C : ∀ {Ty} {Γ Δ Ξ : Ctx Ty} {ρ ρ' : arr Δ Ξ} {γ γ' : arr Γ Δ} →
ρ ≡C ρ' → γ ≡C γ' → ρ ∘′ γ ≡C ρ' ∘′ γ'
comp-resp-≡C {_} {Γ} {Δ} {Ξ} {ρ} {ρ'} {γ} {γ'} ρ≡ρ' γ≡γ'
= record { ≡C-proof = p }
where
p : ∀ {a} {x} → (ρ ∘′ γ) a x ≡ (ρ' ∘′ γ') a x
p {a} {x} =
begin
(ρ ∘′ γ) a x
≡⟨ refl ⟩
ρ a (γ a x)
≡⟨ cong (λ u → ρ a u) (≡C-proof γ≡γ') ⟩
ρ a (γ' a x)
≡⟨ ≡C-proof ρ≡ρ' ⟩
ρ' a (γ' a x)
≡⟨ refl ⟩
(ρ' ∘′ γ') a x
∎
{-
-- | Contexts form a category
ctx-cat : Set → Category Level.zero Level.zero Level.zero
ctx-cat Ty = record
{ Obj = Ctx Ty
; _⇒_ = arr
; _≡_ = _≡C_
; _∘_ = _∘′_
; id = ctx-id
; assoc = record { ≡C-proof = refl }
; identityˡ = record { ≡C-proof = refl }
; identityʳ = record { ≡C-proof = refl }
; equiv = ≡C-equiv
; ∘-resp-≡ = comp-resp-≡C
}
-}
-------------------------
---- Coproduct structure on contexts
{-
_⊕_ : Ctx → Ctx → Ctx
Γ₁ ⊕ Γ₂ = Γ₁ ++ Γ₂
in₁ : {Γ₁ Γ₂ : Ctx} → Γ₁ ▹ (Γ₁ ⊕ Γ₂)
in₁ _ zero = zero
in₁ a (succ .a x) = succ a (in₁ a x)
in₂ : {{Γ₁ Γ₂ : Ctx}} → Γ₂ ▹ (Γ₁ ⊕ Γ₂)
in₂ {{[]}} _ x = x
in₂ {{b ∷ Γ₁}} a x = succ a (in₂ a x)
split : {Γ₁ Γ₂ : Ctx} {a : Ty} → Var (Γ₁ ⊕ Γ₂) a → Var Γ₁ a ⊎ Var Γ₂ a
split {[]} {Γ₂} x = inj₂ x
split {a ∷ Γ₁'} {Γ₂} zero = inj₁ zero
split {b ∷ Γ₁'} {Γ₂} {a} (succ .a y) = (Sum.map (succ a) (ctx-id a)) (split {Γ₁'} y)
[_,_] : {Γ₁ Γ₂ Δ : Ctx} (f : Γ₁ ▹ Δ) (g : Γ₂ ▹ Δ)
→ ((Γ₁ ⊕ Γ₂) ▹ Δ)
[_,_] {Γ} {Γ₂} f g a x = ([ f a , g a ]′) (split x)
_-⊕-_ : {Γ Γ₂ Γ' Γ₂' : Ctx} (f : Γ ▹ Γ') (g : Γ₂ ▹ Γ₂')
→ ((Γ ⊕ Γ₂) ▹ (Γ' ⊕ Γ₂'))
_-⊕-_ {Γ} {Γ₂} {Γ'} {Γ₂'} f g = [ in₁ ● f , in₂ {{Γ'}} {{Γ₂'}} ● g ]
succ-distr-lemma : {Γ : Ctx} {a b : Ty} (Γ₂ : Ctx) (x : Var Γ a) →
(in₁ {b ∷ Γ} ● succ {Γ}) a x
≡ (succ {Γ ⊕ Γ₂} ● in₁ {Γ} {Γ₂}) a x
succ-distr-lemma Γ₂ x = refl
split-lemma₁ : {a : Ty} (Γ₁ Γ₂ : Ctx) (x : Var Γ₁ a) →
split {Γ₁} {Γ₂} (in₁ {Γ₁} a x) ≡ inj₁ x
split-lemma₁ (tt ∷ Γ₁) Γ₂ zero = refl
split-lemma₁ (tt ∷ Γ₁) Γ₂ (succ a x) =
begin
split {tt ∷ Γ₁} (in₁ {tt ∷ Γ₁} a (succ a x))
≡⟨ refl ⟩
(Sum.map (succ a) id) (split (in₁ a x))
≡⟨ cong (Sum.map (succ a) id) (split-lemma₁ Γ₁ Γ₂ x) ⟩
(Sum.map (succ a) id) (inj₁ x)
≡⟨ refl ⟩
inj₁ (succ a x)
∎
split-lemma₂ : {a : Ty} (Γ₁ Γ₂ : Ctx) (x : Var Γ₂ a) →
split {Γ₁} {Γ₂} (in₂ a x) ≡ inj₂ x
split-lemma₂ [] Γ₂ x = refl
split-lemma₂ {a} (tt ∷ Γ₁) Γ₂ x =
begin
split {tt ∷ Γ₁} {Γ₂} (in₂ {{tt ∷ Γ₁}} a x)
≡⟨ refl ⟩
Sum.map (succ a) id (split (in₂ {{Γ₁}} a x))
≡⟨ cong (λ u → Sum.map (succ a) id u) (split-lemma₂ Γ₁ Γ₂ x) ⟩
Sum.map (succ a) id (inj₂ x)
≡⟨ refl ⟩
inj₂ x
∎
split-lemma : (Γ₁ Γ₂ : Ctx) (a : Ty) (x : Var (Γ₁ ⊕ Γ₂) a) →
[ in₁ {Γ₁} {Γ₂} a , in₂ a ]′ (split x) ≡ x
split-lemma [] Γ₂ _ x = refl
split-lemma (a ∷ Γ₁) Γ₂ .a zero = refl
split-lemma (b ∷ Γ₁) Γ₂ a (succ .a x) =
begin
[ in₁ {b ∷ Γ₁} a , in₂ {{b ∷ Γ₁}} a ]′ (split (succ a x))
≡⟨ refl ⟩
[ in₁ {b ∷ Γ₁} a , (succ {Γ₁ ⊕ Γ₂} ● in₂ {{Γ₁}} ) a ]′
(Sum.map (succ {Γ₁} a) id (split x))
≡⟨ copair-sum-map-merge {f₁ = Var.succ {Γ₁} {b} a} (split x) ⟩
[ (in₁ {b ∷ Γ₁} ● succ {Γ₁}) a , (succ {Γ₁ ⊕ Γ₂} ● in₂) a ]′ (split x)
≡⟨ copair-cong {f = (in₁ {b ∷ Γ₁} ● succ {Γ₁}) a}
(succ-distr-lemma Γ₂)
(split x) ⟩
[ (succ {Γ₁ ⊕ Γ₂} ● in₁ {Γ₁}) a , (succ {Γ₁ ⊕ Γ₂} ● in₂) a ]′ (split x)
≡⟨ copair-distr {f = in₁ {Γ₁} {Γ₂} a} {h = succ {Γ₁ ⊕ Γ₂} a} (split x)⟩
(Var.succ {Γ₁ ⊕ Γ₂} {b} a ∘ [ in₁ {Γ₁} a , in₂ a ]′) (split x)
≡⟨ cong (succ {Γ₁ ⊕ Γ₂} {b} a) (split-lemma Γ₁ Γ₂ a x) ⟩
succ {Γ₁ ⊕ Γ₂} a x
∎
⊕-is-coprod-arg : ∀{Γ₁ Γ₂ : Ctx} (a : Ty) (x : Var (Γ₁ ⊕ Γ₂) a) →
[ in₁ {Γ₁} {Γ₂} , in₂ ] a x ≡ ctx-id a x
⊕-is-coprod-arg {Γ₁} {Γ₂} = split-lemma Γ₁ Γ₂
⊕-is-coprod : ∀{Γ₁ Γ₂ : Ctx} → [ in₁ {Γ₁} {Γ₂} , in₂ ] ≡C ctx-id
⊕-is-coprod {Γ₁} = {!!}
{-
η-≡ {f₁ = [ in₁ {Γ₁} , in₂ ]}
{f₂ = ctx-id}
(λ (a : Ty) →
η-≡ {f₁ = [ in₁ {Γ₁}, in₂ ] a}
{f₂ = ctx-id a}
(⊕-is-coprod-arg {Γ₁} a)
)
-}
●-distr-copair₁ˡ : ∀{Γ₁ Γ₂ Δ : Ctx}
(h : (Γ₁ ⊕ Γ₂) ▹ Δ) (a : Ty) (x : Var (Γ₁ ⊕ Γ₂) a) →
[ h ● in₁ {Γ₁} {Γ₂} , h ● in₂ {{Γ₁}} {{Γ₂}} ] a x
≡ (h ● [ in₁ {Γ₁} {Γ₂} , in₂ ]) a x
●-distr-copair₁ˡ {Γ₁} {Γ₂} {Δ} h a x =
begin
[ h ● in₁ {Γ₁} , h ● in₂ ] a x
≡⟨ refl ⟩
([ (h ● in₁ {Γ₁}) a , (h ● in₂) a ]′) (split x)
≡⟨ copair-distr {f = in₁ {Γ₁} a} {g = in₂ a} {h = h a} (split x) ⟩
(h ● [ in₁ {Γ₁} , in₂ ]) a x
∎
●-distr-copairˡ : ∀{Γ₁ Γ₂ Δ : Ctx} (h : (Γ₁ ⊕ Γ₂) ▹ Δ) →
[ h ● in₁ {Γ₁} {Γ₂} , h ● in₂ {{Γ₁}} {{Γ₂}} ]
≡ h ● [ in₁ {Γ₁} {Γ₂} , in₂ ]
●-distr-copairˡ {Γ₁} h = {!!}
-- η-≡ (λ a → η-≡ (●-distr-copair₁ˡ {Γ₁} h a))
⊕-is-coprod₁ : ∀{Γ₁ Γ₂ Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ} {h : (Γ₁ ⊕ Γ₂) ▹ Δ} →
h ● in₁ ≡C f → h ● in₂ ≡C g → [ f , g ] ≡C h
⊕-is-coprod₁ {Γ₁} {Γ₂} {Δ} {f} {g} {h} h●in₁≡f h●in₂≡g
= record { ≡C-proof = p }
where
p : ∀ {a} {x} → [ f , g ] a x ≡ h a x
p {a} {x} =
begin
[ f , g ] a x
≡⟨ refl ⟩
([ f a , g a ]′) (split x)
≡⟨ cong (λ u → [ u , g a ]′ (split x)) {!!} ⟩
([ (h ● in₁ {Γ₁}) a , g a ]′) (split x)
≡⟨ {!!} ⟩
h a x
∎
{-
[ h ● in₁ {Γ₁} , g ]
≡⟨ cong (λ u → [ h ● in₁ {Γ₁} , u ]) (sym h●in₂≡g) ⟩
[ h ● in₁ {Γ₁} , h ● in₂ ]
≡⟨ ●-distr-copairˡ {Γ₁} h ⟩
h ● [ in₁ {Γ₁}, in₂ ]
≡⟨ cong (λ u → h ● u) (⊕-is-coprod {Γ₁}) ⟩
h ● ctx-id
≡⟨ refl ⟩
h
-}
commute-in₁-arg : ∀ {Γ₁ Γ₂ Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
(a : Ty) (x : Var Γ₁ a) →
([ f , g ] ● in₁) a x ≡ f a x
commute-in₁-arg _ zero = refl
commute-in₁-arg {b ∷ Γ₁} {Γ₂} {Δ} {f} {g} a (succ .a x) =
begin
([ f , g ] ● in₁ {b ∷ Γ₁}) a (succ {Γ₁} a x)
≡⟨ refl ⟩
[ f , g ] a (succ {Γ₁ ⊕ Γ₂} a (in₁ {Γ₁} a x))
≡⟨ refl ⟩
([ f a , g a ]′) (split (succ {Γ₁ ⊕ Γ₂} a (in₁ {Γ₁} a x)))
≡⟨ refl ⟩
[ f a , g a ]′ ((Sum.map (succ a) id) (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)))
≡⟨ refl ⟩
(([ f a , g a ]′ ∘ (Sum.map (succ a) id)) (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)))
≡⟨ copair-sum-map-merge {f₁ = succ a} (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)) ⟩
([ (f ● succ) a , g a ]′ (split {Γ₁} {Γ₂} (in₁ {Γ₁} a x)))
≡⟨ cong ([ (f ● succ) a , g a ]′) (split-lemma₁ Γ₁ Γ₂ x) ⟩
f a (succ a x)
∎
commute-in₁ : (Γ₁ : Ctx) → (Γ₂ : Ctx) → {Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
→ ([ f , g ] ● in₁) ≡C f
commute-in₁ Γ₁ Γ₂ {Δ} {f} {g} =
record { ≡C-proof = λ {a} {x} → commute-in₁-arg {f = f} {g} a x }
commute-in₂-arg : ∀ {Γ₁ Γ₂ Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
(a : Ty) (x : Var Γ₂ a) →
([ f , g ] ● in₂) a x ≡ g a x
commute-in₂-arg {[]} _ _ = refl
commute-in₂-arg {tt ∷ Γ₁} {Γ₂} {Δ} {f} {g} a x =
begin
([ f , g ] ● in₂ {{tt ∷ Γ₁}} ) a x
≡⟨ refl ⟩
[ f , g ] a ((succ ● in₂) a x)
≡⟨ refl ⟩
[ f a , g a ]′ (split {tt ∷ Γ₁} (succ a (in₂ a x)))
≡⟨ cong (λ u → [ f a , g a ]′ u) {x = split {tt ∷ Γ₁} (succ a (in₂ a x))} refl ⟩
[ f a , g a ]′ ((Sum.map (succ a) id) (split {Γ₁} (in₂ a x)))
≡⟨ cong (λ u → [ f a , g a ]′ (Sum.map (succ a) id u)) (split-lemma₂ Γ₁ Γ₂ x) ⟩
[ f a , g a ]′ ((Sum.map (succ a) id) (inj₂ x))
≡⟨ copair-sum-map-merge {f₁ = succ {Γ₁} a} {f₂ = id} {g₁ = f a} {g₂ = g a} (inj₂ x) ⟩
[ (f ● succ) a , (g ● ctx-id) a ]′ (inj₂ x)
≡⟨ copair-elimʳ {f = (f ● succ) a} {g = (g ● ctx-id) a} x ⟩
g a x
∎
commute-in₂ : (Γ₁ : Ctx) → (Γ₂ : Ctx) → {Δ : Ctx} {f : Γ₁ ▹ Δ} {g : Γ₂ ▹ Δ}
→ ([ f , g ] ● in₂) ≡C g
commute-in₂ Γ₁ Γ₂ {Δ} {f} {g} =
record { ≡C-proof = λ {a} {x} → commute-in₂-arg {f = f} {g} a x }
open import Categories.Object.Coproduct ctx-cat
ctx-coproduct : ∀{Γ₁ Γ₂ : Ctx} → Coproduct Γ₁ Γ₂
ctx-coproduct {Γ₁} {Γ₂} = record
{ A+B = Γ₁ ⊕ Γ₂
; i₁ = in₁
; i₂ = in₂
; [_,_] = [_,_]
; commute₁ = commute-in₁ Γ₁ Γ₂
; commute₂ = commute-in₂ Γ₁ Γ₂
; universal = ⊕-is-coprod₁
}
open import Categories.Object.BinaryCoproducts ctx-cat
ctx-bin-coproducts : BinaryCoproducts
ctx-bin-coproducts = record { coproduct = ctx-coproduct }
open BinaryCoproducts ctx-bin-coproducts
-}