bobatkey/cont-cwf.agda

## cont-cwf.agda
{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; cong; cong-app; subst)
open Eq.≡-Reasoning -- using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Axiom.Extensionality.Propositional
open import Level using (0ℓ)

postulate
  fext : Extensionality 0ℓ 0ℓ

----------------------------------------------------------------------
-- Sum types as pairs
data is-false : Bool -> Set where
  false : is-false false

data is-true : Bool -> Set where
  true : is-true true

Ch : (A B : Set) -> Bool -> Set
Ch A B false = A
Ch A B true  = B

_⊎_ : (A B : Set) → Set
A ⊎ B = Σ Bool (Ch A B)

⊎-map' : ∀ {A B C D} → (x : A ⊎ C) -> (is-false (fst x) -> A -> B) -> (is-true (fst x) -> C -> D) → B ⊎ D
⊎-map' x f g .fst = fst x
⊎-map' (false , a) f g .snd = f false a
⊎-map' (true , c) f g .snd = g true c

⊎-map'-fusion : ∀ {A B C D E F} ->
  (x : A ⊎ D) ->
  (f : is-false (fst x) -> B -> C) -> (f' : is-false (fst x) -> A -> B) ->
  (g : is-true (fst x) -> E -> F) -> (g' : is-true (fst x) -> D -> E) ->
  ⊎-map' (⊎-map' x f' g') f g ≡ ⊎-map' x (λ p x → f p (f' p x)) (λ p x → g p (g' p x))
⊎-map'-fusion (false , a) f f' g g' = refl
⊎-map'-fusion (true , a) f f' g g' = refl

{-# REWRITE ⊎-map'-fusion #-}

get-left : ∀{X Y} → (s : X ⊎ Y) → is-false (fst s) → X
get-left{X}{Y} (false , x) false = x

get-left-comm : ∀{X Y X' Y'} → (s : X ⊎ Y) → (x : is-false (fst s)) → (f : is-false (fst s) → X → X') → (g : is-true (fst s) → Y → Y') → get-left (⊎-map' s f g) x ≡ f x (get-left s x)
get-left-comm (false , snd₁) false f g = refl

⊎-map-getleft : ∀ {X Y} → (s : X ⊎ Y) → ⊎-map' s (λ p x → get-left s p) (λ p x → x) ≡ s
⊎-map-getleft (false , _) = refl
⊎-map-getleft (true , _)  = refl

{-# REWRITE ⊎-map-getleft #-}

⊎-case : ∀ {A B C : Set} → (x : A ⊎ B) → (is-false (fst x) -> A -> C) -> (is-true (fst x) -> B -> C) -> C
⊎-case (false , a) f g = f false a
⊎-case (true , b) f g = g true b

-- ⊎-map-case-fusion : ∀ {A B C D E} ->
--   (x : A ⊎ D) ->
--   (f : is-false (fst x) -> B -> C) -> (f' : is-false (fst x) -> A -> B) ->
--   (g : is-true (fst x) -> E -> C) -> (g' : is-true (fst x) -> D -> E) ->
--   ⊎-case (⊎-map' x f' g') f g ≡ ⊎-case x (λ p x → f p (f' p x)) (λ p x → g p (g' p x))
-- ⊎-map-case-fusion (false , a) f f' g g' = refl
-- ⊎-map-case-fusion (true , d) f f' g g' = refl

-- {-# REWRITE ⊎-map-case-fusion #-}

-- ⊎-case-id : ∀ {X Y} (s : X ⊎ Y) → ⊎-case s (λ _ x → false , x) (λ _ y → true , y) ≡ s
-- ⊎-case-id (false , _) = refl
-- ⊎-case-id (true , _) = refl

-- -- {-# REWRITE ⊎-case-id #-}

----------------------------------------------------------------------
record Cont : Set₁ where
  constructor _,_
  field
    q : Set
    r : q -> Set
open Cont

----------------------------------------------------------------------
record _==>_ (Γ Δ : Cont) : Set₁ where
  constructor _,_
  field
    mor : q Γ -> q Δ
    rom : (γ : q Γ) -> r Δ (mor γ) -> r Γ γ
open _==>_

record _≡mor_ {Γ Δ} (f g : Γ ==> Δ) : Set where
  field
    mor≡ : (γ : q Γ) → mor f γ ≡ mor g γ
    rom≡ : (γ : q Γ) → (δ- : r Δ (mor f γ)) → rom f γ δ- ≡ rom g γ (subst (r Δ) (mor≡ γ) δ-)
open _≡mor_

herlp : ∀ {X : Set}{X- : X → Set}
          {Y : X → Set} {Y- : (x : X) → Y x → Set} →
        (m : (x : X) → Y x) →
        (r₁ : (x : X) -> Y- x (m x) -> X- x) →
        (r₂ : (x : X) -> Y- x (m x) -> X- x) →
        (e₁ : (x : X) → m x ≡ m x) →
        (e₂ : (x : X) → (y- : Y- x (m x)) → r₁ x y- ≡ r₂ x (subst (Y- x) (e₁ x) y-)) →
        (x : X) → (y- : Y- x (m x)) → r₁ x y- ≡ r₂ x y-
herlp m r₁ r₂ e₁ e₂ x y- with e₂ x y-
... | e with e₁ x
... | refl = e

≡mor→≡ : ∀ {Γ Δ} {f g : Γ ==> Δ} → f ≡mor g → f ≡ g
≡mor→≡ {Γ}{Δ} {mor₁ , rom₁} {mor₂ , rom₂} f≡g with fext (f≡g .mor≡)
... | refl = cong (λ x → mor₁ , x)
                  (fext λ γ →
                   fext λ δ- →
                   herlp mor₁ rom₁ rom₂ (f≡g .mor≡) (f≡g .rom≡) γ δ-)

id : ∀ {Γ} → Γ ==> Γ
id .mor = λ γ → γ
id .rom = λ _ γ → γ

_∘_ : ∀{A B C} → B ==> C → A ==> B → A ==> C
(f ∘ g) .mor = λ a → mor f (mor g a)
(f ∘ g) .rom = λ a y → rom g a (rom f (mor g a) y)

infixl 30 _∘_

module category-laws where

  id-comp : ∀ A B → (f : A ==> B) → id ∘ f ≡ f
  id-comp A B f = refl

  comp-id : ∀ A B → (f : A ==> B) → f ∘ id ≡ f
  comp-id A B f = refl

  comp-assoc : ∀ A B C D → (f : C ==> D)(g : B ==> C)(h : A ==> B) ->
      (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)
  comp-assoc A B C D f g h = refl

----------------------------------------------------------------------
-- Terminal object, representing the empty context

ε : Cont
q ε = ⊤
r ε = λ _ → ⊥

! : ∀ A → A ==> ε
mor (! A) _ = tt

!-unique : ∀ A -> (h : A ==> ε) -> h ≡mor ! A
mor≡ (!-unique A h) γ = refl

----------------------------------------------------------------------
-- Types

record Ty (Γ : Cont) : Set₁ where
  field
    q : q Γ → Set
    r : (γ : Cont.q Γ) → q γ → Set
open Ty

-- The direct definition is `Ty Γ = q Γ → Cont`, but this doesn't work
-- well with unification for solving metavariables.

_[_] : ∀{ Γ Δ } → Ty Δ → Γ ==> Δ → Ty Γ
q (S [ f ]) γ   = q S (mor f γ)
r (S [ f ]) γ s = r S (mor f γ) s

infixr 30 _[_]

Ty-subst-id : ∀ {Γ} {S : Ty Γ} → S [ id ] ≡ S
Ty-subst-id = refl

Ty-subst-comp : ∀ {Γ Δ Θ} {S : Ty Θ} → (f : Γ ==> Δ) → (g : Δ ==> Θ) → S [ g ∘ f ] ≡ S [ g ] [ f ]
Ty-subst-comp f g = refl

----------------------------------------------------------------------
-- Terms

record Tm (Γ : Cont) (S : Ty Γ) : Set where
  field
    mor : (γ : q Γ) → q S γ
    rom : (γ : q Γ) → r S γ (mor γ) → r Γ γ
open Tm

_<_> : ∀ { Γ Δ S } → Tm Δ S → (f : Γ ==> Δ) → Tm Γ (S [ f ])
(M < f >) .mor γ    = mor M (mor f γ)
(M < f >) .rom γ s- = rom f γ (rom M (mor f γ) s-)

infixr 30 _<_>

Tm-subst-id : ∀ {Γ} {S} {M : Tm Γ S} → M < id > ≡ M
Tm-subst-id = refl

Tm-subst-comp : ∀ {Γ Δ Θ} {S : Ty Θ} {M : Tm Θ S} → (f : Γ ==> Δ) → (g : Δ ==> Θ) → M < g ∘ f > ≡ M < g > < f >
Tm-subst-comp f g = refl


record _≡Tm_ {Γ S} (M N : Tm Γ S) : Set where
  field
    mor≡ : (γ : q Γ) → mor M γ ≡ mor N γ
    rom≡ : (γ : q Γ) → (s- : r S γ (mor M γ)) → rom M γ s- ≡ rom N γ (subst (r S γ) (mor≡ γ) s-)
open _≡Tm_

≡Tm→≡ : ∀ {Γ S} {M N : Tm Γ S} → M ≡Tm N → M ≡ N
≡Tm→≡{Γ}{S}{M}{N} M≡N with fext (M≡N .mor≡)
... | refl = cong (λ x → record { mor = mor N; rom = x })
                  (fext λ γ → fext λ s- → herlp (mor N) (rom M) (rom N) (mor≡ M≡N) (rom≡ M≡N) γ s-)

≡Tm-cong1 : ∀ { Γ Δ S } → {M N : Tm Δ S} → (f : Γ ==> Δ) → M ≡Tm N → (M < f > ≡Tm N < f > )
≡Tm-cong1 f e .mor≡ γ = e .mor≡ (mor f γ)
≡Tm-cong1 f e .rom≡ γ s- = cong (rom f γ) (e .rom≡ (mor f γ) s-)

----------------------------------------------------------------------
-- Comprehension

_,-_ : (Γ : Cont) → Ty Γ → Cont
q (Γ ,- S)         = Σ (q Γ) λ γ → q S γ
r (Γ ,- S) (γ , s) = r Γ γ ⊎ r S γ s

π₁ : ∀ { Γ S } → (Γ ,- S) ==> Γ
mor π₁ γs    = fst γs
rom π₁ γs γ- = false , γ-

var : ∀ { Γ S } → Tm (Γ ,- S) (S [ π₁ ])
mor var γs    = snd γs
rom var γs s- = true , s-

_,=_ : ∀ { Δ Γ S } → (f : Δ ==> Γ) → Tm Δ (S [ f ]) → Δ ==> (Γ ,- S)
(f ,= M) .mor δ = mor f δ , mor M δ
(f ,= M) .rom δ x = ⊎-case x (λ _ → rom f δ) (λ _ → rom M δ)

infixl 20 _,-_
infixl 20 _,=_

-- Shift a type up by one
_⁺ : ∀ {Γ S} → Ty Γ → Ty (Γ ,- S)
_⁺ T = T [ π₁ ]

-- Shift a term up by one
_⁺ᵗᵐ : ∀ {Γ S T} → Tm Γ T → Tm (Γ ,- S) (T ⁺)
_⁺ᵗᵐ M = M < π₁ >

infixr 30 _⁺
infixr 30 _⁺ᵗᵐ

-- Substitute a single term
↓ : ∀ {Γ S} → Tm Γ S → Γ ==> (Γ ,- S)
↓ M = id ,= M

-- weaken a morphism
wk : ∀ {Γ Δ S} → (f : Γ ==> Δ) → (Γ ,- S [ f ]) ==> (Δ ,- S)
-- wk f = f ∘ π₁ ,= var
wk f .mor (γ , s) = mor f γ , s
wk f .rom (γ , s) δs- = ⊎-map' δs- (λ _ → rom f γ) (λ _ s- → s-)

pair-π-var : ∀ {Γ S} → (π₁ ,= var) ≡mor (id{Γ ,- S})
pair-π-var .mor≡ γ              = refl
pair-π-var .rom≡ γ (false , γ-) = refl
pair-π-var .rom≡ γ (true , s-)  = refl

π-pair : ∀ {Γ Δ S} → (f : Δ ==> Γ) → (M : Tm Δ (S [ f ])) → π₁{Γ}{S} ∘ (f ,= M) ≡mor f
π-pair f M .mor≡ γ    = refl
π-pair f M .rom≡ γ δ- = refl

-- needs π-pair to type check, luckily π-pair holds definitionally
var-pair : ∀ {Γ Δ S} → (f : Δ ==> Γ) → (M : Tm Δ (S [ f ])) → (var{Γ}{S} < f ,= M >) ≡Tm M
var-pair f M .mor≡ γ    = refl
var-pair f M .rom≡ γ s- = refl

,=-natural : ∀ {Γ Δ Θ}{S : Ty Θ}
             (f : Δ ==> Θ)
             (g : Γ ==> Δ)
             (M : Tm Δ (S [ f ])) →
             (f ,= M) ∘ g ≡mor (_,=_{Γ}{Θ}{S} (f ∘ g) (M < g >))
,=-natural f g M .mor≡ γ = refl
,=-natural f g M .rom≡ γ (false , θ-) = refl
,=-natural f g M .rom≡ γ (true , s-) = refl

----------------------------------------------------------------------
-- Π-types

Π : ∀ {Γ} → (S : Ty Γ) → (T : Ty (Γ ,- S)) → Ty Γ
q (Π S T) γ   = (s : q S γ) → Σ (q T (γ , s)) λ t → r T (γ , s) t -> ⊤ ⊎ r S γ s
r (Π S T) γ f = Σ (q S γ) λ s → Σ (r T (γ , s) (fst (f s))) λ t → is-false (fst (snd (f s) t))

ƛ : ∀ {Γ S T} → Tm (Γ ,- S) T → Tm Γ (Π S T)
ƛ M .mor γ s .fst    = mor M (γ , s)
ƛ M .mor γ s .snd t- = ⊎-map' (rom M (γ , s) t-) (λ _ x → tt) (λ _ x → x)
ƛ M .rom γ (s , (r- , x)) = get-left (rom M (γ , s) r-) x

unƛ : ∀ {Γ S T} → Tm Γ (Π S T) → Tm (Γ ,- S) T
unƛ M .mor (γ , s)    = fst (mor M γ s)
unƛ M .rom (γ , s) t- = ⊎-map' (snd (mor M γ s) t-) (λ x _ → rom M γ (s , (t- , x))) (λ _ s → s)

module Π-naturality {Γ Δ S T} (f : Δ ==> Γ) where

  Π-natural : (Π S T) [ f ] ≡ Π (S [ f ]) (T [ wk f ])
  Π-natural = refl

  ƛ-natural : (M : Tm (Γ ,- S) T) → ƛ (M < wk f >) ≡Tm (ƛ M) < f >
  ƛ-natural M .mor≡ γ              = refl
  ƛ-natural M .rom≡ γ (s , t- , x) with rom M (mor f γ , s) t-
  ƛ-natural M .rom≡ γ (s , t- , false) | false , γ- = refl

  unƛ-natural : (M : Tm Γ (Π S T)) → unƛ (M < f >) ≡Tm (unƛ M) < wk f >
  unƛ-natural M .mor≡ γ = refl
  unƛ-natural M .rom≡ (γ , s) t- = refl

ƛ-unƛ : ∀ {Γ S T} → (M : Tm (Γ ,- S) T) → unƛ (ƛ M) ≡Tm M
ƛ-unƛ M .mor≡ γ = refl
ƛ-unƛ M .rom≡ (γ , s) t- = refl

unƛ-ƛ : ∀ {Γ S T} → (M : Tm Γ (Π S T)) → ƛ (unƛ M) ≡Tm M
mor≡ (unƛ-ƛ M) γ                = refl
rom≡ (unƛ-ƛ M) γ (s , (t- , x)) = get-left-comm (snd (mor M γ s) t-) x (λ x _ → rom M γ (s , t- , x)) (λ _ s → s)

_·_ : ∀ {Γ S T} → (M : Tm Γ (Π S T)) → (N : Tm Γ S) → Tm Γ (T [ ↓ N ])
_·_ M N = (unƛ M) < ↓ N >

Π-β : ∀ {Γ S T} → (M : Tm (Γ ,- S) T) → (N : Tm Γ S) → ((ƛ M) · N) ≡Tm M < ↓ N >
Π-β M N = ≡Tm-cong1 (↓ N) (ƛ-unƛ M)

lem : ∀ {X Y X'} → (x : X ⊎ Y) → (f : is-false (fst x) → X') →
      ⊎-case (⊎-map' x (λ p x → false , f p) (λ p x → x)) (λ _ γ₁ → γ₁) (λ _ s- → true , s-)
      ≡
      ⊎-map' x (λ x _ → f x) (λ _ s₁ → s₁)
lem (false , snd₁) f = refl
lem (true , snd₁) f = refl

h : ∀ {Γ S} → wk{Γ ,- S}{Γ} π₁ ∘ ↓ var ≡mor id{Γ ,- S}
h .mor≡ γ = refl
h .rom≡ γ (false , x) = refl
h .rom≡ γ (true , x) = refl

Π-η : ∀ {Γ S T} → (M : Tm Γ (Π S T)) → ƛ (M ⁺ᵗᵐ · var) ≡ M
Π-η M =
   begin
     ƛ ((M ⁺ᵗᵐ) · var)
   ≡⟨ refl ⟩
     ƛ ( (unƛ (M < π₁ >)) < ↓ var > )
   ≡⟨ cong (λ x → ƛ (x < id ,= var >)) (≡Tm→≡ (Π-naturality.unƛ-natural π₁ M)) ⟩
     ƛ ( unƛ M < wk π₁ > < ↓ var > )
   ≡⟨ refl ⟩
     ƛ ( unƛ M < wk π₁ ∘ (id ,= var) > )
   ≡⟨ cong ƛ (≡Tm→≡ h2) ⟩
     ƛ ( unƛ M < id > )
   ≡⟨ ≡Tm→≡ (unƛ-ƛ M) ⟩
     M
   ∎
  where h2 : unƛ M < wk π₁ ∘ (id ,= var) > ≡Tm unƛ M < id >
        h2 .mor≡ (γ , s)    = refl
        h2 .rom≡ (γ , s) t- = lem (snd (mor M γ s) t-) λ x → rom M γ (s , t- , x)

----------------------------------------------------------------------
-- Σ-types

ΣΣ : ∀ {Γ} → (S : Ty Γ) → (T : Ty (Γ ,- S)) → Ty Γ
q (ΣΣ S T) γ         = Σ (q S γ) λ s → q T (γ , s)
r (ΣΣ S T) γ (s , t) = r S γ s ⊎ r T (γ , s) t

ΣΣ-natural : ∀ {Γ Δ S T} → (f : Δ ==> Γ) → (ΣΣ S T) [ f ] ≡ ΣΣ (S [ f ]) (T [ wk f ])
ΣΣ-natural f = refl

mkpair : ∀ {Γ S T} → (M : Tm Γ S) → Tm Γ (T [ ↓ M ]) → Tm Γ (ΣΣ S T)
mkpair M N .mor γ = mor M γ , mor N γ
mkpair M N .rom γ (false , s-) = rom M γ s-
mkpair M N .rom γ (true , t-)  = rom N γ t-

mkpair-natural : ∀ {Δ Γ S T} → (f : Δ ==> Γ) → (M : Tm Γ S) → (N : Tm Γ (T [ ↓ M ])) → mkpair{Γ}{S}{T} M N < f > ≡Tm mkpair (M < f >) (N < f >)
mkpair-natural f M N .mor≡ γ = refl
mkpair-natural f M N .rom≡ γ (false , s-) = refl
mkpair-natural f M N .rom≡ γ (true , t-)  = refl

proj1 : ∀ {Γ S T} → Tm Γ (ΣΣ S T) → Tm Γ S
proj1 M .mor γ    = fst (mor M γ)
proj1 M .rom γ s- = rom M γ (false , s-)

proj1-natural : ∀ {Δ Γ S T} → (f : Δ ==> Γ) → (M : Tm Γ (ΣΣ S T)) → proj1 M < f > ≡Tm proj1 (M < f >)
proj1-natural f M .mor≡ γ = refl
proj1-natural f M .rom≡ γ s- = refl

proj2 : ∀ {Γ S T} → (M : Tm Γ (ΣΣ S T)) → Tm Γ (T [ ↓ (proj1 M) ])
proj2 M .mor γ    = snd (mor M γ)
proj2 M .rom γ t- = rom M γ (true , t-)

proj2-natural : ∀ {Δ Γ S T} → (f : Δ ==> Γ) → (M : Tm Γ (ΣΣ S T)) → proj2 M < f > ≡Tm proj2 (M < f >)
proj2-natural f M .mor≡ γ = refl
proj2-natural f M .rom≡ γ t- = refl

ΣΣ-β-1 : ∀ {Γ S T} → (M : Tm Γ S) → (N : Tm Γ (T [ ↓ M ])) → proj1{Γ}{S}{T} (mkpair M N) ≡Tm M
ΣΣ-β-1 M N .mor≡ γ    = refl
ΣΣ-β-1 M N .rom≡ γ s- = refl

ΣΣ-β-2 : ∀ {Γ S T} → (M : Tm Γ S) → (N : Tm Γ (T [ ↓ M ])) → proj2{Γ}{S}{T} (mkpair M N) ≡Tm N
ΣΣ-β-2 M N .mor≡ γ    = refl
ΣΣ-β-2 M N .rom≡ γ s- = refl

ΣΣ-η : ∀ {Γ S T} → (M : Tm Γ (ΣΣ S T)) → mkpair (proj1 M) (proj2 M) ≡Tm M
ΣΣ-η M .mor≡ γ              = refl
ΣΣ-η M .rom≡ γ (false , s-) = refl
ΣΣ-η M .rom≡ γ (true , s-)  = refl

----------------------------------------------------------------------
-- Natural number type

NAT : ∀ {Γ} → Ty Γ
q NAT γ = Nat
r NAT γ n = ⊥

ZE : ∀ {Γ} → Tm Γ NAT
ZE .mor γ = zero

SU : ∀ {Γ} → Tm Γ NAT → Tm Γ NAT
SU M .mor γ = suc (mor M γ)

SU' : ∀ {Γ} → (Γ ,- NAT) ==> (Γ ,- NAT)
SU' = π₁ ,= SU var

NAT-rec : ∀ {Γ} T →
          (Ze : Tm Γ (T [ ↓ ZE ])) →
          (Su : Tm (Γ ,- NAT ,- T) (T [ SU' ∘ π₁ ])) →
          Tm (Γ ,- NAT) T
NAT-rec T Ze Su .mor (γ , zero)  = mor Ze γ
NAT-rec T Ze Su .mor (γ , suc n) = mor Su ((γ , n) , mor (NAT-rec T Ze Su) (γ , n))
NAT-rec T Ze Su .rom (γ , zero)  t- = false , rom Ze γ t-
NAT-rec T Ze Su .rom (γ , suc n) t- =
  ⊎-case (rom Su ((γ , n) , mor (NAT-rec T Ze Su) (γ , n)) t-) (λ _ x → x) (λ _ → rom (NAT-rec T Ze Su) (γ , n))

lemma10 :   ∀ {X : Set} {Y Z : X → Set} ->
  (f  : (x : X) → Y x → Z x) ->
  {x y : X} ->
  (eq : x ≡ y) ->
  (y- : Y x) ->
  subst Z eq (f x y-) ≡ f y (subst Y eq y-)
lemma10 f refl y- = refl

subst-cong : ∀ {X Y : Set} → {T : Y → Set} → {f : X → Y}{x x' : X} → (eq : x ≡ x') → (x : T (f x)) → subst (λ x → T (f x)) eq x ≡ subst T (cong f eq) x
subst-cong refl x = refl

-- FIXME: naturality of the above in Γ
{-
NAT-rec-natural : ∀ {Δ Γ} T →
          (f : Δ ==> Γ) →
          (Ze : Tm Γ (T [ ↓ ZE ])) →
          (Su : Tm (Γ ,- NAT ,- T) (T [ SU' ∘ π₁ ])) →
          NAT-rec T Ze Su < wk f > ≡Tm NAT-rec (T [ wk f ]) (Ze < f >) (Su < wk (wk f) >)
NAT-rec-natural T f Ze Su .mor≡ (δ , zero) = refl
NAT-rec-natural T f Ze Su .mor≡ (δ , suc n) = cong (λ x → mor Su ((mor f δ , n) , x)) (NAT-rec-natural T f Ze Su .mor≡ (δ , n))
NAT-rec-natural T f Ze Su .rom≡ (δ , zero) t- = refl
NAT-rec-natural{Δ}{Γ} T f Ze Su .rom≡ (δ , suc n) t- =
  trans {!NAT-rec-natural{Δ}{Γ} T f Ze Su .rom≡ (δ , n) !} (cong (λ z → ⊎-case
      (⊎-map' z
       (λ _ δs- → ⊎-map' δs- (λ _ → rom f δ) (λ _ s- → s-)) (λ _ s- → s-))
      (λ _ x → x)
      (λ _ → rom (NAT-rec (T [ wk f ]) (Ze < f >) (Su < wk (wk f) >)) (δ , n))) helper)
  where
   helper :
      subst
        (λ x → Σ Bool (Ch (r Γ (mor f δ) ⊎ ⊥) (r T (mor f δ , n) x)))
        (NAT-rec-natural T f Ze Su .mor≡ (δ , n))
        (rom Su ((mor f δ , n) , mor (NAT-rec T Ze Su) (mor f δ , n)) t-)
      ≡
      rom Su
       ((mor f δ , n) ,
        mor (NAT-rec (T [ wk f ]) (Ze < f >) (Su < wk (wk f) >)) (δ , n))
       (subst (λ s → r T (mor f δ , suc n) s)
        (cong (λ x → mor Su ((mor f δ , n) , x))
         (NAT-rec-natural T f Ze Su .mor≡ (δ , n)))
        t-)
   helper = trans (lemma10 (λ x → rom Su ((mor f δ , n) , x)) (NAT-rec-natural T f Ze Su .mor≡ (δ , n)) t-)
                  (cong (rom Su ((mor f δ , n) , mor (NAT-rec (T [ wk f ]) (Ze < f >) (Su < wk (wk f) >)) (δ , n)))
                        (subst-cong (NAT-rec-natural T f Ze Su .mor≡ (δ , n)) t-))
-}

NAT-β-ZE : ∀ {Γ} T →
          (Ze : Tm Γ (T [ ↓ ZE ])) →
          (Su : Tm (Γ ,- NAT ,- T) (T [ SU' ∘ π₁ ])) →
          NAT-rec T Ze Su < ↓ ZE > ≡Tm Ze
NAT-β-ZE T Ze Su .mor≡ γ = refl
NAT-β-ZE T Ze Su .rom≡ γ t- = refl

NAT-β-SU : ∀ {Γ} T →
          (Ze : Tm Γ (T [ ↓ ZE ])) →
          (Su : Tm (Γ ,- NAT ,- T) (T [ SU' ∘ π₁ ])) →
          (N  : Tm Γ NAT) →
          NAT-rec T Ze Su < ↓ (SU N) > ≡Tm Su < ↓ N ,= NAT-rec T Ze Su < ↓ N > >
NAT-β-SU T Ze Su N .mor≡ γ = refl
NAT-β-SU T Ze Su N .rom≡ γ t- with rom Su ((γ , mor N γ)  , mor (NAT-rec T Ze Su) (γ , mor N γ)) t-
NAT-β-SU T Ze Su N .rom≡ γ t- | false , false , _ = refl
NAT-β-SU T Ze Su N .rom≡ γ t- | true , t-' with rom (NAT-rec T Ze Su) (γ , mor N γ) t-'
NAT-β-SU T Ze Su N .rom≡ γ t- | true , t-' | false , _ = refl

----------------------------------------------------------------------
-- A universe

mutual
  data U : Set where
    `nat   : U
    `π     : (X : U) → (Y : q (decode X) → U) → U

  decode : U → Cont
  q (decode `nat)     = Nat
  r (decode `nat)     _ = ⊥
  q (decode (`π S T)) = (s : q (decode S)) → Σ (q (decode (T s))) λ t → r (decode (T s)) t → ⊤ ⊎ r (decode S) s
  r (decode (`π S T)) f =
     Σ (q (decode S)) λ s → Σ (r (decode (T s)) (fst (f s))) λ t- → is-false (fst (snd (f s) t-))

UU : ∀ {Γ} → Ty Γ
q UU γ   = U
r UU γ _ = ⊥

UU-natural : ∀ {Γ Δ} → (f : Γ ==> Δ) → UU [ f ] ≡ UU
UU-natural f = refl

El : ∀ {Γ} → Tm Γ UU → Ty Γ
q (El M) γ = q (decode (mor M γ))
r (El M) γ = r (decode (mor M γ))

El-natural : ∀ {Γ Δ} → (f : Γ ==> Δ) → (M : Tm Δ UU) → El (M < f >) ≡ El M [ f ]
El-natural f M = refl

El' : ∀ {Γ} → Ty (Γ ,- UU)
q El' (γ , c)   = q (decode c)
r El' (γ , c) x = r (decode c) x

`Π : ∀ {Γ} → (X : Tm Γ UU) → (Y : Tm (Γ ,- El X) UU) → Tm Γ UU
mor (`Π X Y) γ = `π (mor X γ) (λ x → mor Y (γ , x))

`NAT : ∀ {Γ} → Tm Γ UU
mor `NAT γ = `nat

El-Π : ∀ {Γ}{X : Tm Γ UU}{Y} → El (`Π X Y) ≡ Π (El X) (El Y)
El-Π = refl

El-NAT : ∀ {Γ} → El{Γ} `NAT ≡ NAT
El-NAT = refl

----------------------------------------------------------------------
-- Eq-type

Eq : ∀ {Γ} → (S : Ty Γ) → Ty (Γ ,- S ,- S ⁺)
q (Eq S) ((γ , s₁) , s₂)   = s₁ ≡ s₂
r (Eq S) ((γ , s₁) , s₂) _ = ⊥
                          -- r (S γ) s₁ ⊎ r (S γ) s₂
-- FIXME: lots of choice here for the refutation of equality

Eq-natural : ∀ {Γ Δ S} → (f : Γ ==> Δ) → Eq (S [ f ]) ≡ (Eq S) [ wk (wk f) ]
Eq-natural f = refl

Eq-refl : ∀ {Γ S} → (Γ ,- S) ==> (Γ ,- S ,- S ⁺ ,- Eq S)
Eq-refl .mor (γ , s) = ((γ , s) , s) , refl
Eq-refl .rom (γ , s) (false , false , false , γ-) = false , γ-
Eq-refl .rom (γ , s) (false , false , true , s-)  = true , s-
Eq-refl .rom (γ , s) (false , true , s-)          = true , s-

Eq-refl-natural : ∀ {Γ Δ S} → (f : Δ ==> Γ) → Eq-refl{Γ}{S} ∘ wk f ≡mor wk (wk (wk f)) ∘ Eq-refl{Δ}
Eq-refl-natural f .mor≡ (δ , s) = refl
Eq-refl-natural f .rom≡ (δ , s) (false , false , false , _) = refl
Eq-refl-natural f .rom≡ (δ , s) (false , false , true , _)  = refl
Eq-refl-natural f .rom≡ (δ , s) (false , true , _) = refl

dup : ∀ {Γ S} → (Γ ,- S) ==> (Γ ,- S ,- S ⁺)
dup = id ,= var

Eq-refl-dup : ∀ {Γ S} → π₁ ∘ Eq-refl{Γ}{S} ≡mor dup
Eq-refl-dup .mor≡ γs = refl
Eq-refl-dup .rom≡ (γ , s) (false , false , y-) = refl
Eq-refl-dup .rom≡ (γ , s) (false , true , y-) = refl
Eq-refl-dup .rom≡ (γ , s) (true , y-) = refl

Eq-J : ∀ {Γ S} T -> Tm (Γ ,- S) (T [ Eq-refl ])
                 -> Tm (Γ ,- S ,- S ⁺ ,- Eq S) T
Eq-J T M .mor (((γ , s₁) , s₂) , refl) = mor M (γ , s₁)
Eq-J T M .rom (((γ , s₁) , s₂) , refl) t- with rom M (γ , s₁) t-
... | false , γ- = false , false , false , γ-
... | true , s-  = false , false , true  , s- -- FIXME: why this choice?

Eq-J-natural : ∀ {Δ Γ S} T ->
               (f : Δ ==> Γ) ->
               (M : Tm (Γ ,- S) (T [ Eq-refl ])) ->
               Eq-J T M < wk (wk (wk f)) > ≡Tm Eq-J (T [ wk (wk (wk f)) ]) (M < wk f >)
Eq-J-natural T f M .mor≡ (((δ , s) , s) , refl) = refl
Eq-J-natural T f M .rom≡ (((δ , s) , s) , refl) t- with rom M (mor f δ , s) t-
... | false , _ = refl
... | true , _ = refl

Eq-refl-tm : ∀ {Γ S} → (M : Tm Γ S) → Tm Γ (Eq S [ id ,= M ,= M ])
Eq-refl-tm M = var < Eq-refl ∘ ↓ M >

Eq-β : ∀ {Γ S T}
       -> (M : Tm (Γ ,- S) (T [ Eq-refl ]))
       -> Eq-J T M < Eq-refl > ≡Tm M
Eq-β M .mor≡ (γ , s) = refl
Eq-β M .rom≡ (γ , s) s- with rom M (γ , s) s-
...                        | false , x = refl
...                        | true , x = refl

----------------------------------------------------------------------
-- failure of functional extensionality in the model

fext-stmt : Set₁
fext-stmt = ∀ {Γ S T} ->
              (F G : Tm Γ (Π S T)) ->
              Tm (Γ ,- S) (Eq T [ id ,= (F ⁺ᵗᵐ · var) ,= (G ⁺ᵗᵐ · var) ]) ->
              Tm Γ (Eq (Π S T) [ id ,= F ,= G ])

module fext-fails where

    S : Ty ε
    q S tt = ⊤
    r S tt tt = Bool

    T : Ty (ε ,- S)
    q T (tt , tt) = ⊤
    r T (tt , tt) tt = ⊤

    F : Tm ε (Π S T)
    F .mor tt tt = tt , λ _ → true , true
    F .rom tt (tt , (tt , ()))

    G : Tm ε (Π S T)
    G .mor tt tt = tt , λ _ → true , false
    G .rom tt (tt , (tt , ()))

    F-ptwise-eq-G : Tm (ε ,- S) (Eq T [ id ,= (F ⁺ᵗᵐ · var) ,= (G ⁺ᵗᵐ · var) ])
    F-ptwise-eq-G .mor (tt , tt) = refl
    F-ptwise-eq-G .rom (tt , tt) ()

    Cont-fext-fail : fext-stmt -> ⊥
    Cont-fext-fail fext = contradiction
      where
        F-eq-G : Tm ε (Eq (Π S T) [ id ,= F ,= G ])
        F-eq-G = fext F G F-ptwise-eq-G

        morF≡morG : mor F tt ≡ mor G tt
        morF≡morG = F-eq-G .mor tt

        true≡false : (true , true) ≡ (true , false)
        true≡false = subst (λ x → F .mor tt tt .snd tt ≡ x tt .snd tt) morF≡morG refl

        contradiction : ⊥
        contradiction with true≡false
        contradiction | ()