Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted

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
open import Relation.Binary.PropositionalEquality public using (_≡_; refl; trans; subst; cong)
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

----------------------------------------------------------------------
-- Sum types as pairs
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} → (A -> B) -> (C -> D) -> A ⊎ C → B ⊎ D
⊎-map f g x .fst = fst x
⊎-map f g (false , a) .snd = f a
⊎-map f g (true , c) .snd = g c

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

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

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

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

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

----------------------------------------------------------------------
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_

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 ≡mor f
  mor≡ (id-comp A B f) a    = refl
  rom≡ (id-comp A B f) a b- = refl

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

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

----------------------------------------------------------------------
-- Terminal object, representng 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

Ty-Eq : ∀{Γ}{S T : Ty Γ} → (e : q S ≡ q T) → subst (λ x → (γ : q Γ) → x γ → Set) e (r S) ≡ r T → S ≡ T
Ty-Eq refl refl = refl

-- previously: 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-preserve : ∀{Γ Δ S} → (f g : Γ ==> Δ) → f ≡mor g → S [ f ] ≡ S [ g ]
-- Ty-preserve f g e = {!!}

-- FIXME: composition and identities

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

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

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_

_<_> : ∀ { Γ Δ 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-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-)

-- FIXME: preservation, composition, and identities

----------------------------------------------------------------------
-- 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 δ = ⊎-case (rom f δ) (rom M δ)

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

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

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 (rom f γ) (λ s- → s-) δs-

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

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

-- FIXME: needs π-pair to type check
-- var-pair : ∀ {Γ Δ S} → (f : Cont-mor Δ Γ) → (M : Tm Δ (S [ f ])) → (var [ f ,= M ]) ≡Tm M

-- FIXME: the other naturality equation from Hofmann

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

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

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

Π : ∀ {Γ} → (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))

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

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

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

lemma : ∀ {X Y} → (s : ⊤ ⊎ Y) -> (is-false (fst s) -> X) -> X ⊎ Y
fst (lemma x f) = fst x
snd (lemma (false , tt) f) = f false
snd (lemma (true , y)   f) = y

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

lemma-natural : ∀ {X X' Y : Set} →
   (s : ⊤ ⊎ Y) →
   (g : is-false (fst s) -> X) →
   (f : X → X') →
   lemma s (λ x → f (g x)) ≡ ⊎-map (λ y → f y) (λ s- → s-) (lemma s g )
lemma-natural (false , tt) g f = refl
lemma-natural (true , y) g f = refl

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

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

_·_ : ∀ {Γ 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)

lemma2 : ∀ {X Y} → (x : ⊤ ⊎ Y) → (f : is-false (fst x) -> X) → ⊎-map (λ x → tt) (λ x → x) (lemma x f) ≡ x
lemma2 (false , x) f = refl
lemma2 (true , x)  f = refl

{-# REWRITE lemma2 #-}

lemma4 : ∀{X Y : Set} -> (s : ⊤ ⊎ Y) → (f : is-false (fst s) → X) → (x : is-false (fst s)) → get-left (lemma s f) x ≡ f x
lemma4 (.false , tt) f false = refl

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

----------------------------------------------------------------------
-- Σ-type

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

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

pair : ∀ {Γ S T} → (Γ ,- S ,- T) ==> (Γ ,- Sg S T)
pair .mor ((γ , s) , t) = γ , (s , t)
pair .rom ((γ , s) , t) (false , γ-)        = false , false , γ-
pair .rom ((γ , s) , t) (true , false , s-) = false , true , s-
pair .rom ((γ , s) , t) (true , true , t-)  = true , t-

elim : ∀ {Γ S T} →
       (U : Ty (Γ ,- Sg S T)) →
       (M : Tm (Γ ,- S ,- T) (U [ pair ])) →
       Tm (Γ ,- Sg S T) U
elim U M .mor (γ , s , t) = mor M ((γ , s) , t)
elim U M .rom (γ , s , t) u- with rom M ((γ , s) , t) u-
... | false , false , γ- = false , γ-
... | false , true , s-  = true , false , s-
... | true , t-          = true , true , t-

Sg-β : ∀ {Γ S T} →
     (U : Ty (Γ ,- Sg S T)) →
     (M : Tm (Γ ,- S ,- T) (U [ pair ])) →
     elim U M < pair > ≡Tm M
Sg-β U M .mor≡ γ = refl
Sg-β U M .rom≡ ((γ , s) , t) u- with rom M ((γ , s) , t) u-
... | false , false , _ = refl
... | false , true  , _ = refl
... | true  , _         = refl

-- FIXME: naturality of pair and elim

----------------------------------------------------------------------
-- 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 (λ x → x) (rom (NAT-rec T Ze Su) (γ , n)) (rom Su ((γ , n) , mor (NAT-rec T Ze Su) (γ , n)) t-)

-- FIXME: naturality of the above in Γ

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 γ _ = ⊥

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

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)
mor Eq-refl (γ , s) = ((γ , s) , s) , refl
rom Eq-refl (γ , s) (false , false , false , γ-) = false , γ-
rom Eq-refl (γ , s) (false , false , true , s-)  = true , s-
rom Eq-refl (γ , s) (false , true , s-)          = true , s-

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

-- FIXME: to prove:
-- 1. Eq-refl is natural in Γ
-- 2. Eq-refl is also a duplication morphism
-- 3. Eq-J is natural in Γ

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 ,= unƛ F ,= unƛ G ]) ->
              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)
    mor F tt tt = tt , λ _ → true , true
    rom F tt (tt , (tt , ()))

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

    F-ptwise-eq-G : Tm (ε ,- S) (Eq T [ id ,= unƛ F ,= unƛ G ])
    mor F-ptwise-eq-G (tt , tt) = refl
    rom F-ptwise-eq-G (tt , tt) ()

    Cont-fext-fail : fext-stmt -> ⊥
    Cont-fext-fail fext      with fext F G F-ptwise-eq-G
    ...          | F-eq-G    with mor F-eq-G tt
    ...          | morF≡morG with subst (λ x -> snd (mor F tt tt) tt ≡ snd (x tt) tt) morF≡morG refl
    ...          | ()