indexsource

open import Agda.Primitive renaming (Set to Type; Setω to Typeω)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Axiom.Extensionality.Propositional
{-# BUILTIN REWRITE _≡_ #-}

-- Investigating the erasure modality. See also ErasureOpen
module Erasure where

private variable
  a b : Level
  A : Type a

-- The erased path induction principle J₀

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

-- The Erased monadic modality

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 ]

-- Paths (Erased A) → Erased (Paths A)
erased-cong :  {a} {@0 A : Type a} {@0 x y : A}  [ x ]  [ y ]  Erased (x  y)
erased-cong p = [ cong erased p ]

-- Erased (Paths A) → Paths (Erased A) ("erasure extensionality")
[]-cong-type =  {a} {@0 A : Type a} {@0 x y : A}  Erased (x  y)  [ x ]  [ y ]

-- J₀ and []-cong (with their respective computation rules) are interderivable

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 #-}

  --                        []-cong                        μ
  -- Erased (Paths (Erased A)) → Paths (Erased (Erased A)) → Paths (Erased A)
  stable-≡ :  {@0 A : Type a} {x y : Erased A}  Erased (x  y)  x  y
  stable-≡ p = cong μ ([]-cong p)

  --         η               []-cong          erased-cong
  -- Paths A → Erased (Paths A) → Paths (Erased A) → Erased (Paths A)
  --           Erased (Paths A)           →          Erased (Paths A)
  --                                      id
  []-cong-section'
    :  {@0 A : Type a} {@0 x y : A} (p : x  y)
     erased-cong ([]-cong (η p))  η p
  []-cong-section' refl = refl

  -- We can cancel out η by unique elimination and stability of paths in Erased
  []-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

-- Function extensionality implies erasure extensionality
module funext→[]-cong where
  postulate
    funext :  {a b}  Extensionality a b

  -- Direct proof, extracted from "Logical properties of a modality for erasure" (Danielsson 2019)

  -- id : Paths (Erased A) → Paths (Erased A)
  --    → {funext}
  --      Paths (Paths (Erased A) → Erased A)
  --    → {uniquely eliminating}
  --      Paths (Erased (Paths (Erased A)) → Erased A)
  --    → {apply p}
  --      Paths (Erased A)
  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))

  --                  η                        stable-≡
  -- Erased (Paths A) → Erased (Paths (Erased A)) → Paths (Erased A)
  []-cong : []-cong-type
  []-cong [ p ] = stable-≡ [ cong η p ]

  -- Alternative proof: ignoring some details, the types of funext and []-cong look very similar:
  --   funext  : Functions (Paths A) → Paths (Functions A)
  --   []-cong : Erased    (Paths A) → Paths (Erased    A)
  --
  -- If we have inductive types with erased constructors, then we can
  -- present erasure as an *open modality* generated by the subterminal
  -- object with a single erased point (see ErasureOpen):

  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

  -- We don't actually need this
  ○→E→○ : {A :  Type a}  (f : ○' A)  E→○ (○→E f)  f
  ○→E→○ f = funext (E→○ [ refl {x = f compiling} ])

  -- Since Erased is (equivalent to) a function type, erasure extensionality/[]-cong
  -- is a special case of function extensionality:
  --
  --                                       funext
  -- Erased (Paths A) ≃ (Compiling → Paths A) → Paths (Compiling → A) ≃ Paths (Erased A)
  []-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)