CwF.agda

module CwF where

open import Setoid
open EqChain

infixr 30 _⇒_
infixl 50 _/_ _/ˢ_
infixr 45 _◄_
infixl 45 _▷_

Cxt : Set
Cxt = Setoid

_⇒_ : Cxt -> Cxt -> Set
Γ ⇒ Δ = El (Γ ==> Δ)

Type : Cxt -> Set
Type Γ = Fam Γ

_/_ : {Γ Δ : Cxt} -> Type Γ -> (Δ ⇒ Γ) -> Type Δ
A / σ = A ○ σ

lem-/id : {Γ : Cxt}{A : Type Γ} -> A / id == A
lem-/id = lem-○-id

Term : (Γ : Cxt) -> Type Γ -> Set
Term Γ A = El (Π Γ A)

_◄_ : {Γ : Cxt}{A B : Type Γ} -> B == A -> Term Γ A -> Term Γ B
B=A ◄ u = eqΠ refl B=A << u

_/ˢ_ : {Γ Δ : Cxt}{A : Type Γ} -> Term Γ A -> (σ : Δ ⇒ Γ) -> Term Δ (A / σ)
u /ˢ σ = u ∘ σ

_▷_ : (Γ : Cxt) -> Type Γ -> Cxt
Γ ▷ A = Σ Γ A

wk : {Γ : Cxt}(A : Type Γ) -> Γ ▷ A ⇒ Γ
wk A = ƛ fst \ x y x=y -> fst-eq x=y

vz : {Γ : Cxt}(A : Type Γ) -> Term (Γ ▷ A) (A / wk A)
vz A = ƛ snd \ x y x=y -> snd-eq x=y

ext : {Γ Δ : Cxt}(A : Type Γ)(σ : Δ ⇒ Γ)(u : Term Δ (A / σ)) -> Δ ⇒ Γ ▷ A
ext A σ u = ƛ (\x -> (σ # x , u # x))
               \x y x=y -> eqInΣ refl (#-cong-R σ x=y) (#-cong-R u x=y)

lem-/-· : {Γ Δ Θ : Cxt}(A : Type Γ)(σ : Δ ⇒ Γ)(δ : Θ ⇒ Δ) ->
          A / σ · δ == A / σ / δ
lem-/-· A σ δ = eqFam refl \x y x=y ->
  !-cong-R A (sym (cast-id' _ (#-cong-R σ (#-cong-R δ (cast-id' _ (sym x=y)))))) 

lem-wk-∘-ext : {Γ Δ : Cxt}(A : Type Δ)(σ : Γ ⇒ Δ)(u : Term Γ (A / σ)) ->
            wk A ∘ ext A σ u == σ
lem-wk-∘-ext A (ƛ σ pσ) u = eqInΠ refl pσ

lem-vz-/-ext : {Γ Δ : Cxt}(A : Type Δ)(σ : Γ ⇒ Δ)(u : Term Γ (A / σ)) ->
               vz A /ˢ (ext A σ u) == u
lem-vz-/-ext A σ (ƛ u pu) = eqInΠ refl pu

-- (σ , u) ∘ δ == (σ ∘ δ , u / δ)
lem-ext-∘ : {Γ Δ Θ : Cxt}{A : Type Γ}(σ : Δ ⇒ Γ)(δ : Θ ⇒ Δ)(u : Term Δ (A / σ)) ->
            ext A σ u · δ == ext A (σ · δ) (lem-/-· A σ δ ◄ u /ˢ δ)
lem-ext-∘ σ δ u = eqInΠ refl \x y x=y ->
  eqInΣ refl
    (cast-irr _ _ (#-cong-R σ (#-cong-R δ (cast-irr _ _ x=y))))
    (cast-irr _ _ (#-cong-R u (#-cong-R δ (cast-irr _ _ x=y))))

<_> : {Γ : Cxt}{A : Type Γ} -> Term Γ A -> Γ ⇒ Γ ▷ A
< u > = ext _ id (lem-○-id ◄ u)

lift : {Γ Δ : Cxt}(A : Type Γ)(σ : Δ ⇒ Γ) -> Δ ▷ (A / σ) ⇒ Γ ▷ A
lift A σ = ƛ (\x -> σ # fst x , snd x)
              \x y x=y -> eqInΣ refl (#-cong-R σ (fst-eq x=y)) (snd-eq x=y)

curryFam : {A : Setoid}{F : Fam A} -> Fam (Σ A F) -> (x : El A) -> Fam (F ! x)
curryFam G x = fam (\y -> G ! (x , y))
                   \z w z=w -> !-cong-R G (eqInΣ refl refl z=w)

Pi : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A)) -> Type Γ
Pi A B = fam (\x -> Π (A ! x) (curryFam B x))
              \x y x=y ->
                eqΠ (!-cong-R A (sym x=y))
                    (eqFam (!-cong-R A (sym x=y)) \z w z=w ->
                            !-cong-R B (eqInΣ refl x=y z=w)
                    )

lem-Pi-/ : {Γ Δ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))(σ : Δ ⇒ Γ) ->
           Pi A B / σ == Pi (A / σ) (B / lift A σ)
lem-Pi-/ A B σ = eqFam refl \x y x=y ->
  eqΠ (Aσ-eq x=y)
      (eqFam (Aσ-eq x=y) \z w z=w ->
        !-cong-R B (eqInΣ refl (#-cong-R σ x=y) z=w)
      )
  where
    Aσ-eq : forall {x y} -> x == y -> A ! σ # y == A ! σ # x
    Aσ-eq x=y = !-cong-R A (#-cong-R σ (sym x=y))

lam : {Γ : Cxt}{A : Type Γ}{B : Type (Γ ▷ A)} -> Term (Γ ▷ A) B -> Term Γ (Pi A B)
lam {A = A} f =
  ƛ (\γ -> ƛ (\x -> f # (γ , x)) (prf₁ γ)) prf₂
  where
      prf₁ : forall γ x y x=y -> _
      prf₁ = \γ x y x=y -> #-cong-R f (eqInΣ refl refl x=y)

      prf₂ = \x y x=y ->
        eqInΠ (!-cong-R A (sym x=y)) \z w z=w ->
          #-cong-R f (eqInΣ refl x=y z=w)

app : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))
      (v : Term Γ (Pi A B))(u : Term Γ A) -> Term Γ (B / < u >)
app A B v u = ƛ (\γ -> prf₁ γ << v # γ # (u # γ)) prf₂
  where
      lem : forall γ -> < u > # γ == (γ , u # γ)
      lem γ = eqInΣ refl refl (#-cong (lem-○-id ◄ u) u (sym (cast-id _)) refl)

      prf₁ : forall γ -> (B / < u >) ! γ == B ! (γ , u # γ)
      prf₁ γ = !-cong-R B (lem γ)

      prf₂ = \x y x=y -> cast-irr _ _ (#-cong (v # x) (v # y)
                                              (#-cong-R v x=y)
                                              (#-cong-R u x=y)
                                      )

lem-β : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))
        (v : Term (Γ ▷ A) B)(u : Term Γ A) ->
        app A B (lam v) u == v /ˢ < u >
lem-β A B v u = eqInΠ refl \x y x=y ->
  sym (cast-id' _
    (#-cong-R v
      (eqInΣ refl (sym x=y)
        (#-cong (lem-○-id ◄ u) u (sym (cast-id _)) (sym x=y)))
      )
    )

-- The stack blows when trying to prove η.
-- I'm not sure it does anymore, but I have no idea how to prove η,
-- I struggled just giving the type.
-- lem-η : {Γ : Cxt}(A : Type Γ)(B : Type (Γ ▷ A))
--         (v : Term Γ (Pi A B)) →
--         v == lam (app (A / wk A) (B / lift A (wk A)) (sym (lem-Pi-/ A B (wk A)) ◄ v /ˢ wk A) (vz A))
-- lem-η {Γ} A B (ƛ f pf) =
--   eqInΠ =S=-refl λ γ δ γ=δ →
--   proof f γ ≡ ƛ (_#_ (f γ)) (λ _ _ → #-cong-R (f γ)) by η (f γ)
--             ≡ _ by eqInΠ (!-cong-R A (sym γ=δ)) (λ x y x=y →
--     proof f γ # x
--       ≡ (_ << (_ << f (_ << δ))) # y by {!!}
--     qed)
--   qed