mini-OTT.agda

{-# OPTIONS --type-in-type #-}

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Unit.Base
open import Data.Empty
open import Data.Product
open import Data.Nat.Base

{-# NO_POSITIVITY_CHECK #-}
mutual
  data Type : Set where
    nat  : Type
    type : Type
    π    : (A : Type) -> (⟦ A ⟧ -> Type) -> Type

  ⟦_⟧ : Type -> Set
  ⟦ nat   ⟧ = ℕ
  ⟦ type  ⟧ = Type
  ⟦ π a b ⟧ = (x : ⟦ a ⟧) -> ⟦ b x ⟧

{-# TERMINATING #-}
_≈_ : Type -> Type -> Set
_≋_ : ∀ {a} -> ⟦ a ⟧ -> ⟦ a ⟧ -> Set

nat     ≈ nat     = ⊤
type    ≈ type    = ⊤
π a₁ b₁ ≈ π a₂ b₂ = ∃ λ (eq : a₂ ≡ a₁) -> ∀ {x₁ x₂} -> x₁ ≋ x₂ -> b₁ (subst ⟦_⟧ eq x₁) ≈ b₂ x₂
_       ≈ _       = ⊥

coerce : ∀ {a b} -> a ≈ b -> ⟦ a ⟧ -> ⟦ b ⟧
osubst : ∀ {a x y} -> (P : ⟦ a ⟧ -> Type) -> x ≋ y -> ⟦ P x ⟧ -> ⟦ P y ⟧

_≋_ {nat}   n  m  = n ≡ m
_≋_ {type}  a  b  = a ≈ b
_≋_ {π a b} f₁ f₂ = ∀ {x₁ x₂} -> (eq : x₁ ≋ x₂) -> osubst b eq (f₁ x₁) ≋ f₂ x₂

postulate orefl : ∀ {a} -> (x : ⟦ a ⟧) -> x ≋ x

coerce {nat}     {nat}      _          n = n
coerce {type}    {type}     _          a = a
coerce {π a₁ b₁} {π a₂ b₂} (refl , eq) f = λ x -> coerce (eq (orefl x)) (f x)
coerce = undefined where postulate undefined : _ -- just being lazy

-- `vrefl P eq` is of the same type as `eq′`,
-- but Agda gets confused because `osubst` appears in its own type.
osubst P eq = coerce eq′ where postulate eq′ : _

-- Test

shallowC42 : ℕ -> ℕ
shallowC42 = const 42

deepC42 : ℕ -> ℕ
deepC42  0      = 42
deepC42 (suc n) = deepC42 n

-- Two functions are equal if they are equal pointwise. I.e. this is functional extensionality.
c42-eq : shallowC42 ≋ deepC42
c42-eq {zero } refl = refl
c42-eq {suc n} refl = c42-eq {n} refl

postulate
  Favourite : (ℕ -> ℕ) -> Type
  fave : ⟦ Favourite shallowC42 ⟧

fave′ : ⟦ Favourite deepC42 ⟧
fave′ = osubst Favourite c42-eq fave