|
|
@@ -0,0 +1,99 @@ |
|
|
{-# OPTIONS --cubical #-} |
|
|
module natmod where |
|
|
open import Cubical.Foundations.Prelude |
|
|
|
|
|
data Ctx : Type |
|
|
data _⊢_ : Ctx → Ctx → Type |
|
|
data Ty : Ctx → Type |
|
|
data Tm : Ctx → Type |
|
|
-- This is halfway between EAT and GAT. |
|
|
-- GAT is hard! Why is EAT so easy? |
|
|
|
|
|
variable |
|
|
Γ Δ Θ : Ctx |
|
|
σ δ θ τ : Γ ⊢ Δ |
|
|
A B : Ty Γ |
|
|
a b s t : Tm Γ |
|
|
|
|
|
infix 3 _⊢_ |
|
|
infixl 5 _∘_ |
|
|
infixl 5 _⟦_⟧ᵗ _⟦_⟧ₜ |
|
|
infixl 4 _,,_ |
|
|
|
|
|
_⟦_⟧ᵗ' : Ty Γ → Δ ⊢ Γ → Ty Δ |
|
|
_⟦_⟧ₜ' : Tm Γ → Δ ⊢ Γ → Tm Δ |
|
|
type' : Tm Γ → Ty Γ |
|
|
|
|
|
data Ctx where |
|
|
-- Is it possible to make univalent in one go? |
|
|
-- Or Rezk complete later? |
|
|
|
|
|
[] : Ctx |
|
|
_,,_ : (Γ : Ctx) → Ty Γ → Ctx |
|
|
|
|
|
𝔮' : ∀ A → Tm (Γ ,, A) |
|
|
𝔭' : Γ ,, A ⊢ Γ |
|
|
_∘'_ : Δ ⊢ Γ → Θ ⊢ Δ → Θ ⊢ Γ |
|
|
path' : type' (𝔮' A ⟦ σ ⟧ₜ') ≡ (A ⟦ 𝔭' ∘' σ ⟧ᵗ') |
|
|
|
|
|
data _⊢_ where |
|
|
isSet⊢ : isSet (Γ ⊢ Δ) |
|
|
|
|
|
_∘_ : Δ ⊢ Γ → Θ ⊢ Δ → Θ ⊢ Γ |
|
|
id : ∀ Γ → Γ ⊢ Γ |
|
|
|
|
|
assoc : (σ ∘ δ) ∘ τ ≡ σ ∘ (δ ∘ τ) |
|
|
idₗ : id Γ ∘ σ ≡ σ |
|
|
idᵣ : σ ∘ id Γ ≡ σ |
|
|
|
|
|
[] : Γ ⊢ [] |
|
|
η[] : (f : Γ ⊢ []) → σ ≡ [] |
|
|
|
|
|
𝔭 : Γ ,, A ⊢ Γ |
|
|
|
|
|
ext : (σ : Γ ⊢ Δ) (a : Tm Γ) -- no pretty syntax |
|
|
→ type' a ≡ A ⟦ σ ⟧ᵗ' |
|
|
→ Γ ⊢ Δ ,, A |
|
|
𝔭-ext : (p : type' a ≡ A ⟦ σ ⟧ᵗ') → 𝔭 ∘ ext σ a p ≡ σ |
|
|
𝔭𝔮 : ext (𝔭' ∘' σ) (𝔮' A ⟦ σ ⟧ₜ') path' ≡ σ |
|
|
|
|
|
data Tm where |
|
|
isSetTm : isSet (Tm Γ) |
|
|
|
|
|
-- Functorial action |
|
|
_⟦_⟧ₜ : Tm Γ → Δ ⊢ Γ → Tm Δ |
|
|
_⟦id⟧ₜ : ∀ t → t ⟦ id Γ ⟧ₜ ≡ t |
|
|
_⟦_⟧⟦_⟧ₜ : ∀ t (σ : Δ ⊢ Γ) (τ : Θ ⊢ Δ) |
|
|
→ t ⟦ σ ∘ τ ⟧ₜ ≡ t ⟦ σ ⟧ₜ ⟦ τ ⟧ₜ |
|
|
|
|
|
𝔮 : ∀ A → Tm (Γ ,, A) |
|
|
|
|
|
𝔮-ext : (p : type' a ≡ A ⟦ σ ⟧ᵗ') → 𝔮 A ⟦ ext σ a p ⟧ₜ ≡ a |
|
|
|
|
|
data Ty where |
|
|
isSetTy : isSet (Ty Γ) |
|
|
|
|
|
-- Functorial action |
|
|
_⟦_⟧ᵗ : Ty Γ → Δ ⊢ Γ → Ty Δ |
|
|
_⟦id⟧ᵗ : ∀ A → A ⟦ id Γ ⟧ᵗ ≡ A |
|
|
_⟦_⟧⟦_⟧ᵗ : ∀ A (σ : Δ ⊢ Γ) (τ : Θ ⊢ Δ) |
|
|
→ A ⟦ σ ∘ τ ⟧ᵗ ≡ A ⟦ σ ⟧ᵗ ⟦ τ ⟧ᵗ |
|
|
|
|
|
-- Typing |
|
|
type : Tm Γ → Ty Γ |
|
|
type⟦⟧ : type (t ⟦ σ ⟧ₜ) ≡ (type t) ⟦ σ ⟧ᵗ |
|
|
|
|
|
type-𝔮 : type (𝔮 A) ≡ A ⟦ 𝔭 ⟧ᵗ |
|
|
|
|
|
_⟦_⟧ᵗ' = _⟦_⟧ᵗ |
|
|
_⟦_⟧ₜ' = _⟦_⟧ₜ |
|
|
type' = type |
|
|
|
|
|
𝔮' = 𝔮 |
|
|
𝔭' = 𝔭 |
|
|
|
|
|
_∘'_ = _∘_ |
|
|
path' {σ = σ} |
|
|
= type⟦⟧ |
|
|
∙ cong (_⟦ σ ⟧ᵗ) type-𝔮 |
|
|
∙ sym (_ ⟦ _ ⟧⟦ σ ⟧ᵗ) |
Trebor-Huang created this gist