Test37.agda

{-# OPTIONS -vtac:10 --cubical -vtc.unquote.elaborate:50 #-}
module Test37 where

open import Agda.Builtin.Reflection
open import Agda.Primitive.Cubical
open import Agda.Builtin.Sigma
open import Agda.Builtin.Maybe
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Primitive

pattern argH x = arg (arg-info hidden (modality relevant quantity-ω)) x
pattern argN x = arg (arg-info visible (modality relevant quantity-ω)) x

data _≡ₛ_ {ℓ} {A : Set ℓ} (x : A) : A → SSet ℓ where
  reflₛ : x ≡ₛ x

postulate
  funextₛ : ∀ {ℓ ℓ′} {A : Set ℓ} {B : A → Set ℓ′} {f g : ∀ x → B x}
          → (∀ x → f x ≡ₛ g x)
          → f ≡ₛ g

Path : ∀ {ℓ} (A : Set ℓ) → A → A → Set ℓ
Path A x y = PathP (λ _ → A) x y

funext : ∀ {ℓ ℓ′} {A : Set ℓ} {B : A → Set ℓ′} {f g : ∀ x → B x}
       → (∀ x → PathP (λ _ → B x) (f x) (g x))
       → PathP (λ _ → ∀ x → B x) f g
funext f i x = f x i

_$_ : ∀ {ℓ ℓ′} {A : Set ℓ} {B : A → Set ℓ′} → (∀ x → B x) → ∀ x → B x
f $ x = f x

data Subst : Set where
  ids        : Subst
  _∷_        : Term → Subst → Subst
  wk         : Nat → Subst → Subst
  lift       : Nat → Subst → Subst
  strengthen : Nat → Subst → Subst

infixr 5 _∷_

wkS : Nat → Subst → Subst
wkS zero ρ = ρ
wkS n (wk x ρ) = wk (n + x) ρ
wkS n ρ        = wk n ρ

liftS : Nat → Subst → Subst
liftS zero ρ       = ρ
liftS n ids        = ids
liftS n (lift k ρ) = lift (n + k) ρ
liftS n ρ          = lift n ρ

_++#_ : List Term → Subst → Subst
[] ++# ρ = ρ
(x ∷ x₁) ++# ρ = x ∷ x₁ ++# ρ
infix 15 _++#_

raiseS : Nat → Subst
raiseS n = wk n ids

raise-fromS : Nat → Nat → Subst
raise-fromS n k = liftS n $ raiseS k

map : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

_++_ : ∀ {ℓ} {A : Set ℓ} → List A → List A → List A
[] ++ y = y
x ∷ x₁ ++ y = x ∷ (x₁ ++ y)
infixr 4 _++_

_<$>_ : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} → (A → B) → Maybe A → Maybe B
x <$> just x₁ = just (x x₁)
x <$> nothing = nothing

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Set ℓ₁} {B : A → Set ℓ₂} {C : (x : A) → B x → Set ℓ₃}
    → (∀ {x} → (y : B x) → C x y)
    → (f : ∀ x → B x)
    → ∀ x → C x (f x)
f ∘ g = λ z → f (g z)

infixr 40 _∘_

module maybe where
  _>>=_ : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} → Maybe A → (A → Maybe B) → Maybe B
  just x >>= f = f x
  nothing >>= f = nothing
  _>>_ : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} → Maybe A → Maybe B → Maybe B
  x >> y = x >>= λ _ → y

module _ where
  open maybe
  {-# TERMINATING #-}
  subst-tm  : Subst → Term → Maybe Term
  subst-tm* : Subst → List (Arg Term) → Maybe (List (Arg Term))
  apply-tm  : Term → Arg Term → Maybe Term

  raise : Nat → Term → Maybe Term
  raise n = subst-tm (raiseS n)

  subst-tm* ρ [] = just []
  subst-tm* ρ (arg ι x ∷ ls) = do
    x ← subst-tm ρ x
    (arg ι x ∷_) <$> subst-tm* ρ ls

  apply-tm* : Term → List (Arg Term) → Maybe Term
  apply-tm* tm [] = just tm
  apply-tm* tm (x ∷ xs) = do
    tm′ ← apply-tm tm x
    apply-tm* tm′ xs

  lookup-tm : (σ : Subst) (i : Nat) → Maybe Term
  lookup-tm ids i = just $ var i []
  lookup-tm (wk n ids) i = just $ var (i + n) []
  lookup-tm (wk n ρ) i = lookup-tm ρ i >>= subst-tm (raiseS n)
  lookup-tm (x ∷ ρ) i with (i == 0)
  … | true  = just x
  … | false = lookup-tm ρ (i - 1)
  lookup-tm (strengthen n ρ) i with (i < n)
  … | true = nothing
  … | false = lookup-tm ρ (i - n)
  lookup-tm (lift n σ) i with (i < n)
  … | true  = just $ var i []
  … | false = lookup-tm σ (i - n) >>= raise n

  apply-tm (var x args)      argu = just $ var x (args ++ argu ∷ [])
  apply-tm (con c args)      argu = just $ con c (args ++ argu ∷ [])
  apply-tm (def f args)      argu = just $ def f (args ++ argu ∷ [])
  apply-tm (lam v (abs n t)) (arg _ argu) = subst-tm (argu ∷ ids) t
  apply-tm (pat-lam cs args) argu = nothing
  apply-tm (pi a b)          argu = nothing
  apply-tm (agda-sort s)     argu = nothing
  apply-tm (lit l)           argu = nothing
  apply-tm (meta x args)     argu = just $ meta x (args ++ argu ∷ [])
  apply-tm unknown           argu = just unknown

  subst-tm ids tm = just tm
  subst-tm ρ (var i args) = do
    r ← lookup-tm ρ i
    es ← subst-tm* ρ args
    apply-tm* r es
  subst-tm ρ (con c args)      = con c <$> subst-tm* ρ args
  subst-tm ρ (def f args)      = def f <$> subst-tm* ρ args
  subst-tm ρ (meta x args)     = meta x <$> subst-tm* ρ args
  subst-tm ρ (pat-lam cs args) = nothing
  subst-tm ρ (lam v (abs n b)) = lam v ∘ abs n <$> subst-tm (liftS 1 ρ) b
  subst-tm ρ (pi (arg ι a) (abs n b)) = do
    a ← subst-tm ρ a
    b ← subst-tm (liftS 1 ρ) b
    just (pi (arg ι a) (abs n b))
  subst-tm ρ (lit l) = just (lit l)
  subst-tm ρ unknown = just unknown
  subst-tm ρ (agda-sort s) with s
  … | set t     = agda-sort ∘ set <$> subst-tm ρ t
  … | lit n     = just (agda-sort (lit n))
  … | prop t    = agda-sort ∘ prop <$> subst-tm ρ t
  … | propLit n = just (agda-sort (propLit n))
  … | inf n     = just (agda-sort (inf n))
  … | unknown   = just unknown

module TC where
  _>>=_ = bindTC
  _>>_ : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} → TC A → TC B → TC B
  x >> f = x >>= λ _ → f

data Strictness : Set where
  path sset : Strictness

pattern _`$_ f x = def (quote _$_) (argN f ∷ argN x ∷ [])

module _ where
  open maybe
  equate : Strictness → Type → Term → Term → Term
  equate path ty a b = def (quote Path) (argN ty ∷ argN a ∷ argN b ∷ [])
  equate sset ty a b = def (quote _≡ₛ_) (argH unknown ∷ argH ty ∷ argN a ∷ argN b ∷ [])

  fe : Strictness → Term → Term
  fe path go = def (quote funext) (argN go ∷ [])
  fe sset go = def (quote funextₛ) (argN go ∷ [])

  pushEquality
    : Strictness → Type → Term → Term → Maybe (Σ Term λ _ → Term → Maybe Term)
  pushEquality sn (pi a (abs n b)) f g = do
    f↑ ← raise 1 f
    g↑ ← raise 1 g
    (inner , f) ← pushEquality sn b (f↑ `$ var 0 []) (g↑ `$ var 0 [])

    let
      cont g = do
        g' ← raise 1 g
        g' ← apply-tm g' (argN (var 0 []))
        g' ← f g'
        just (fe sn (lam visible (abs "x" g')))
    just (pi a (abs n inner) , cont)
  pushEquality sn a x y = just (equate sn a x y , just)

module _ where
  open TC
  macro
    extensionality : PostponedTerm → Term → TC ⊤
    extensionality argu goal = (inferType goal >>= reduce) >>= λ where
      ty@(def (quote PathP) (argH _ ∷ argN (lam visible (abs _ bd)) ∷ argN x ∷ argN y ∷ [])) → do
        just bd ← returnTC (subst-tm (strengthen 1 ids) bd)
          where _ → typeError (strErr "Can not apply extensionality for genuinely dependent PathP" ∷ [])

        just (a , w) ← returnTC (pushEquality path bd x y)
          where _ → typeError (strErr "Failed to push endpoints inwards for type " ∷ termErr ty ∷ [])

        a ← onlyReduceDefs (quote _$_ ∷ []) (normalise a)
        worker ← elaborate argu a

        just worker ← returnTC (w worker)
          where _ → typeError []
        unify goal worker

      ty@(def (quote _≡ₛ_) (argH _ ∷ argH bd ∷ argN x ∷ argN y ∷ [])) → do
        just (a , w) ← returnTC (pushEquality sset bd x y)
          where _ → typeError (strErr "Failed to push endpoints inwards for type " ∷ termErr ty ∷ [])

        a ← onlyReduceDefs (quote _$_ ∷ []) (normalise a)
        worker ← elaborate argu a

        just worker ← returnTC (w worker)
          where _ → typeError []
        unify goal worker

      x → typeError (strErr "Not a supported equality type: " ∷ termErr x ∷ [])

module _
  {ℓ ℓ′ ℓ′′ : Level}
  {A : Set ℓ}
  {B : A → Set ℓ′}
  {C : ∀ x → B x → Set ℓ′′}
  {f g : ∀ x y → C x y}
  where

  _ : Path (∀ x y → C x y) f g
  _ = extensionality {!   !}

  _ : f ≡ₛ g
  _ = extensionality {!   !}