Created
November 13, 2020 08:23
-
-
Save jespercockx/745aea9fe90e7e291e7554f4295cd375 to your computer and use it in GitHub Desktop.
OTT in Agda using rewrite rules
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 #-} | |
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 ⟩ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment