open import Agda.Primitive renaming (Set to Type; Setω to Typeω)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Axiom.Extensionality.Propositional
{-# BUILTIN REWRITE _≡_ #-}
module Erasure where
private variable
a b : Level
A : Type a
J₀-type =
∀ {a b} {@0 A : Type a} {@0 x : A} (B : (@0 y : A) → @0 x ≡ y → Type b)
→ {@0 y : A} (@0 p : x ≡ y) → B x refl → B y p
record Erased (@0 A : Type a) : Type a where
constructor [_]
field
@0 erased : A
open Erased
η : {@0 A : Type a} → A → Erased A
η x = [ x ]
μ : {@0 A : Type a} → Erased (Erased A) → Erased A
μ [ [ x ] ] = [ x ]
erased-cong : ∀ {a} {@0 A : Type a} {@0 x y : A} → [ x ] ≡ [ y ] → Erased (x ≡ y)
erased-cong p = [ cong erased p ]
[]-cong-type = ∀ {a} {@0 A : Type a} {@0 x y : A} → Erased (x ≡ y) → [ x ] ≡ [ y ]
module J₀→[]-cong where
postulate
J₀ : J₀-type
J₀-refl
: ∀ {a b} {@0 A : Type a} {@0 x : A} (B : (@0 y : A) → @0 x ≡ y → Type b) (r : B x refl)
→ J₀ B refl r ≡ r
{-# REWRITE J₀-refl #-}
[]-cong : []-cong-type
[]-cong {x} [ p ] = J₀ (λ y _ → [ x ] ≡ [ y ]) p refl
[]-cong-refl
: ∀ {a} {@0 A : Type a} {@0 x : A}
→ []-cong {x = x} [ refl ] ≡ refl
[]-cong-refl = refl
module []-cong→J₀ where
postulate
[]-cong : []-cong-type
[]-cong-refl
: ∀ {a} {@0 A : Type a} {@0 x : A}
→ []-cong {x = x} [ refl ] ≡ refl
{-# REWRITE []-cong-refl #-}
stable-≡ : ∀ {@0 A : Type a} {x y : Erased A} → Erased (x ≡ y) → x ≡ y
stable-≡ p = cong μ ([]-cong p)
[]-cong-section'
: ∀ {@0 A : Type a} {@0 x y : A} (p : x ≡ y)
→ erased-cong ([]-cong (η p)) ≡ η p
[]-cong-section' refl = refl
[]-cong-section
: ∀ {@0 A : Type a} {@0 x y : A} (@0 p : x ≡ y)
→ erased-cong ([]-cong [ p ]) ≡ [ p ]
[]-cong-section p = stable-≡ [ []-cong-section' p ]
J₀ : J₀-type
J₀ B {y} p r = subst (λ ([ p ]) → B y p) ([]-cong-section p) b'
where
b' : B y (cong erased ([]-cong [ p ]))
b' = J (λ ([ y ]) p → B y (cong erased p)) ([]-cong [ p ]) r
J₀-refl
: ∀ {a b} {@0 A : Type a} {@0 x : A} (B : (@0 y : A) → @0 x ≡ y → Type b) (r : B x refl)
→ J₀ B refl r ≡ r
J₀-refl B r = refl
module funext→[]-cong where
postulate
funext : ∀ {a b} → Extensionality a b
stable-≡ : ∀ {@0 A : Type a} {x y : Erased A} → Erased (x ≡ y) → x ≡ y
stable-≡ {A} {x} {y} [ p ] =
cong (λ (f : x ≡ y → Erased A) → [ f p .erased ])
(funext (λ (p : x ≡ y) → p))
[]-cong : []-cong-type
[]-cong [ p ] = stable-≡ [ cong η p ]
data Compiling : Type where
@0 compiling : Compiling
○_ : Type a → Type a
○ A = Compiling → A
○'_ : ○ Type a → Type a
○' A = (n : Compiling) → A n
E→○ : {A : ○ Type a} → Erased (A compiling) → ○' A
E→○ a compiling = a .erased
○→E : {A : ○ Type a} → ○' A → Erased (A compiling)
○→E f .erased = f compiling
E→○→E : {A : ○ Type a} → (a : Erased (A compiling)) → ○→E (E→○ {A = A} a) ≡ a
E→○→E _ = refl
○→E→○ : {A : ○ Type a} → (f : ○' A) → E→○ (○→E f) ≡ f
○→E→○ f = funext (E→○ [ refl {x = f compiling} ])
[]-cong' : []-cong-type
[]-cong' {A} {x} {y} p = cong ○→E x'≡y'
where
x' y' : ○' E→○ [ A ]
x' = E→○ [ x ]
y' = E→○ [ y ]
x'≡y' : x' ≡ y'
x'≡y' = funext (E→○ p)