OTT in Agda using rewrite rules

OTT-rewriting.agda

{-# OPTIONS --rewriting #-}

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Product using (Σ; Σ-syntax; _×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality

Π : (A : Set) (B : A → Set) → Set
Π A B = (x : A) → B x

infix 0 _↦_
postulate _↦_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set
{-# BUILTIN REWRITE _↦_ #-}

-- Type-level equality
infix 1 _==_
postulate _==_ : Set → Set → Set

-- Value-level equality
infix 1 _∋_==_∋_
postulate _∋_==_∋_ : (A : Set) (x : A) (B : Set) (y : B) → Set

-- Coercion
infix 10 _[_⟩
postulate _[_⟩ : {A B : Set} → A → .(A == B) → B

-- Coherence
infix 10 _∥_
postulate ._∥_ : {A B : Set} (x : A) (Q : A == B) → A ∋ x == B ∋ x [ Q ⟩

postulate ⊥-equality : ⊥ == ⊥ ↦ ⊤
{-# REWRITE ⊥-equality #-}

postulate coerce-⊥ : ∀ (z : ⊥) (Q : ⊥ == ⊥) → z [ Q ⟩ ↦ z
{-# REWRITE coerce-⊥ #-}

postulate ⊤-equality : ⊤ == ⊤ ↦ ⊤
{-# REWRITE ⊤-equality #-}

postulate coerce-⊤ : ∀ (u : ⊤) (Q : ⊤ == ⊤) → u [ Q ⟩ ↦ u
{-# REWRITE coerce-⊤ #-}

postulate Bool-equality : Bool == Bool ↦ ⊤
{-# REWRITE Bool-equality #-}

postulate coerce-Bool : ∀ (b : Bool) (Q : Bool == Bool) → b [ Q ⟩ ↦ b
{-# REWRITE coerce-Bool #-}

postulate Σ-equality : ∀ S₀ T₀ S₁ T₁
                     → (Σ S₀ T₀) == (Σ S₁ T₁)
                     ↦ (S₀ == S₁) × ((x₀ : S₀) (x₁ : S₁) → .(S₀ ∋ x₀ == S₁ ∋ x₁) → T₀ x₀ == T₁ x₁)
{-# REWRITE Σ-equality #-}

postulate coerce-Σ : ∀ S₀ T₀ S₁ T₁ (p₀ : Σ S₀ T₀) (Q : Σ S₀ T₀ == Σ S₁ T₁)
                   → let s₀ = proj₁ p₀
                         t₀ = proj₂ p₀
                         s₁ = s₀ [ proj₁ Q ⟩
                         Qs = proj₁ Q
                         Qt = proj₂ Q s₀ s₁ ( s₀ ∥ Qs )
                         t₁ = t₀ [ Qt ⟩
                     in  p₀ [ Q ⟩ ↦ s₁ , t₁


{-# REWRITE coerce-Σ #-}

postulate Π-equality : ∀ (S₀ : Set) (T₀ : S₀ → Set) (S₁ : Set) (T₁ : S₁ → Set)
                     → (Π S₀ T₀) == (Π S₁ T₁)
                     ↦ (S₁ == S₀) × ((x₁ : S₁) (x₀ : S₀) → .(S₁ ∋ x₁ == S₀ ∋ x₀) → T₀ x₀ == T₁ x₁)
{-# REWRITE Π-equality #-}

postulate coerce-Π : ∀ S₀ T₀ S₁ T₁ (f₀ : Π S₀ T₀) (Q : Π S₀ T₀ == Π S₁ T₁)
                   → f₀ [ Q ⟩ ↦ λ (s₁ : S₁) →
                     let Qs = proj₁ Q
                         s₀ = s₁ [ Qs ⟩
                         t₀ = f₀ s₀
                         Qt = proj₂ Q s₁ s₀ (s₁ ∥ Qs)
                     in  t₀ [ Qt ⟩
{-# REWRITE coerce-Π #-}

postulate ⊥-eta : (z₀ z₁ : ⊥) → ⊥ ∋ z₀ == ⊥ ∋ z₁ ↦ ⊤
{-# REWRITE ⊥-eta #-}

postulate ⊤-eta : (u₀ u₁ : ⊤) → ⊤ ∋ u₀ == ⊤ ∋ u₁ ↦ ⊤
{-# REWRITE ⊤-eta #-}

postulate true-true : Bool ∋ true == Bool ∋ true ↦ ⊤
{-# REWRITE true-true #-}

postulate true-false : Bool ∋ true == Bool ∋ false ↦ ⊥
{-# REWRITE true-false #-}

postulate false-true : Bool ∋ false == Bool ∋ true ↦ ⊥
{-# REWRITE false-true #-}

postulate false-false : Bool ∋ false == Bool ∋ false ↦ ⊤
{-# REWRITE false-false #-}

postulate function-equality : ∀ S₀ T₀ S₁ T₁ f₀ f₁
                            → Π S₀ T₀ ∋ f₀ == Π S₁ T₁ ∋ f₁
                            ↦ ∀ x₀ x₁ → S₀ ∋ x₀ == S₁ ∋ x₁ → T₀ x₀ ∋ f₀ x₀ == T₁ x₁ ∋ f₁ x₁
{-# REWRITE function-equality #-}

postulate pair-equality : ∀ S₀ T₀ S₁ T₁ p₀ p₁
                        → Σ S₀ T₀ ∋ p₀ == Σ S₁ T₁ ∋ p₁
                        ↦ (S₀ ∋ proj₁ p₀ == S₁ ∋ proj₁ p₁) × (T₀ (proj₁ p₀) ∋ proj₂ p₀ == T₁ (proj₁ p₁) ∋ proj₂ p₁)
{-# REWRITE pair-equality #-}

postulate bar : ∀ {S} (s : S) → S ∋ s == S ∋ s

postulate R : ∀ S (T : S → Set) (y z : S) → S ∋ y == S ∋ z → T y == T z

type-refl : ∀ S → S == S
type-refl S = R ⊤ (λ _ → S) tt tt tt

postulate _||_ : ∀ {A B C D} → A == C → B == D → (A == B) == (C == D)

postulate _,_||_,_ : ∀ {A B C D a b c d}
                   → A == C → A ∋ a == C ∋ c → B == D → B ∋ b == D ∋ d
                   → (A ∋ a == B ∋ b) == (C ∋ c == D ∋ d)

type-sym : ∀ {X Y} → X == Y → Y == X
type-sym {X} {Y} Q = type-refl X [ _||_ {A = X} Q (type-refl X) ⟩

type-trans : ∀ {X Y Z} → X == Y → Y == Z → X == Z
type-trans {X} {Y} {Z} Q R = Q [ _||_ {A = X} (type-refl X) R ⟩