Skip to content

Instantly share code, notes, and snippets.

@bobatkey

bobatkey/cont-cwf.agda

Last active June 16, 2023 21:23
Show Gist options
  • Save bobatkey/0d1f04057939905d35699f1b1c323736 to your computer and use it in GitHub Desktop.
Save bobatkey/0d1f04057939905d35699f1b1c323736 to your computer and use it in GitHub Desktop.
Download ZIP
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
Raw
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 | ()
@bond15
Copy link

bond15 commented Jan 29, 2022

Question. Why use the Lens mapping between polynomial functors instead of a Chart?
Where the mapping is forward on positions/questions and forward on directions/answers.

terminology from (https://www.youtube.com/watch?v=FU9B-H6Tb4w&list=PLhgq-BqyZ7i6IjU82EDzCqgERKjjIPlmh&index=10)

@bond15
Copy link

bond15 commented Jan 29, 2022

from https://arxiv.org/pdf/1904.00827.pdf
Definition 2.21 of CwF uses Charts

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment