Last active
June 16, 2023 21:23
-
-
Save bobatkey/0d1f04057939905d35699f1b1c323736 to your computer and use it in GitHub Desktop.
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# 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 | () |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Question. Why use the
Lensmapping between polynomial functors instead of aChart?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)