IndexingByCanonicity.agda

{-# OPTIONS --type-in-type  --no-positivity-check --no-termination-check #-}

module IndexingByCanonicity where

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁
open Σ public

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
  
data ⊥ : Set where

! : {A : Set} → ⊥ → A
! ()

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : {A : Set} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f

----------------------------------------------------------------------

data Canonicity : Set where
  can uni : Canonicity
  
mutual
  
  data Type : Set where
    `Set `⊥ `⊤ `Bool : Type
    _`→_ _`×_ : (τ τ' : Type) → Type
    _`≡_ : {τ : Type} (x y : Term can τ) → Type
  
  ⟦_⟧t : Type → Set 
  ⟦ `Set ⟧t = Set
  ⟦ `⊥ ⟧t = ⊥
  ⟦ `⊤ ⟧t = ⊤
  ⟦ `Bool ⟧t = Bool
  ⟦ τ `→ τ′ ⟧t = (ρ : Term can τ) → ⟦ τ′ ⟧t
  ⟦ τ `× τ′ ⟧t = Σ ⟦ τ ⟧t λ _ → ⟦ τ′ ⟧t
  ⟦ τ `≡ τ′ ⟧t = ⟦ τ ⟧ ≡ ⟦ τ′ ⟧
  
  ----------------------------------------------------------------------
  
    
  data Term : Canonicity → Type → Set
  ⟦_⟧ : ∀ {τ} → Term can τ → ⟦ τ ⟧t
  
  data Term where
    ⟨_⟩ : Type → Term can `Set
    _`$_ : {τ τ′ : Type} (e : Term can (τ `→ τ′)) (e′ : Term can τ) → Term can τ′
    `refl : {τ : Type} {x y : Term can τ} {{p : ⟦ x ⟧ ≡ ⟦ y ⟧}} → Term can (x `≡ y)
    `iso : {σ τ : Type}
           (f : ⟦ σ ⟧t → ⟦ τ ⟧t)
           (g : ⟦ τ ⟧t → ⟦ σ ⟧t)
           (α : ∀ x → f (g x) ≡ x)
           (β : ∀ x → g (f x) ≡ x)
           → Term uni (⟨ σ ⟩ `≡ ⟨ τ ⟩ )
    `transport : {σ τ : Type} (p : Term uni (⟨ σ ⟩ `≡ ⟨ τ ⟩)) → Term can σ → Term can τ
    _`,_ : {σ τ : Type} → Term can σ → Term can τ → Term can (σ `× τ)
    `π₁ : {σ τ : Type} (pair : Term can (σ `× τ)) → Term can σ
    `π₂ : {σ τ : Type} (pair : Term can (σ `× τ)) → Term can τ
    `tt : Term can `⊤
    `true `false : Term can `Bool
    `λ : {τ τ′ : Type} (e : (ρ : Term can τ) → Term can τ′) → Term can (τ `→ τ′)
    `! : {τ : Type} (e : Term can `⊥) → Term can τ
    `if_then_else_ : {τ : Type} (e : Term can `Bool) (e₁ e₂ : Term can τ) → Term can τ

  ⟦ ⟨ t ⟩ ⟧ = ⟦ t ⟧t
  ⟦ `refl {{p}} ⟧ = p
  ⟦_⟧ (_`$_ x x₁) = ⟦ x ⟧ x₁
  ⟦_⟧ (`transport (`iso f g α β) x) = f ⟦ x ⟧
  ⟦_⟧ (_`,_ x y) = ⟦ x ⟧ , ⟦ y ⟧
  ⟦ `π₁ x ⟧ = π₁ ⟦ x ⟧
  ⟦ `π₂ x ⟧ = π₂ ⟦ x ⟧
  ⟦_⟧ `tt = tt
  ⟦_⟧ `true = true
  ⟦_⟧ `false = false
  ⟦_⟧ (`λ e) = λ v → ⟦ e v ⟧
  ⟦_⟧ (`! x) = ! ⟦ x ⟧
  ⟦_⟧ (`if x then x₁ else x₂) = if ⟦ x ⟧ then ⟦ x₁ ⟧  else ⟦ x₂ ⟧

id : Bool → Bool
id x = x

not : Bool → Bool
not x = if x then false else true

bool-refl : Term _ (⟨ `Bool ⟩ `≡ ⟨ `Bool ⟩)
bool-refl = `refl 

bool-equiv-id : Term _ (⟨ `Bool ⟩ `≡ ⟨ `Bool ⟩)
bool-equiv-id = `iso (λ x → x) (λ x → x) (λ x → refl) (λ x → refl) 

bool-equiv-not : Term _ (⟨ `Bool ⟩ `≡ ⟨ `Bool ⟩)
bool-equiv-not = `iso not not coh coh where
  coh : (x : Bool) → not (not x) ≡ x
  coh true = refl
  coh false = refl

test-refl : Term can ((`transport bool-equiv-id `true) `≡ `true )
test-refl = `refl

test-id : Term can ((`transport bool-equiv-id `true) `≡ `true)
test-id = `refl

test-not : Term can ((`transport bool-equiv-not `true) `≡ `false)
test-not = `refl

swap : ∀ {A B} → (Σ A λ _ → B) → (Σ B λ _ → A)
swap (x , y) = (y , x)

pair-equiv-swap : ∀ {A B} → Term _ (⟨ A `× B ⟩ `≡ ⟨ B `× A ⟩)
pair-equiv-swap {A} {B} = `iso swap swap (λ x → refl) (λ x → refl)

test-pair-swap : Term can ((`transport pair-equiv-swap (`true `, `false)) `≡ (`false `, `true ))
test-pair-swap = `refl 

is-true : Term can (`Bool `→ `Set)
is-true = `λ (λ ρ → `if ρ then ⟨ `⊤ ⟩ else ⟨ `⊥ ⟩)