simple-bracket.agda

module simple-bracket where
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

record PCA : Set₁ where
  constructor mk-pca
  field
    A   : Set
    _≈_ : A → A → Set
    s   : A
    k   : A
    i   : A
    _·_ : A → A → A
    id     : ∀ {a} → i · a ≈ a
    k-term : ∀ {a} → k · a ≈ k · a
    k-ap   : ∀ {a b} → (k · a) · b ≈ a
    s-term : ∀ {a b} → (s · a) · b ≈ (s · a) · b
    s-ap   : ∀ {a b c} → ((s · a) · b) · c ≈ (a · c) · (b · c)
    apcong : ∀ {a b c d} → a ≈ c → b ≈ d → a · b ≈ c · d
    ≈sym   : ∀ {a b} → a ≈ b → b ≈ a
    ≈trans : ∀ {a b c} → a ≈ b → b ≈ c → a ≈ c
  infix 3 _≈_
  infixl 5 _·_

module NeedAPCA (P : PCA) where
  open PCA P

  data Term : Set where
    var : ℕ → Term
    ap : Term → Term → Term
    ι :  A → Term

  bracket : ℕ → Term → Term
  bracket n (var x) with n ≟ x
  ... | yes p = ι i
  ... | no ¬p = ap (ι k) (var x)
  bracket n (ap t t₁) = ap (ap (ι s) (bracket n t)) (bracket n t₁)
  bracket n (ι x) = ι (k · x)

  sub : Term → ℕ → Term → Term
  sub new v (var x) with v ≟ x
  ... | yes _ = new
  ... | no _ = var x
  sub new v (ap t t₁) = ap (sub new v t) (sub new v t₁)
  sub new v (ι x) = ι x

  close : (ℕ → A) → Term → A
  close σ (var x) = σ x
  close σ (ap t t₁) = close σ t · close σ t₁
  close σ (ι x) = x

  trivial-close : Term → A
  trivial-close = close (λ x → i)

  _≈t_ : Term → Term → Set
  t₁ ≈t t₂ = (σ : ℕ → A) → close σ t₁ ≈ close σ t₂

  bracket-works : (i : ℕ)(a b : Term) → ap (bracket i a) b ≈t sub b i a
  bracket-works i (var x) b σ with i ≟ x
  ... | yes refl = id
  ... | no ¬p = k-ap
  bracket-works i (ap a a₁) b σ =
    ≈trans s-ap (apcong (bracket-works i a b σ) (bracket-works i a₁ b σ))
  bracket-works i (ι x) b σ = k-ap

  pair : Term → Term → Term
  pair l r = bracket 0 (ap (ap (var 0) l) r)

  fst : Term
  fst = bracket 0 (ap (var 0) (bracket 1 (bracket 2 (var 1))))

  snd : Term
  snd = bracket 0 (ap (var 0) (bracket 1 (bracket 2 (var 2))))

  pair-fst-works : ∀ a b → a ≈ a → b ≈ b → ap fst (pair (ι a) (ι b)) ≈t ι a
  pair-fst-works a b aeq beq σ =
    ≈trans
      (bracket-works 0
        (ap (var 0) (bracket 1 (bracket 2 (var 1))))
        (pair (ι a) (ι b)) σ)
      (≈trans
        (bracket-works 0
          (ap (ap (var 0) (ι a)) (ι b))
          (bracket 1 (bracket 2 (var 1))) σ)
        (≈trans (apcong (bracket-works 1 (bracket 2 (var 1)) (ι a) σ) beq)
          (≈trans (bracket-works 2 (ι a) (ι b) σ) aeq)))

  pair-snd-works : ∀ a b → a ≈ a → b ≈ b → ap snd (pair (ι a) (ι b)) ≈t ι b
  pair-snd-works a b aeq beq σ =
    ≈trans
      (bracket-works 0
        (ap (var 0) (bracket 1 (bracket 2 (var 2))))
        (pair (ι a) (ι b)) σ)
      (≈trans
        (bracket-works 0
          (ap (ap (var 0) (ι a)) (ι b))
          (bracket 1 (bracket 2 (var 2))) σ)
        (≈trans (apcong (bracket-works 1 (bracket 2 (var 2)) (ι a) σ) beq)
          (≈trans (bracket-works 2 (var 2) (ι b) σ) beq)))
open NeedAPCA public