text:
import cedille-options
open import general-util
module classify (options : cedille-options.options)
                {mF : Set → Set} ⦃ mFm : monad mF ⦄ (write-to-log : string → mF ⊤) where

open import cedille-types
open import constants
open import conversion
open import ctxt
open import datatype-util
open import elab-util options
open import free-vars
open import meta-vars options {mF} ⦃ mFm ⦄
open import rename
open import resugar
open import rewriting
open import spans options {mF} ⦃ mFm ⦄
open import subst
open import syntax-util
open import type-util
open import to-string options
open import untyped-spans options {mF} ⦃ mFm ⦄

span-error-t : Set
span-error-t = (string × 𝕃 tagged-val)

{-# TERMINATING #-}
check-term : ctxt → ex-tm → (T? : maybe type) → spanM (check-ret T? term)
check-type : ctxt → ex-tp → (k? : maybe kind) → spanM (check-ret k? type)
check-kind : ctxt → ex-kd → spanM kind
check-tpkd : ctxt → ex-tk → spanM tpkd
check-args : ctxt → ex-args → params → spanM args
check-let : ctxt → ex-def → erased? → posinfo → posinfo → spanM (ctxt × var × tagged-val × (∀ {ed : exprd} → ⟦ ed ⟧ → ⟦ ed ⟧) × (term → term))
check-mu : ctxt → posinfo → posinfo → var → ex-tm → maybe ex-tp → posinfo → ex-cases → posinfo → (T? : maybe type) → spanM (check-ret T? term)
check-sigma : ctxt → posinfo → maybe ex-tm → ex-tm → maybe ex-tp → posinfo → ex-cases → posinfo → (T? : maybe type) → spanM (check-ret T? term)
get-datatype-info-from-head-type : ctxt → var → 𝕃 tmtp → spanM (span-error-t ⊎ datatype-info)
check-sigma-evidence : ctxt → maybe ex-tm → var → 𝕃 tmtp → spanM (span-error-t ⊎ (term × (term → term) × datatype-info))

check-cases : ctxt → ex-cases → (Dₓ : var) → (ctrs : trie type) → renamectxt → (ctr-ps : args) → (drop-as : ℕ) → type → (ctxt → term → type → term) → (ctxt → type → kind → type) → spanM (cases × err-m)
check-case : ctxt → ex-case → (earlier : stringset) → (Dₓ : var) → (ctrs : trie (type × params × 𝕃 tmtp)) → renamectxt → (ctr-ps : args) → (drop-as : ℕ) → type → (ctxt → term → type → term) → (ctxt → type → kind → type) → spanM (case × trie (type × params × 𝕃 tmtp))
check-refinement : ctxt → type → kind → spanM (type × 𝕃 tagged-val × err-m)

synth-tmtp' : ∀ {b X} → ctxt → if b then ex-tm else ex-tp → (if b then term else type → if b then type else kind → spanM X) → spanM X
synth-tmtp' {tt} Γ t f = check-term Γ t nothing >>= uncurry f
synth-tmtp' {ff} Γ T f = check-type Γ T nothing >>= uncurry f

check-tmtp' : ∀ {b X} → ctxt → if b then ex-tm else ex-tp → if b then type else kind → (if b then term else type → spanM X) → spanM X
check-tmtp' {tt} Γ t T f = check-term Γ t (just T) >>= f
check-tmtp' {ff} Γ T k f = check-type Γ T (just k) >>= f

check-tpkd' : ∀ {b X} → ctxt → if b then ex-kd else ex-tk → (if b then kind else tpkd → spanM X) → spanM X
check-tpkd' {tt} Γ k f = check-kind Γ k >>= f
check-tpkd' {ff} Γ k f = check-tpkd Γ k >>= f

lambda-bound-conv? : ctxt → var → tpkd → tpkd → 𝕃 tagged-val → 𝕃 tagged-val × err-m
lambda-bound-conv? Γ x tk tk' ts with conv-tpkd Γ tk tk'
...| tt = ts , nothing
...| ff =
  (to-string-tag-tk "declared classifier" Γ tk' ::
   to-string-tag-tk "expected classifier" Γ tk :: ts) ,
  just "The classifier given for a λ-bound variable is not the one we expected"

id' = id

hnf-of : ∀ {X : Set} {ed} → ctxt → ⟦ ed ⟧ → (⟦ ed ⟧ → X) → X
hnf-of Γ t f = f (hnf Γ unfold-head-elab t)

-- "⊢" = "\vdash" or "\|-"
-- "⇒" = "\r="
-- "⇐" = "\l="
infixr 2 hnf-of id' check-tpkd' check-tmtp' synth-tmtp'
syntax synth-tmtp' Γ t (λ t~ → f) = Γ ⊢ t ↝ t~ ⇒ f
syntax check-tmtp' Γ t T f = Γ ⊢ t ⇐ T ↝ f
syntax check-tpkd' Γ k f = Γ ⊢ k ↝ f
syntax id' (λ x → f) = x / f -- Supposed to look like a horizontal bar (as in typing rules)
syntax hnf-of Γ t f = Γ ⊢ t =β= f

-- t [-]t'
check-term Γ (ExApp t e t') Tₑ? =
  check-term-spine Γ (ExApp t e t') (proto-maybe Tₑ?) tt
    on-fail return-when (Hole (term-start-pos t)) (TpHole (term-start-pos t))
    >>=m (uncurry return-when ∘ check-term-spine-elim Γ)
  where open import type-inf options {mF} check-term check-type

-- t ·T
check-term Γ (ExAppTp tₕ Tₐ) Tₑ? =
-- "Γ ⊢ tₕ ↝ tₕ~ ⇒ Tₕ~ /" desugars to "synth-tmtp' Γ tₕ λ tₕ~ Tₕ~ →"
  Γ ⊢ tₕ ↝ tₕ~ ⇒ Tₕ~ /
  Γ ⊢ Tₕ~ =β= λ where
    (TpAbs tt x (Tkk kₐ) Tᵣ) →
      Γ ⊢ Tₐ ⇐ kₐ ↝ Tₐ~ /
      let Tᵣ = [ Γ - Tₐ~ / x ] Tᵣ in
      [- AppTp-span tt (term-start-pos tₕ) (type-end-pos Tₐ) (maybe-to-checking Tₑ?)
           (head-type Γ Tₕ~ :: type-data Γ Tᵣ :: expected-type-if Γ Tₑ?)
           (check-for-type-mismatch-if Γ "synthesized" Tₑ? Tᵣ) -]
      return-when (AppTp tₕ~ Tₐ~) Tᵣ
    Tₕ'~ →
      untyped-type Γ Tₐ >>= λ Tₐ~ →
      [- AppTp-span tt (term-start-pos tₕ) (type-end-pos Tₐ) (maybe-to-checking Tₑ?)
           (head-type Γ Tₕ'~ :: arg-type Γ Tₐ~ :: expected-type-if Γ Tₑ?)
           (unless (is-hole Tₕ'~)
              ("The type synthesized from the head does not allow it to be applied" ^
               " to a type argument")) -]
      return-when (AppTp tₕ~ Tₐ~) (TpHole (term-start-pos tₕ))

-- β[<t?>][{t?'}]
check-term Γ (ExBeta pi t? t?') Tₑ? =
  maybe-map (λ {(PosTm t _) → untyped-term Γ t}) t?  >>=? λ t?~  →
  maybe-map (λ {(PosTm t _) → untyped-term Γ t}) t?' >>=? λ t?'~ →
  let t'~ = maybe-else' t?'~ id-term id
      e-t~ = maybe-else' Tₑ?
        (maybe-else' t?~
          (inj₁ ([] , "When synthesizing, specify what equality to prove with β<...>"))
          (λ t → inj₂ (t , nothing)))
        λ Tₑ → Γ ⊢ Tₑ =β= λ where
          (TpEq t₁ t₂) →
            if conv-term Γ t₁ t₂
              then maybe-else' (t?~ >>= λ t~ → check-for-type-mismatch Γ "computed"
                                    (TpEq t~ t~) (TpEq t₁ t₂) >>= λ e → just (e , t~))
                     (inj₂ (t₁ , just t₂))
                     (uncurry λ e t~ → inj₁ ([ type-data Γ (TpEq t~ t~) ] , e))
              else inj₁ ([] , "The two terms in the equation are not β-equal")
          Tₕ → inj₁ ([] , "The expected type is not an equation")
      e? = either-else' e-t~ (map-snd just) λ _ → [] , nothing
      fₓ = fresh-var Γ "x"
      t~T~ = either-else' e-t~ (λ _ → Hole pi , TpEq (Hole pi) (Hole pi))
             $ uncurry λ t₁ → maybe-else (Beta t₁ t'~ , TpEq t₁ t₁)
                                λ t₂ → (Beta t₁ t'~) , TpEq t₁ t₂ in
  [- uncurry (λ tvs → Beta-span pi (term-end-pos (ExBeta pi t? t?')) (maybe-to-checking Tₑ?)
         (expected-type-if Γ Tₑ? ++ tvs)) e? -]
  uncurry return-when t~T~

-- χ [T?] - t
check-term Γ (ExChi pi T? t) Tₑ? =
  (maybe-else' T?
    (check-term Γ t nothing)
    λ T → Γ ⊢ T ⇐ KdStar ↝ T~ /
          Γ ⊢ t ⇐ T~ ↝ t~ /
          return2 t~ T~
  ) >>= uncurry λ t~ T~ →
  [- Chi-span Γ pi (just T~) t (maybe-to-checking Tₑ?)
       (type-data Γ T~ :: expected-type-if Γ Tₑ?)
       (check-for-type-mismatch-if Γ
         (maybe-else' T? "synthesized" (const "computed")) Tₑ? T~) -]
  return-when t~ T~

-- δ [T?] - t
check-term Γ (ExDelta pi T? t) Tₑ? =
  Γ ⊢ t ↝ t~ ⇒ Tcontra /
  maybe-else' T?
    (return (maybe-else' Tₑ? (TpAbs Erased "X" (Tkk KdStar) (TpVar "X")) id))
    (λ T → Γ ⊢ T ⇐ KdStar ↝ return) >>= λ T~' →
  let b = Γ ⊢ Tcontra =β= λ {(TpEq t₁ t₂) → when (inconv Γ t₁ t₂) (t₁ , t₂); _ → nothing}
      b? = unless (conv-type Γ Tcontra (TpEq tt-term ff-term)) triv >> b in
  [- Delta-span pi t (maybe-to-checking Tₑ?)
      (to-string-tag "the contradiction" Γ Tcontra ::
       type-data Γ T~' :: expected-type-if Γ Tₑ?)
       (maybe-not b >> just
         "We could not find a contradiction in the synthesized type of the subterm") -]
  return-when (Delta b? T~' t~) T~'

-- ε[lr][-?] t
check-term Γ (ExEpsilon pi lr -? t) Tₑ? =
  let hnf-from = if -? then hanf Γ tt else hnf Γ unfold-head
      update-eq : term → term → type
      update-eq = λ t₁ t₂ → uncurry TpEq $ maybe-else' lr (hnf-from t₁ , hnf-from t₂) λ lr →
                    if lr then (t₁ , hnf-from t₂) else (hnf-from t₁ , t₂) in
  case-ret {m = Tₑ?}
    (Γ ⊢ t ↝ t~ ⇒ T~ /
     Γ ⊢ T~ =β= λ where
       (TpEq t₁ t₂) →
         let Tᵣ = update-eq t₁ t₂ in
         [- Epsilon-span pi lr -? t (maybe-to-checking Tₑ?) [ type-data Γ Tᵣ ] nothing -]
         return2 t~ Tᵣ
       Tₕ →
         [- Epsilon-span pi lr -? t (maybe-to-checking Tₑ?)
              [ to-string-tag "synthesized type" Γ Tₕ ]
              (unless (is-hole Tₕ)
                 "The synthesized type of the body is not an equation") -]
         return2 t~ Tₕ)
    λ Tₑ → Γ ⊢ Tₑ =β= λ where
      (TpEq t₁ t₂) →
        [- Epsilon-span pi lr -? t (maybe-to-checking Tₑ?)
             [ expected-type Γ (TpEq t₁ t₂) ] nothing -]
        Γ ⊢ t ⇐ update-eq t₁ t₂ ↝ return
      Tₕ →
        [- Epsilon-span pi lr -? t (maybe-to-checking Tₑ?) [ expected-type Γ Tₕ ]
             (unless (is-hole Tₕ) "The expected type is not an equation") -]
        untyped-term Γ t

-- ●
check-term Γ (ExHole pi) Tₑ? =
  [- hole-span Γ pi Tₑ? (maybe-to-checking Tₑ?) [] -]
  return-when (Hole pi) (TpHole pi)

-- [ t₁ , t₂ [@ Tₘ,?] ]
check-term Γ (ExIotaPair pi t₁ t₂ Tₘ? pi') Tₑ? =
  maybe-else' {B = spanM (err-m × 𝕃 tagged-val × term × term × term × type)} Tₑ?
    (maybe-else' Tₘ?
       (untyped-term Γ t₁ >>= λ t₁~ →
        untyped-term Γ t₂ >>= λ t₂~ →
        return (just "Iota pairs require a specified type when synthesizing" , [] ,
                t₁~ , t₁~ , t₂~ , TpHole pi))
       λ {(ExGuide pi'' x T₂) →
            Γ ⊢ t₁ ↝ t₁~ ⇒ T₁~ /
            (Γ , pi'' - x :` Tkt T₁~) ⊢ T₂ ⇐ KdStar ↝ T₂~ /
            Γ ⊢ t₂ ⇐ [ Γ - t₁~ / (pi'' % x) ] T₂~ ↝ t₂~ /
            let T₂~ = [ Γ - Var x / (pi'' % x) ] T₂~
                bd = binder-data Γ pi'' x (Tkt T₁~) ff nothing
                       (type-start-pos T₂) (type-end-pos T₂) in
            [- Var-span Γ pi'' x checking [ type-data Γ T₁~ ] nothing -]
            return (nothing , (type-data Γ (TpIota x T₁~ T₂~) :: [ bd ]) ,
                    IotaPair t₁~ t₂~ x T₂~ , t₁~ , t₂~ , TpIota x T₁~ T₂~)})
    (λ Tₑ → Γ ⊢ Tₑ =β= λ where
      (TpIota x T₁ T₂) →
        Γ ⊢ t₁ ⇐ T₁ ↝ t₁~ /
        maybe-else' Tₘ?
          (Γ ⊢ t₂ ⇐ [ Γ - t₁~ / x ] T₂ ↝ t₂~ /
           return (nothing , (type-data Γ (TpIota x T₁ T₂) :: [ expected-type Γ Tₑ ]) ,
                   IotaPair t₁~ t₂~ x T₂ , t₁~ , t₂~ , TpIota x T₁ T₂))
          λ {(ExGuide pi'' x' Tₘ) →
               (Γ , pi'' - x' :` Tkt T₁) ⊢ Tₘ ⇐ KdStar ↝ Tₘ~ /
               let Tₘ~ = [ Γ - Var x' / (pi'' % x') ] Tₘ~
                   T₂ = [ Γ - Var x' / x ] T₂
                   Tₛ = TpIota x' T₁ Tₘ~ in
               Γ ⊢ t₂ ⇐ [ Γ - t₁~ / x' ] Tₘ~ ↝ t₂~ /
               [- Var-span Γ pi'' x checking [ type-data Γ T₁ ] nothing -]
               return (check-for-type-mismatch Γ "computed" Tₘ~ T₂ ,
                       (type-data Γ Tₛ :: expected-type Γ (TpIota x' T₁ T₂) ::
                        [ binder-data Γ pi'' x' (Tkt T₁) ff nothing
                            (type-start-pos Tₘ) (type-end-pos Tₘ) ]) ,
                       IotaPair t₁~ t₂~ x' Tₘ~ , t₁~ , t₂~ , Tₛ)}
      Tₕ →
        untyped-term Γ t₁ >>= λ t₁~ →
        untyped-term Γ t₂ >>= λ t₂~ →
        return (unless (is-hole Tₕ) "The expected type is not an iota-type" ,
                [ expected-type Γ Tₕ ] , t₁~ , t₁~ , t₂~ , Tₕ)) >>= λ where
    (err? , tvs , t~ , t₁~ , t₂~ , T~) →
      let conv-e = "The two components of the iota-pair are not convertible (as required)"
          conv-e? = unless (conv-term Γ t₁~ t₂~) conv-e
          conv-tvs = maybe-else' conv-e? [] λ _ →
              to-string-tag "hnf of the first component"  Γ (hnf Γ unfold-head t₁~) ::
            [ to-string-tag "hnf of the second component" Γ (hnf Γ unfold-head t₂~) ] in
      [- IotaPair-span pi pi' (maybe-to-checking Tₑ?) (conv-tvs ++ tvs)
           (conv-e? ||-maybe err?) -]
      return-when t~ T~

-- t.(1 / 2)
check-term Γ (ExIotaProj t n pi) Tₑ? =
  Γ ⊢ t ↝ t~ ⇒ T~ /
  let n? = case n of λ {"1" → just ι1; "2" → just ι2; _ → nothing} in
  maybe-else' n?
    ([- IotaProj-span t pi (maybe-to-checking Tₑ?) (expected-type-if Γ Tₑ?)
          (just "Iota-projections must use .1 or .2 only") -]
     return-when t~ (TpHole pi)) λ n →
    Γ ⊢ T~ =β= λ where
      (TpIota x T₁ T₂) →
        let Tᵣ = if n iff ι1 then T₁ else ([ Γ - t~ / x ] T₂) in
        [- IotaProj-span t pi (maybe-to-checking Tₑ?)
             (type-data Γ Tᵣ :: expected-type-if Γ Tₑ?)
             (check-for-type-mismatch-if Γ "synthesized" Tₑ? Tᵣ) -]
        return-when (IotaProj t~ n) Tᵣ
      Tₕ~ →
        [- IotaProj-span t pi (maybe-to-checking Tₑ?)
             (head-type Γ Tₕ~ :: expected-type-if Γ Tₑ?)
             (unless (is-hole Tₕ~)
                "The synthesized type of the head is not an iota-type") -]
        return-when (IotaProj t~ n) (TpHole pi)

-- λ/Λ x [: T?]. t
check-term Γ (ExLam pi e pi' x tk? t) Tₑ? =
  [- punctuation-span "Lambda" pi (posinfo-plus pi 1) -]
  let erase-err : (exp act : erased?) → tpkd → term → err-m × 𝕃 tagged-val
      erase-err = λ where
        Erased NotErased tk t →
          just ("The expected type is a ∀-abstraction (implicit input), " ^
                "but the term is a λ-abstraction (explicit input)") , []
        NotErased Erased tk t →
          just ("The expected type is a Π-abstraction (explicit input), " ^
                "but the term is a Λ-abstraction (implicit input)") , []
        Erased Erased tk t →
          maybe-else (nothing , []) (λ e-tv → just (fst e-tv) , [ snd e-tv ])
            (trie-lookup (free-vars (erase t)) x >>
             just ("The Λ-bound variable occurs free in the erasure of the body" ,
                   erasure Γ t))
        NotErased NotErased (Tkk _) t →
          just "λ-terms must bind a term, not a type (use Λ instead)" , []
        NotErased NotErased (Tkt _) t →
          nothing , [] in
  case-ret {m = Tₑ?}
    (maybe-else' tk?
      (untyped-term (Γ , pi' - x :` Tkt (TpHole pi')) t >>= λ t~ →
       [- Lam-span Γ synthesizing pi pi' e x (Tkt (TpHole pi')) t []
           (just ("We are not checking this abstraction against a type, " ^
                  "so a classifier must be given for the bound variable " ^ x)) -]
       return2 (Lam e x nothing (rename-var Γ (pi' % x) x t~)) (TpHole pi'))
      λ tk →
        Γ ⊢ tk ↝ tk~ /
        (Γ , pi' - x :` tk~) ⊢ t ↝ t~ ⇒ T~ /
        let T~ = rename-var Γ (pi' % x) x T~
            t~ = rename-var Γ (pi' % x) x t~
            Tᵣ = TpAbs e x tk~ T~ in
        [- var-span e (Γ , pi' - x :` tk~) pi' x checking tk~ nothing -]
        [- uncurry (λ tvs → Lam-span Γ synthesizing pi pi' e x tk~ t
               (type-data Γ Tᵣ :: tvs)) (twist-× (erase-err e e tk~ t~)) -]
        return2 (Lam e x (just tk~) t~) Tᵣ)
    λ Tₑ → Γ ⊢ Tₑ =β= λ where
      (TpAbs e' x' tk T) →
        maybe-map (check-tpkd Γ) tk? >>=? tk~? /
        let tk~ = maybe-else' tk~? tk id in
        --maybe-else' tk? (return tk) (λ tk → Γ ⊢ tk ↝ return) >>= tk~ /
        (Γ , pi' - x :` tk~) ⊢ t ⇐ rename-var Γ x' (pi' % x) T ↝ t~ /
        let xₙ = if x =string ignored-var && is-free-in x' T then x' else x
            t~ = rename-var Γ (pi' % x) xₙ t~
            T = rename-var Γ x' xₙ T
            Tₛ = TpAbs e xₙ tk~ T
            Tₑ = TpAbs e' xₙ tk T
            vₑ = check-for-tpkd-mismatch-if Γ "computed" tk~? tk in
        [- var-span e (Γ , pi' - x :` tk~) pi' x (maybe-to-checking tk?) tk~ nothing -]
        [- uncurry (λ err tvs → Lam-span Γ checking pi pi' e x tk~ t
                 (type-data Γ Tₛ :: expected-type Γ Tₑ :: tvs) (err ||-maybe vₑ))
             (erase-err e' e tk~ t~) -]
        return (Lam e xₙ (just tk~) t~)
      Tₕ →
        maybe-else' tk? (return (Tkt (TpHole pi'))) (check-tpkd Γ) >>= tk~ /
        untyped-term (Γ , pi' - x :` tk~) t >>= t~ /
        [- Lam-span Γ checking pi pi' e x (Tkt (TpHole pi')) t
             [ expected-type Γ Tₕ ] (just "The expected type is not a ∀- or a Π-type") -]
        return (Lam e x (unless (is-hole -tk' tk~) tk~)
                 (rename-var Γ (pi' % x) x t~))

-- [d] - t
check-term Γ (ExLet pi e? d t) Tₑ? =
  check-let Γ d e? (term-start-pos t) (term-end-pos t) >>= λ where
    (Γ' , x , tv , σ , f) →
      case-ret-body {m = Tₑ?} (check-term Γ' t Tₑ?) λ t~ T~ →
      [- punctuation-span "Parens (let)" pi (term-end-pos t) -]
      [- Let-span e? pi (term-end-pos t) (maybe-to-checking Tₑ?)
           (maybe-else' Tₑ? (type-data Γ T~) (expected-type Γ) :: [ tv ])
           (when (e? && is-free-in x (erase t~))
              (unqual-local x ^ "occurs free in the body of the term")) -]
      return-when (f t~) (σ T~)

-- open/close x - t
check-term Γ (ExOpen pi o pi' x t) Tₑ? =
  let Γ? = ctxt-clarify-def Γ o x
      e? = maybe-not Γ? >> just (x ^ " does not have a definition that can be " ^
                                       (if o then "opened" else "closed")) in
  [- Var-span Γ pi' x (maybe-to-checking Tₑ?) [ not-for-navigation ] nothing -]
  [- Open-span o pi x t (maybe-to-checking Tₑ?) (expected-type-if Γ Tₑ?) e? -]
  check-term (maybe-else' Γ? Γ id) t Tₑ?

-- (t)
check-term Γ (ExParens pi t pi') Tₑ? =
  [- punctuation-span "Parens (term)" pi pi' -]
  check-term Γ t Tₑ?

-- φ t₌ - t₁ {t₂}
check-term Γ (ExPhi pi t₌ t₁ t₂ pi') Tₑ? =
  case-ret-body {m = Tₑ?} (check-term Γ t₁ Tₑ?) λ t₁~ T~ →
  untyped-term Γ t₂ >>= λ t₂~ →
  Γ ⊢ t₌ ⇐ TpEq t₁~ t₂~ ↝ t₌~ /
  [- Phi-span pi pi' (maybe-to-checking Tₑ?)
       [ maybe-else' Tₑ? (type-data Γ T~) (expected-type Γ)] nothing -]
  return-when (Phi t₌~ t₁~ t₂~) T~

-- ρ[+]<ns> t₌ [@ Tₘ?] - t
check-term Γ (ExRho pi ρ+ <ns> t₌ Tₘ? t) Tₑ? =
  Γ ⊢ t₌ ↝ t₌~ ⇒ T₌ /
  Γ ⊢ T₌ =β= λ where
    (TpEq t₁ t₂) →
      let tₗ = if isJust Tₑ? then t₁ else t₂
          tᵣ = if isJust Tₑ? then t₂ else t₁
          tvs = λ T~ Tᵣ → to-string-tag "equation" Γ (TpEq t₁ t₂) ::
                          maybe-else' Tₑ?
                            (to-string-tag "type of second subterm" Γ T~)
                            (expected-type Γ) ::
                          [ to-string-tag "rewritten type" Γ Tᵣ ] in
      maybe-else' Tₘ?
        (elim-pair (optNums-to-stringset <ns>) λ ns ns-e? →
         let x = fresh-var Γ "x"
             Γ' = ctxt-var-decl x Γ
             T-f = λ T → rewrite-type T Γ' ρ+ ns (just t₌~) tₗ x 0
             Tᵣ-f = fst ∘ T-f
             nn-f = snd ∘ T-f
             Tₚ-f = map-fst (post-rewrite Γ' x t₌~ tᵣ) ∘ T-f in
         maybe-else' Tₑ?
           (Γ ⊢ t ↝ t~ ⇒ T~ /
            return2 t~ T~)
           (λ Tₑ → Γ ⊢ t ⇐ fst (Tₚ-f Tₑ) ↝ t~ /
             return2 t~ Tₑ) >>=c λ t~ T~ →
         elim-pair (Tₚ-f T~) λ Tₚ nn →
         [- Rho-span pi t₌ t (maybe-to-checking Tₑ?) ρ+
              (inj₁ (fst nn)) (tvs T~ Tₚ) (ns-e? (snd nn)) -]
         return-when (Rho t₌~ x (erase (Tᵣ-f T~)) t~) Tₚ)
        λ where
          (ExGuide pi' x Tₘ) →
            [- Var-span Γ pi' x untyped [] nothing -]
            let Γ' = Γ , pi' - x :` Tkt (TpHole pi') in
            untyped-type Γ' Tₘ >>= λ Tₘ~ →
            let Tₘ~ = [ Γ' - Var x / (pi' % x) ] Tₘ~
                T' = [ Γ' - tₗ / x ] Tₘ~
                T'' = post-rewrite Γ' x t₌~ tᵣ (rewrite-at Γ' x (just t₌~) tt T' Tₘ~)
                check-str = if isJust Tₑ? then "computed" else "synthesized" in
            maybe-else' Tₑ?
              (check-term Γ t nothing)
              (λ Tₑ → Γ ⊢ t ⇐ T'' ↝ t~ /
                return2 t~ Tₑ) >>=c λ t~ T~ →
            [- Rho-span pi t₌ t (maybe-to-checking Tₑ?) ρ+ (inj₂ x) (tvs T~ T'')
                 (check-for-type-mismatch Γ check-str T' T~) -]
            return-when (Rho t₌~ x Tₘ~ t~) T''
    Tₕ →
      Γ ⊢ t ↝ t~ ⇒ λ T~ →
      [- Rho-span pi t₌ t (maybe-to-checking Tₑ?) ρ+ (inj₁ 1)
           (to-string-tag "type of first subterm" Γ Tₕ ::
            [ to-string-tag "type of second subterm" Γ T~ ])
           (unless (is-hole Tₕ)
              "We could not synthesize an equation from the first subterm") -]
      return-when t~ T~

-- ς t
check-term Γ (ExVarSigma pi t) Tₑ? =
  case-ret
    (Γ ⊢ t ↝ t~ ⇒ T /
     Γ ⊢ T =β= λ where
       (TpEq t₁ t₂) →
         [- VarSigma-span pi t synthesizing [ type-data Γ (TpEq t₂ t₁) ] nothing -]
         return2 (VarSigma t~) (TpEq t₂ t₁)
       Tₕ →
         [- VarSigma-span pi t synthesizing [ type-data Γ Tₕ ]
           (unless (is-hole Tₕ)
              "The synthesized type of the body is not an equation") -]
         return2 (VarSigma t~) Tₕ)
  λ Tₑ →
    Γ ⊢ Tₑ =β= λ where
      (TpEq t₁ t₂) →
        Γ ⊢ t ⇐ TpEq t₂ t₁ ↝ t~ /
        [- VarSigma-span pi t checking [ expected-type Γ (TpEq t₁ t₂) ] nothing -]
        return (VarSigma t~)
      Tₕ →
        [- VarSigma-span pi t checking [ expected-type Γ Tₕ ]
             (unless (is-hole Tₕ)
                "The expected type is not an equation") -]
        untyped-term Γ t

-- θ t ts
check-term Γ (ExTheta pi θ t ts) Tₑ? =
  case-ret {m = Tₑ?}
    ([- Theta-span Γ pi θ t ts synthesizing [] (just
            "Theta-terms can only be used when checking (and we are synthesizing here)") -]
     return2 (Hole pi) (TpHole pi))
    λ Tₑ →
      Γ ⊢ t ↝ t~ ⇒ T /
      let x = case hnf Γ unfold-head t~ of λ {(Var x) → x; _ → "x"}
          x' = fresh-var Γ x in
      Γ ⊢ T =β= λ where
        (TpAbs me x (Tkk kd) tp) →
          (case θ of λ where
            (AbstractVars vs) → either-else' (wrap-vars vs Tₑ) (return2 (TpHole pi) ∘ just) λ Tₘ → return2 Tₘ nothing
            Abstract → return2 (TpLam x' (Tkt T) (rename-var Γ x x' Tₑ)) nothing
            AbstractEq → return2 (TpLam x' (Tkt T) (TpAbs Erased ignored-var (Tkt (TpEq t~ (Var x'))) (rename-var Γ x x' Tₑ))) nothing) >>=c λ Tₘ e₁ →
          check-refinement Γ Tₘ kd >>=c λ Tₘ → uncurry λ tvs e₂ →
          let tp' = [ Γ - Tₘ / x ] tp in
          check-lterms ts (AppTp t~ Tₘ) tp' >>=c λ t~ T~ →
          let e₃ = check-for-type-mismatch Γ "synthesized" T~ Tₑ
              t~ = case θ of λ {AbstractEq → AppEr t~ (Beta (erase t~) id-term); _ → t~} in
          [- Theta-span Γ pi θ t ts checking
               (type-data Γ T~ :: expected-type Γ Tₑ :: tvs)
               (e₁ ||-maybe (e₂ ||-maybe e₃)) -]
          return t~
        Tₕ →
          [- Theta-span Γ pi θ t ts checking (head-type Γ Tₕ :: expected-type Γ Tₑ :: [])
               (unless (is-hole Tₕ) "The synthesized type of the head is not a type-forall") -]
          return (Hole pi)
  where
  check-lterms : 𝕃 lterm → term → type → spanM (term × type)
  check-lterms [] tm tp = return2 tm tp
  check-lterms (Lterm me t :: ts) tm tp =
    Γ ⊢ tp =β= λ where
      (TpAbs me' x (Tkt T) T') →
        Γ ⊢ t ⇐ T ↝ t~ /
        (if me iff me' then return triv else spanM-add
          (Theta-span Γ pi θ t [] checking [] (just "Mismatched erasure of theta arg"))) >>
        check-lterms ts (if me then AppEr tm t~ else App tm t~) ([ Γ - t~ / x ] T')
      Tₕ →
        (if is-hole Tₕ then id
          else [- Theta-span Γ pi θ t [] checking [ expected-type Γ Tₕ ]
                    (just "The expected type is not an arrow type") -]_)
        (untyped-term Γ t >>= λ t~ → check-lterms ts (if me then AppEr tm t~ else App tm t~) Tₕ)

  var-not-in-scope : var → string
  var-not-in-scope x =
    "We could not compute a motive from the given term because " ^
    "the abstracted variable " ^ x ^ " is not in scope"

  wrap-var : var → type → string ⊎ type
  wrap-var x T =
    let x' = fresh-var Γ x in
    maybe-else' (ctxt-lookup-tpkd-var Γ x)
      (inj₁ (var-not-in-scope x))
      λ {(qx , as , tk) → inj₂ (TpLam x' tk (rename-var Γ qx x' T))}
  wrap-vars : 𝕃 var → type → var ⊎ type
  wrap-vars [] T = inj₂ T
  wrap-vars (x :: xs) T = wrap-vars xs T >>= wrap-var x

  motive : var → var → type → type → theta → term → type
  motive x x' T T' Abstract t = TpLam x' (Tkt T') (rename-var Γ x x' T)
  motive x x' T T' AbstractEq t = TpLam x' (Tkt T') (TpAbs Erased ignored-var (Tkt (TpEq t (Var x'))) (rename-var Γ x x' T))
  motive x x' T T' (AbstractVars vs) t = T -- Shouldn't happen

-- μ(' / rec.) t [@ Tₘ?] {ms...}
check-term Γ (ExMu pi1 pi2 x t Tₘ? pi' ms pi'') Tₑ? =
  check-mu Γ pi1 pi2 x t Tₘ? pi' ms pi'' Tₑ?

check-term Γ (ExSigma pi t? t Tₘ? pi' ms pi'') Tₑ? =
  check-sigma Γ pi t? t Tₘ? pi' ms pi'' Tₑ?

-- x
check-term Γ (ExVar pi x) Tₑ? =
  maybe-else' (ctxt-lookup-term-var Γ x)
    ([- Var-span Γ pi x (maybe-to-checking Tₑ?)
          (expected-type-if Γ Tₑ?)
          (just "Missing a type for a term variable") -]
     return-when (Var x) (TpHole pi))
    λ {(qx , as , T) →
      [- Var-span Γ pi x (maybe-to-checking Tₑ?)
           (type-data Γ T :: expected-type-if Γ Tₑ?)
           (check-for-type-mismatch-if Γ "computed" Tₑ? T) -]
      return-when (apps-term (Var qx) as) T}

-- ∀/Π x : tk. T
check-type Γ (ExTpAbs pi e pi' x tk T) kₑ? =
  Γ ⊢ tk ↝ tk~ /
  (Γ , pi' - x :` tk~) ⊢ T ⇐ KdStar ↝ T~ /
  let T~ = rename-var Γ (pi' % x) x T~ in
  [- punctuation-span "Forall" pi (posinfo-plus pi 1) -]
  [- var-span ff (Γ , pi' - x :` tk~) pi' x checking tk~ nothing -]
  [- TpQuant-span Γ e pi pi' x tk~ T (maybe-to-checking kₑ?)
       (kind-data Γ KdStar :: expected-kind-if Γ kₑ?)
       (check-for-kind-mismatch-if Γ "computed" kₑ? KdStar) -]
  return-when (TpAbs e x tk~ T~) KdStar

-- ι x : T₁. T₂
check-type Γ (ExTpIota pi pi' x T₁ T₂) kₑ? =
  Γ ⊢ T₁ ⇐ KdStar ↝ T₁~ /
  (Γ , pi' - x :` Tkt T₁~) ⊢ T₂ ⇐ KdStar ↝ T₂~ /
  let T₂~ = rename-var Γ (pi' % x) x T₂~ in
  [- punctuation-span "Iota" pi (posinfo-plus pi 1) -]
  [- Var-span (Γ , pi' - x :` Tkt T₁~) pi' x checking [ type-data Γ T₁~ ] nothing -]
  [- Iota-span Γ pi pi' x T₁~ T₂ (maybe-to-checking kₑ?)
       (kind-data Γ KdStar :: expected-kind-if Γ kₑ?)
       (check-for-kind-mismatch-if Γ "computed" kₑ? KdStar) -]
  return-when (TpIota x T₁~ T₂~) KdStar

-- {^ T ^} (generated by theta)
check-type Γ (ExTpNoSpans T pi) kₑ? = check-type Γ T kₑ? >>=spand return

-- [d] - T
check-type Γ (ExTpLet pi d T) kₑ? =
  check-let Γ d ff (type-start-pos T) (type-end-pos T) >>= λ where
    (Γ' , x , tv , σ , f) →
      case-ret-body {m = kₑ?} (check-type Γ' T kₑ?) λ T~ k~ →
      [- punctuation-span "Parens (let)" pi (type-end-pos T) -]
      [- TpLet-span pi (type-end-pos T) (maybe-to-checking kₑ?)
           (maybe-else' kₑ? (kind-data Γ k~) (expected-kind Γ) :: [ tv ]) -]
      return-when (σ T~) (σ k~)

-- T · T'
check-type Γ (ExTpApp T T') kₑ? =
  Γ ⊢ T ↝ T~ ⇒ kₕ /
  Γ ⊢ kₕ =β= λ where
    (KdAbs x (Tkk dom) cod) →
      Γ ⊢ T' ⇐ dom ↝ T'~ /
      let cod' = [ Γ - T'~ / x ] cod in
      [- TpApp-span (type-start-pos T) (type-end-pos T') (maybe-to-checking kₑ?)
           (kind-data Γ cod' :: expected-kind-if Γ kₑ?)
           (check-for-kind-mismatch-if Γ "synthesized" kₑ? cod') -]
      return-when (TpAppTp T~ T'~) cod'
    kₕ' →
      untyped-type Γ T' >>= T'~ /
      [- TpApp-span (type-start-pos T) (type-end-pos T') (maybe-to-checking kₑ?)
           (head-kind Γ kₕ' :: expected-kind-if Γ kₑ?)
           (unless (is-hole kₕ') $
              "The synthesized kind of the head does not allow it to be applied" ^
              " to a type argument") -]
      return-when (TpAppTp T~ T'~) (KdHole (type-start-pos T))

-- T t
check-type Γ (ExTpAppt T t) kₑ? =
  Γ ⊢ T ↝ T~ ⇒ kₕ /
  Γ ⊢ kₕ =β= λ where
    (KdAbs x (Tkt dom) cod) →
      Γ ⊢ t ⇐ dom ↝ t~ /
      let cod' = [ Γ - t~ / x ] cod in
      [- TpAppt-span (type-start-pos T) (term-end-pos t) (maybe-to-checking kₑ?)
           (kind-data Γ cod' :: expected-kind-if Γ kₑ?)
           (check-for-kind-mismatch-if Γ "synthesized" kₑ? cod') -]
      return-when (TpAppTm T~ t~) cod'
    kₕ' →
      untyped-term Γ t >>= t~ /
      [- TpAppt-span (type-start-pos T) (term-end-pos t) (maybe-to-checking kₑ?)
           (head-kind Γ kₕ' :: expected-kind-if Γ kₑ?)
           (unless (is-hole kₕ') $
              "The synthesized kind of the head does not allow it to be applied" ^
              " to a term argument") -]
      return-when (TpAppTm T~ t~) (KdHole (type-start-pos T))

-- T ➔/➾ T'
check-type Γ (ExTpArrow T e T') kₑ? =
  Γ ⊢ T ⇐ KdStar ↝ T~ /
  Γ ⊢ T' ⇐ KdStar ↝ T'~ /
  [- TpArrow-span T T' (maybe-to-checking kₑ?)
       (kind-data Γ KdStar :: expected-kind-if Γ kₑ?)
       (check-for-kind-mismatch-if Γ "computed" kₑ? KdStar) -]
  return-when (TpAbs e ignored-var (Tkt T~) T'~) KdStar

-- { t₁ ≃ t₂ }
check-type Γ (ExTpEq pi t₁ t₂ pi') kₑ? =
  untyped-term Γ t₁ >>= t₁~ /
  untyped-term Γ t₂ >>= t₂~ /
  [- punctuation-span "Parens (equation)" pi pi' -]
  [- TpEq-span pi pi' (maybe-to-checking kₑ?)
       (kind-data Γ KdStar :: expected-kind-if Γ kₑ?)
       (check-for-kind-mismatch-if Γ "computed" kₑ? KdStar) -]
  return-when (TpEq t₁~ t₂~) KdStar

-- ●
check-type Γ (ExTpHole pi) kₑ? =
  [- tp-hole-span Γ pi kₑ? (maybe-to-checking kₑ?) [] -]
  return-when (TpHole pi) (KdHole pi)

-- λ x : tk. T
check-type Γ (ExTpLam pi pi' x tk T) kₑ? =
  [- punctuation-span "Lambda (type)" pi (posinfo-plus pi 1) -]
  Γ ⊢ tk ↝ tk~ /
  case-ret
    ((Γ , pi' - x :` tk~) ⊢ T ↝ T~ ⇒ k /
     let kₛ = KdAbs x tk~ (rename-var Γ (pi' % x) x k) in
     [- var-span ff (Γ , pi' - x :` tk~) pi' x checking tk~ nothing -]
     [- TpLambda-span Γ pi pi' x tk~ T synthesizing [ kind-data Γ kₛ ] nothing -]
     return2 (TpLam x tk~ (rename-var Γ (pi' % x) x T~)) kₛ)
    λ kₑ →
      (Γ ⊢ kₑ =β= λ where
        (KdAbs x' tk' k) →
          (Γ , pi' - x :` tk~) ⊢ T ⇐ (rename-var Γ x' (pi' % x) k) ↝ T~ /
          let xₙ = if x =string ignored-var && is-free-in x' k then x' else x in
          return (xₙ , rename-var Γ (pi' % x) xₙ T~ , lambda-bound-conv? Γ x tk' tk~ [])
        kₕ →
          (Γ , pi' - x :` tk~) ⊢ T ↝ T~ ⇒ _ /
          return (x , rename-var Γ (pi' % x) x T~ , [] , unless (is-hole kₕ)
              "The expected kind is not an arrow- or Pi-kind")
      ) >>= λ where
        (xₙ , T~ , tvs , e?) →
          [- var-span ff (Γ , pi' - x :` tk~) pi' x checking tk~ nothing -]
          [- TpLambda-span Γ pi pi' x tk~ T checking (expected-kind Γ kₑ :: tvs) e? -]
          return (TpLam xₙ tk~ T~)

-- (T)
check-type Γ (ExTpParens pi T pi') kₑ? =
  [- punctuation-span "Parens (type)" pi pi' -]
  check-type Γ T kₑ?

-- x
check-type Γ (ExTpVar pi x) kₑ? =
  maybe-else' (ctxt-lookup-type-var Γ x)
    ([- TpVar-span Γ pi x (maybe-to-checking kₑ?) (expected-kind-if Γ kₑ?)
          (just "Undefined type variable") -]
     return-when (TpVar x) (KdHole pi)) λ where
    (qx , as , k) →
      [- TpVar-span Γ pi x (maybe-to-checking kₑ?)
           (expected-kind-if Γ kₑ? ++ [ kind-data Γ k ])
           (check-for-kind-mismatch-if Γ "computed" kₑ? k) -]
      return-when (apps-type (TpVar qx) as) k

-- Π x : tk. k
check-kind Γ (ExKdAbs pi pi' x tk k) =
  Γ ⊢ tk ↝ tk~ /
  Γ , pi' - x :` tk~ ⊢ k ↝ k~ /
  [- KdAbs-span Γ pi pi' x tk~ k checking nothing -]
  [- var-span ff Γ pi' x checking tk~ nothing -]
  [- punctuation-span "Pi (kind)" pi (posinfo-plus pi 1) -]
  return (KdAbs x tk~ (rename-var Γ (pi' % x) x k~))

-- tk ➔ k
check-kind Γ (ExKdArrow tk k) =
  Γ ⊢ tk ↝ tk~ /
  Γ ⊢ k ↝ k~ /
  [- KdArrow-span tk k checking nothing -]
  return (KdAbs ignored-var tk~ k~)

-- ●
check-kind Γ (ExKdHole pi) =
  [- kd-hole-span pi checking -]
  return (KdHole pi)

-- (k)
check-kind Γ (ExKdParens pi k pi') =
  [- punctuation-span "Parens (kind)" pi pi' -]
  check-kind Γ k

-- ★
check-kind Γ (ExKdStar pi) =
  [- Star-span pi checking nothing -]
  return KdStar

-- κ as...
check-kind Γ (ExKdVar pi κ as) =
  case ctxt-lookup-kind-var-def Γ κ of λ where
    nothing →
      [- KdVar-span Γ (pi , κ) (args-end-pos (posinfo-plus-str pi κ) as)
           [] checking [] (just "Undefined kind variable") -]
      return (KdHole pi)
    (just (ps , k)) →
      check-args Γ as ps >>= λ as~ →
      [- KdVar-span Γ (pi , κ) (args-end-pos (posinfo-plus-str pi κ) as)
          ps checking (params-data Γ ps)
          (when (length as < length ps)
            ("Needed " ^ ℕ-to-string (length ps ∸ length as)
              ^ " further argument(s)")) -]
      return (fst (subst-params-args' Γ ps as~ k))

check-tpkd Γ (ExTkt T) = Tkt <$> check-type Γ T (just KdStar)
check-tpkd Γ (ExTkk k) = Tkk <$> check-kind Γ k

check-args Γ (ExTmArg me t :: as) (Param me' x (Tkt T) :: ps) =
  Γ ⊢ t ⇐ T ↝ t~ /
  let e-s = mk-span "Argument" (term-start-pos t) (term-end-pos t)
              [ expected-type Γ T ] (just "Mismatched argument erasure")
      e-m = λ r → if me iff me' then return {F = spanM} r else ([- e-s -] return {F = spanM} r) in
  check-args Γ as (subst-params Γ t~ x ps) >>= λ as~ →
  e-m ((if me then inj₂ (inj₁ t~) else inj₁ t~) :: as~)
check-args Γ (ExTpArg T :: as) (Param _ x (Tkk k) :: ps) =
  Γ ⊢ T ⇐ k ↝ T~ /
  check-args Γ as (subst-params Γ T~ x ps) >>= λ as~ →
  return (inj₂ (inj₂ T~) :: as~)
check-args Γ (ExTmArg me t :: as) (Param _ x (Tkk k) :: ps) =
  [- mk-span "Argument" (term-start-pos t) (term-end-pos t) [ expected-kind Γ k ]
       (just "Expected a type argument") -]
  return []
check-args Γ (ExTpArg T :: as) (Param me x (Tkt T') :: ps) =
  [- mk-span "Argument" (type-start-pos T) (type-end-pos T) [ expected-type Γ T' ]
       (just ("Expected a" ^ (if me then "n erased" else "") ^ " term argument")) -]
  return []
check-args Γ (a :: as) [] =
  let range = case a of λ {(ExTmArg me t) → term-start-pos t , term-end-pos t;
                           (ExTpArg T) → type-start-pos T , type-end-pos T} in
  check-args Γ as [] >>= λ as~ →
  [- mk-span "Argument" (fst range) (snd range) [] (just "Too many arguments given") -]
  return []
check-args Γ [] _ = return []

check-erased-margs : ctxt → posinfo → posinfo → term → maybe type → spanM ⊤
check-erased-margs Γ pi pi' t T? =
  let psₑ = foldr (λ {(Param me x tk) psₑ → if me then x :: psₑ else psₑ}) [] (ctxt.ps Γ)
      fvs = free-vars (erase t)
      e = list-any (stringset-contains fvs) psₑ in
  if e then spanM-add (erased-marg-span Γ pi pi' T?) else spanMok

check-let Γ (ExDefTerm pi x (just Tₑ) t) e? fm to =
  Γ ⊢ Tₑ ⇐ KdStar ↝ Tₑ~ /
  Γ ⊢ t ⇐ Tₑ~ ↝ t~ /
  elim-pair (compileFail-in Γ t~) λ tvs e →
  [- Var-span (Γ , pi - x :` Tkt Tₑ~) pi x checking (type-data Γ Tₑ~ :: tvs) e -]
  return
    (ctxt-term-def pi localScope opacity-open x (just t~) Tₑ~ Γ ,
     pi % x ,
     binder-data Γ pi x (Tkt Tₑ~) e? (just t~) fm to ,
     (λ {ed} T' → [ Γ - t~ / (pi % x) ] T') ,
     (λ t' → LetTm (e? || ~ is-free-in (pi % x) (erase t')) x nothing t~
                   ([ Γ - Var x / (pi % x) ] t')))
check-let Γ (ExDefTerm pi x nothing t) e? fm to =
  Γ ⊢ t ↝ t~ ⇒ Tₛ~ /
  elim-pair (compileFail-in Γ t~) λ tvs e →
  let Γ' = ctxt-term-def pi localScope opacity-open x (just t~) Tₛ~ Γ in
   [- Var-span Γ' pi x synthesizing (type-data Γ Tₛ~ :: tvs) e -]
   return
     (Γ' ,
     pi % x ,
     binder-data Γ pi x (Tkt Tₛ~) e? (just t~) fm to ,
     (λ {ed} T' → [ Γ - t~ / (pi % x) ] T') ,
     (λ t' → LetTm (e? || ~ is-free-in (pi % x) (erase t')) x nothing t~
                   ([ Γ - Var x / (pi % x) ] t')))
check-let Γ (ExDefType pi x k T) e? fm to =
  Γ ⊢ k ↝ k~ /
  Γ ⊢ T ⇐ k~ ↝ T~ /
  [- TpVar-span (Γ , pi - x :` Tkk k~) pi x checking [ kind-data Γ k~ ] nothing -]
  return
    (ctxt-type-def pi localScope opacity-open x (just T~) k~ Γ ,
     pi % x ,
     binder-data Γ pi x (Tkk k~) e? (just T~) fm to ,
     (λ {ed} T' → [ Γ - T~ / (pi % x) ] T') ,
     (λ t' → LetTp x k~ T~ ([ Γ - TpVar x / (pi % x) ] t')))

check-case Γ (ExCase pi x cas t) es Dₓ cs ρₒ as dps Tₘ cast-tm cast-tp =
  [- pattern-span pi x cas -]
  maybe-else'
    (trie-lookup (ctxt.qual Γ) x >>= uncurry λ x' _ →
     trie-lookup cs x' >>= λ T →
     just (x' , T))
    (let e = maybe-else' (trie-lookup es x)
               ("This is not a constructor of " ^
                  unqual-local (unqual-all (ctxt.qual Γ) Dₓ))
               λ _ → "This case is unreachable" in
     [- pattern-ctr-span Γ pi x [] [] (just e) -]
     return2 (Case x [] (Hole pi) []) cs)
    λ where
     (x' , Tₕ , ps , is) →
      decl-args Γ cas ps empty-trie ρₒ [] (const spanMok) >>= λ where
        (Γ' , cas' , e , σ , ρ , tvs , sm) →
          let rs = tmtps-to-args' Γ' σ (drop dps is)
              Tₘ' = TpAppTm (apps-type Tₘ rs)
                            (app-caseArgs (cast-tm Γ') (cast-tp Γ') (recompose-apps as (Var x')) (zip cas cas'))
              Tₘ' = hnf Γ' unfold-no-defs Tₘ' in
          Γ' ⊢ t ⇐ Tₘ' ↝ t~ /
          sm t~ >>
          [- pattern-clause-span pi t (reverse tvs) -]
          [- pattern-ctr-span Γ' pi x cas' [] e -]
          return2 (Case x'
                     (subst-case-args cas' Γ ρₒ)
                     (subst-renamectxt Γ ρ t~)
                     (args-to-tmtps (as ++ (subst-renamectxt Γ ρ -arg_ <$> rs))))
                  (trie-remove cs x')
  where
  subst-case-args : case-args → ctxt → renamectxt → case-args
  subst-case-args [] Γ ρ = []
  subst-case-args (CaseArg e x tk? :: cs) Γ ρ =
    CaseArg e x (subst-renamectxt Γ ρ -tk_ <$> tk?) ::
      subst-case-args cs (ctxt-var-decl x Γ) (renamectxt-insert ρ x x)

  free-in-term : var → term → err-m
  free-in-term x t = when (is-free-in x (erase t))
                       "Erased argument occurs free in the body of the term"
  tmtp-to-arg' : ctxt → trie (Σi exprd ⟦_⟧) → tmtp → arg
  tmtp-to-arg' = λ Γ σ → either-else (Arg ∘ substs Γ σ) (ArgTp ∘ substs Γ σ)
  tmtps-to-args' : ctxt → trie (Σi exprd ⟦_⟧) → 𝕃 tmtp → args
  tmtps-to-args' = λ Γ σ → tmtp-to-arg' Γ σ <$>_
  app-caseArgs : (term → type → term) → (type → kind → type) → term → 𝕃 (ex-case-arg × case-arg) → term
  app-caseArgs tf Tf = foldl λ where
    (ExCaseArg _ pi x , CaseArg me _ tk?) t → elim-pair (me , tk?) λ where
      tt (just (Tkt T)) → AppEr t (tf (Var (pi % x)) T)
      tt (just (Tkk k)) → AppTp t (Tf (TpVar (pi % x)) k)
      ff (just (Tkt T)) → App t (tf (Var (pi % x)) T)
      _ _ → t
  spos = term-start-pos t
  epos = term-end-pos t
  add-case-arg : ∀ {X Y} → ctxt → var → var → case-arg → spanM (X × case-args × Y) → spanM (X × case-args × Y)
  add-case-arg Γ x xₙ ca m = m >>=c λ X → return2 X ∘ map-fst λ cas → ca :: subst-case-args cas Γ (renamectxt-single x xₙ)
  decl-args : ctxt → ex-case-args → params → trie (Σi exprd ⟦_⟧) →
                renamectxt → 𝕃 tagged-val → (term → spanM ⊤) →
              spanM (ctxt × case-args × err-m × trie (Σi exprd ⟦_⟧) ×
                     renamectxt × 𝕃 tagged-val × (term → spanM ⊤))
  decl-args Γ (ExCaseArg ExCaseArgTp pi x :: as) (Param me x' (Tkt T) :: ps) σ ρ xs sm =
    let T' = substs Γ σ T
        Γ' = ctxt-var-decl-loc pi x Γ
        xₙ = if x =string ignored-var then x' else x in
    add-case-arg Γ' (pi % x) xₙ (CaseArg tt xₙ (just (Tkt T'))) $
    decl-args Γ' as ps
      (trie-insert σ x' (, TpVar (pi % x)))
      (renamectxt-insert ρ (pi % x) xₙ)
      (binder-data Γ' pi x (Tkt T') Erased nothing spos epos :: xs)
      λ t → [- TpVar-span Γ' pi x checking [ expected-type Γ T' ]
                 (just ("This type argument should be a" ^
                     (if me then "n erased term" else " term"))) -] sm t
  decl-args Γ (ExCaseArg ExCaseArgTp pi x :: as) (Param _ x' (Tkk k) :: ps) σ ρ xs sm =
    let k' = substs Γ σ k
        Γ' = ctxt-type-decl pi x k' Γ
        xₙ = if x =string ignored-var then x' else x in
    add-case-arg Γ' (pi % x) xₙ (CaseArg tt xₙ (just (Tkk k'))) $
    decl-args Γ' as ps
      (trie-insert σ x' (, TpVar (pi % x)))
      (renamectxt-insert ρ (pi % x) xₙ)
      (binder-data Γ' pi x (Tkk k') Erased nothing spos epos :: xs)
      λ t → [- TpVar-span Γ' pi x checking [ kind-data Γ k' ] (free-in-term x t) -] sm t
  decl-args Γ (ExCaseArg me pi x :: as) (Param me' x' (Tkt T) :: ps) σ ρ xs sm =
    let T' = substs Γ σ T
        e₁ = when (ex-case-arg-erased me xor me') "Mismatched erasure of term argument"
        e₂ = λ t → ifMaybe (ex-case-arg-erased me) $ free-in-term x t
        Γ' = Γ , pi - x :` (Tkt T')
        xₙ = if x =string ignored-var then x' else x in
    (add-case-arg Γ' (pi % x) xₙ (CaseArg me' xₙ (just (Tkt T'))) $
    decl-args Γ' as ps
      (trie-insert σ x' (, Var (pi % x)))
      (renamectxt-insert ρ (pi % x) xₙ)
      (binder-data Γ' pi x (Tkt T') (ex-case-arg-erased me) nothing spos epos :: xs)
      λ t → [- Var-span Γ' pi x checking [ type-data Γ T' ] (e₁ ||-maybe e₂ t) -] sm t)
  decl-args Γ (ExCaseArg me pi x :: as) (Param me' x' (Tkk k) :: ps) σ ρ xs sm =
    let k' = substs Γ σ k
        Γ' = ctxt-var-decl-loc pi x Γ
        xₙ = if x =string ignored-var then x' else x in
    add-case-arg Γ' (pi % x) xₙ (CaseArg tt xₙ (just (Tkk k'))) $
    decl-args Γ' as ps
      (trie-insert σ x' (, Var (pi % x)))
      (renamectxt-insert ρ (pi % x) xₙ)
      (binder-data Γ' pi x (Tkk k') (ex-case-arg-erased me) nothing spos epos :: xs)
      λ t → [- Var-span Γ' pi x checking [ expected-kind Γ k' ]
                 (just "This term argument should be a type") -] sm t
  decl-args Γ [] [] σ ρ xs sm =
    return (Γ , [] , nothing , σ , ρ , xs , sm)
  decl-args Γ as [] σ ρ xs sm =
    return (Γ , [] , just (ℕ-to-string (length as) ^ " too many arguments supplied") ,
              σ , ρ , xs , sm)
  decl-args Γ [] ps σ ρ xs sm =
    return (Γ , params-to-case-args (substs-params Γ σ ps) ,
            just (ℕ-to-string (length ps) ^ " more arguments expected") , σ , ρ , xs , sm)

check-cases Γ ms Dₓ cs ρ as dps Tₘ cast-tm cast-tp =
  foldr {B = stringset → trie (type × params × 𝕃 tmtp) →
              spanM (cases × trie (type × params × 𝕃 tmtp))}
    (λ m x es cs' →
      check-case Γ m es Dₓ cs' ρ as dps Tₘ cast-tm cast-tp >>=c λ m~ cs →
      x (stringset-insert es (ex-case-ctr m)) cs >>=c λ ms~ →
      return2 (m~ :: ms~))
    (λ es → return2 [])
    ms
    empty-stringset
    (trie-map (decompose-ctr-type Γ) cs)
  >>=c λ ms~ missing-cases →
  let xs = map (map-snd snd) $ trie-mappings missing-cases
      csf = uncurry₂ λ Tₕ ps as →
              rope-to-string $ strRun Γ $
                strVar (unqual-all (ctxt.qual Γ) Tₕ) >>str args-to-string (params-to-args ps)
      e = "Missing patterns: " ^ 𝕃-to-string csf ", " xs in
  return2 ms~ (unless (iszero (length xs)) e)

check-refinement Γ Tₘ kₘ s =
  check-type (qualified-ctxt Γ) (resugar Tₘ) (just kₘ) empty-spans >>= uncurry λ Tₘ' s' →
    return $ (λ x → x , s) $
      Tₘ' ,
      [ to-string-tag "computed motive" Γ Tₘ ] ,
      (when (spans-have-error s') "We could not compute a well-kinded motive")

get-datatype-info-from-head-type Γ X as = return $ maybe-else' (data-lookup Γ X as)
    (inj₁ $ "The head type of the subterm is not a datatype" , [ head-type Γ (TpVar X) ])
    (λ μ → inj₂ μ)

check-sigma-evidence Γ tₑ? X as = maybe-else' tₑ?
  (get-datatype-info-from-head-type Γ X as >>=s λ d → return $ inj₂ (sigma-build-evidence X d , id , d))
  (λ tₑ →
    Γ ⊢ tₑ ↝ tₑ~ ⇒ T /
    let ev-err = inj₁ $
                   ("The synthesized type of the evidence does not prove " ^
                      unqual-local (unqual-all (ctxt.qual Γ) X) ^ " is a datatype") ,
                    [ to-string-tag "evidence type" Γ T ] in
    case decompose-tpapps (hnf Γ unfold-head-elab T) of λ where
      (TpVar X' , as') → case reverse as' of λ where
        (Ttp T :: as') → return $ if ~ conv-type Γ T (TpVar X)
          then ev-err
          else maybe-else
            ev-err
            (λ {d@(mk-data-info X Xₒ asₚ asᵢ mps kᵢ k cs csₚₛ eds gds) →
              inj₂ (tₑ~ , (App $ recompose-apps (asₚ ++ tmtps-to-args Erased asᵢ) $
                                   Var $ data-to/ X) , d)})
            -- AS: it looks like we are reversing as' twice, so not reversing at all?
            (data-lookup-mu Γ X X' $ reverse as' ++ as)
            -- TODO: Make sure "X" isn't a _defined_ type, but a _declared_ one!
            --       This way we avoid the possibility that "as" has arguments
            --       to parameters in it, but only to indices.
            -- Also TODO: Make sure that parameters are equal in above conversion check!
        _ → return ev-err
      _ → return ev-err
  )

ctxt-mu-decls : ctxt → term → indices → type → datatype-info → posinfo → posinfo → posinfo → var → (cases → spanM ⊤) × ctxt × 𝕃 tagged-val × renamectxt × (ctxt → term → type → term) × (ctxt → type → kind → type)
ctxt-mu-decls Γ t is Tₘ (mk-data-info X Xₒ asₚ asᵢ ps kᵢ k cs csₚₛ eds gds) pi₁ pi₂ pi₃ x =
  let X' = mu-Type/ x
      xₘᵤ = mu-isType/ x
      qXₘᵤ = data-Is/ X
      qXₜₒ = data-to/ X
      qX' = pi₁ % X'
      qxₘᵤ = pi₁ % xₘᵤ
      qx = pi₁ % x
      Tₘᵤ = TpAppTp (flip apps-type asₚ $ TpVar qXₘᵤ) $ TpVar qX'
      Γ' = ctxt-term-def pi₁ localScope opacity-open xₘᵤ nothing Tₘᵤ $
           ctxt-datatype-decl X qx asₚ $
           ctxt-type-decl pi₁ X' k Γ
      freshₓ = fresh-var (add-indices-to-ctxt is Γ') (maybe-else "x" id (is-var (Ttm t)))
      Tₓ = hnf Γ' unfold-no-defs (indices-to-alls is $ TpAbs ff freshₓ (Tkt $ indices-to-tpapps is $ TpVar qX') $ TpAppTm (indices-to-tpapps is Tₘ) $ Phi (Beta (Var freshₓ) (Var freshₓ)) (App (indices-to-apps is $ AppEr (AppTp (flip apps-term asₚ $ Var qXₜₒ) $ TpVar qX') $ Var qxₘᵤ) $ Var freshₓ) (Var freshₓ))
      Γ'' = ctxt-term-decl pi₁ x Tₓ Γ'
      e₂? = unless (X =string Xₒ) "Abstract datatypes can only be pattern matched by σ"
      e₃ = λ x → just $ x ^ " occurs free in the erasure of the body (not allowed)"
      cs-fvs = stringset-contains ∘' free-vars-cases ∘' erase-cases
      e₃ₓ? = λ cs x → ifMaybe (cs-fvs cs x) $ e₃ x
      e₃? = λ cs → e₃ₓ? cs (mu-isType/ x) ||-maybe e₃ₓ? cs (mu-Type/ x) in
    (λ cs → [- var-span NotErased Γ'' pi₁ x checking (Tkt Tₓ) (e₂? ||-maybe e₃? cs) -] spanMok) ,
     Γ'' ,
    (binder-data Γ'' pi₁ X' (Tkk k) Erased nothing pi₂ pi₃ ::
     binder-data Γ'' pi₁ xₘᵤ (Tkt Tₘᵤ) Erased nothing pi₂ pi₃ ::
     binder-data Γ'' pi₁ x (Tkt Tₓ) NotErased nothing pi₂ pi₃ ::
     to-string-tag X' Γ'' k ::
     to-string-tag xₘᵤ Γ'' Tₘᵤ ::
     to-string-tag x Γ'' Tₓ :: []) ,
    renamectxt-insert* empty-renamectxt
      ((qX' , X') :: (qxₘᵤ , xₘᵤ) :: (qx , x) :: []) ,
    let cg = qX' , recompose-tpapps (args-to-tmtps asₚ) (TpVar qx) , AppEr (AppTp (recompose-apps asₚ (Var qXₜₒ)) (TpVar qX')) (Var qxₘᵤ) in
    flip (mk-ctr-fmap-η? ff ∘ ctxt-datatype-undef qX') cg ,
    flip (mk-ctr-fmapₖ-η? ff ∘ ctxt-datatype-undef qX') cg

check-mu Γ pi pi' x t Tₘ? pi'' cs pi''' Tₑ? =
  check-term Γ t nothing >>=c λ t~ T →
  let no-motive-err = just "A motive is required when synthesizing"
      no-motive = return (nothing , [] , no-motive-err) in
  case decompose-tpapps (hnf Γ unfold-head-elab T) of λ where
    (TpVar X , as) →
      get-datatype-info-from-head-type Γ X as on-fail
       (uncurry λ e tvs → spanM-add (Mu-span Γ pi pi''' nothing (maybe-to-checking Tₑ?)
         (expected-type-if Γ Tₑ? ++ tvs) $ just e) >>
        return-when {m = Tₑ?} (Hole pi) (TpHole pi))
       >>=s λ where
        (d @ (mk-data-info Xₒ _ asₚ asᵢ ps kᵢ k cs' csₚₛ eds gds)) →
          let Rₓ = mu-Type/ x; qRₓ = pi' % Rₓ
              Γₘ = data-highlight (ctxt-type-decl pi' Rₓ k Γ) qRₓ
              ρₘ = subst Γₘ (recompose-tpapps (args-to-tmtps asₚ) (TpVar Xₒ)) qRₓ
              ρₘ' = subst Γₘ (TpVar Rₓ) qRₓ
              eₘ = λ Tₘ → when (negₒ (extract-pos (positivity.type+ qRₓ Γₘ (hnf-ctr Γₘ qRₓ Tₘ))))
                            (Rₓ ^ " occurs negatively in the motive")
          in
              maybe-map (λ Tₘ → check-type Γₘ Tₘ (just kᵢ)) Tₘ? >>=? λ Tₘ?' →
              let is = kind-to-indices Γ kᵢ
                  eₘ = Tₘ?' >>= eₘ
                  ret-tp = λ ps as t → maybe-else' Tₘ?' Tₑ? (λ Tₘ → just $ hnf Γ unfold-head-elab (TpAppTm (apps-type (ρₘ Tₘ) $
                              tmtps-to-args NotErased (drop (length ps) as)) t)) in
              (maybe-else' Tₘ?'
                 (return Tₑ? on-fail no-motive >>=m λ Tₑ →
                  let Tₘ = refine-motive Γ is (asᵢ ++ [ Ttm t~ ]) Tₑ in
                  check-refinement Γ Tₘ kᵢ >>=c λ Tₘ → return2 (just Tₘ))
                 λ Tₘ → return (just Tₘ , [] , nothing))
              >>=c λ Tₘ → uncurry λ tvs₁ e₁ →
              let Tₘ = maybe-else' Tₘ (TpHole pi) id
                  is = drop-last 1 is
                  reduce-cs = map λ {(Ctr x T) → Ctr x $ hnf Γ unfold-no-defs T}
                  fcs = λ y → inst-ctrs Γ ps asₚ (map-snd (rename-var {TYPE} Γ Xₒ y) <$> cs')
                  cs' = reduce-cs $ fcs (mu-Type/ (pi' % x)) in
              case
                (ctxt-mu-decls Γ t~ is Tₘ d pi' pi'' pi''' x) of λ where
                (sm , Γ' , bds , ρ , cast-tm , cast-tp) →
                  let cs'' = foldl (λ {(Ctr x T) σ → trie-insert σ x T}) empty-trie cs'
                      drop-ps = 0
                      scrutinee = t~
                      Tᵣ = ret-tp ps (args-to-tmtps asₚ ++ asᵢ) scrutinee in
                  check-cases Γ' cs Xₒ cs'' ρ asₚ drop-ps Tₘ cast-tm cast-tp >>=c λ cs~ e₂ →
                  let e₃ = maybe-else' Tᵣ
                             (just "A motive is required when synthesizing")
                             (check-for-type-mismatch-if Γ "synthesized" Tₑ?) in
                  [- Mu-span Γ pi pi''' Tₘ?' (maybe-to-checking Tₑ?)
                         (expected-type-if Γ Tₑ? ++
                           maybe-else' Tᵣ [] (λ Tᵣ → [ type-data Γ Tᵣ ]) ++
                           tvs₁ ++
                           bds)
                         (e₁ ||-maybe (e₂ ||-maybe (e₃ ||-maybe eₘ))) -]
                  sm cs~ >>
                  return-when {m = Tₑ?}
                    (subst-renamectxt Γ ρ (Mu x t~ (just (ρₘ' Tₘ)) d cs~))
                    (maybe-else' Tᵣ (TpHole pi) id)
    (Tₕ , as) →
      [- Mu-span Γ pi pi''' nothing (maybe-to-checking Tₑ?)
        [ head-type Γ Tₕ ] (just "The head type of the subterm is not a datatype") -]
      return-when {m = Tₑ?} (Hole pi) (TpHole pi)

check-sigma Γ pi t? t Tₘ? pi'' cs pi''' Tₑ? =
  check-term Γ t nothing >>=c λ t~ T →
  let no-motive-err = just "A motive is required when synthesizing"
      no-motive = return (nothing , [] , no-motive-err) in
  case decompose-tpapps (hnf Γ unfold-head-elab T) of λ where
    (TpVar X , as) →
      check-sigma-evidence Γ t? X as on-fail
       (uncurry λ e tvs → spanM-add (Sigma-span Γ pi pi''' nothing (maybe-to-checking Tₑ?)
         (expected-type-if Γ Tₑ? ++ tvs) $ just e) >>
        return-when {m = Tₑ?} (Hole pi) (TpHole pi))
       >>=s λ where
        (tₑ~ , cast , d @ (mk-data-info Xₒ _ asₚ asᵢ ps kᵢ k cs' csₚₛ eds gds)) →
              maybe-map (λ Tₘ → check-type Γ Tₘ (just kᵢ)) Tₘ? >>=? λ Tₘ?' →
              let is = kind-to-indices Γ kᵢ
                  ret-tp = λ ps as t → maybe-else' Tₘ?' Tₑ? (λ Tₘ → just $ hnf Γ unfold-head-elab (TpAppTm (apps-type Tₘ $
                              tmtps-to-args NotErased (drop (length ps) as)) t)) in
              (maybe-else' Tₘ?'
                 (return Tₑ? on-fail no-motive >>=m λ Tₑ →
                  let Tₘ = refine-motive Γ is (asᵢ ++ [ Ttm t~ ]) Tₑ in
                  check-refinement Γ Tₘ kᵢ >>=c λ Tₘ → return2 (just Tₘ))
                 λ Tₘ → return (just Tₘ , [] , nothing))
              >>=c λ Tₘ → uncurry λ tvs₁ e₁ →
              let Tₘ = maybe-else' Tₘ (TpHole pi) id
                  reduce-cs = map λ {(Ctr x T) → Ctr x $ hnf Γ unfold-no-defs T}
                  fcs = λ y → inst-ctrs Γ ps asₚ (map-snd (rename-var {TYPE} Γ Xₒ y) <$> cs')
                  cs' = reduce-cs $ if Xₒ =string X then csₚₛ else fcs X in
              let sm = const spanMok
                  ρ = empty-renamectxt
                  cast-tm = (λ Γ t T → t)
                  cast-tp = (λ Γ T k → T)
                  cs'' = foldl (λ {(Ctr x T) σ → trie-insert σ x T}) empty-trie cs'
                  drop-ps = maybe-else 0 length (when (Xₒ =string X) ps)
                  scrutinee = cast t~
                  Tᵣ = ret-tp ps (args-to-tmtps asₚ ++ asᵢ) scrutinee in
                 check-cases Γ cs Xₒ cs'' ρ asₚ drop-ps Tₘ cast-tm cast-tp >>=c λ cs~ e₂ →
                 let e₃ = maybe-else' Tᵣ
                             (just "A motive is required when synthesizing")
                             (check-for-type-mismatch-if Γ "synthesized" Tₑ?) in
                  [- Sigma-span Γ pi pi''' Tₘ?' (maybe-to-checking Tₑ?)
                         (expected-type-if Γ Tₑ? ++
                           maybe-else' Tᵣ [] (λ Tᵣ → [ type-data Γ Tᵣ ]) ++
                           tvs₁)
                         (e₁ ||-maybe (e₂ ||-maybe e₃)) -]
                  sm cs~ >>
                  return-when {m = Tₑ?}
                    (subst-renamectxt Γ ρ (Sigma (just tₑ~) t~ (just Tₘ) d cs~))
                    (maybe-else' Tᵣ (TpHole pi) id)
    (Tₕ , as) →
      [- Sigma-span Γ pi pi''' nothing (maybe-to-checking Tₑ?)
        [ head-type Γ Tₕ ] (just "The head type of the subterm is not a datatype") -]
      return-when {m = Tₑ?} (Hole pi) (TpHole pi)


text:
{-# OPTIONS --type-in-type #-}
module poly.core where
open import functors
open import prelude

_^ : Set → Set -- Presheaf
I ^ = I → Set

∫ : Set -- Arena
∫ = ∃ _^

_⦅_⦆ : ∫ → Set → Set -- Interpret as a polynomial functor
(A⁺ , A⁻) ⦅ y ⦆ = Σ[ a⁺ ∈ A⁺ ] (A⁻ a⁺ → y)

module _ (A@(A⁺ , A⁻) B@(B⁺ , B⁻) : ∫) where
  ∫[_,_] : Set
  ∫[_,_] = (a⁺ : A⁺) → Σ[ b⁺ ∈ B⁺ ] (B⁻ b⁺ → A⁻ a⁺)
module _ {A@(A⁺ , A⁻) B@(B⁺ , B⁻) : ∫} where
  lens : (get : A⁺ → B⁺)
         (set : (a⁺ : A⁺) → B⁻ (get a⁺) → A⁻ a⁺)
       → ∫[ A , B ]
  lens g s = λ a⁺ → g a⁺ , s a⁺
  get : (l : ∫[ A , B ]) → A⁺ → B⁺
  get l = π₁ ∘ l
  set : (A↝B : ∫[ A , B ]) → (a⁺ : A⁺) → B⁻ (get A↝B a⁺) → A⁻ a⁺
  set l = π₂ ∘ l

instance
    lens-cat : Category ∫[_,_]
    lens-cat = 𝒾: (λ a⁺ → a⁺ , id)
               ▸: (λ l1 l2 a⁺ → let b⁺ , setb = l1 a⁺
                                    c⁺ , setc = l2 b⁺
                                in  c⁺ , setb ∘ setc)
               𝒾▸: (λ _ → refl)
               ▸𝒾: (λ _ → refl)

ext: agda

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
------------------------------------------------------------------------------
-- Bisimilarity relation on unbounded lists
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Relation.Binary.Bisimilarity.Type where

open import FOTC.Base
open import FOTC.Base.List

infix 4 _≈_ _≉_

------------------------------------------------------------------------------
-- The bisimilarity relation _≈_ on unbounded lists is the greatest
-- fixed-point (by ≈-out and ≈-coind) of the bisimulation functional
-- (FOTC.Relation.Binary.Bisimulation).

-- The bisimilarity relation on unbounded lists.
postulate _≈_ : D → D → Set

-- The bisimilarity relation _≈_ on unbounded lists is a post-fixed
-- point of the bisimulation functional (FOTC.Relation.Binary.Bisimulation).
postulate
  ≈-out : ∀ {xs ys} → xs ≈ ys →
          ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ xs' ≈ ys'
{-# ATP axiom ≈-out #-}

-- The bisimilarity relation _≈_ on unbounded lists is the greatest
-- post-fixed point of the bisimulation functional (see
-- FOTC.Relation.Binary.Bisimulation).
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  ≈-coind :
    (B : D → D → Set) →
    -- B is a post-fixed point of the bisimulation functional.
    (∀ {xs ys} → B xs ys →
      ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ B xs' ys') →
    -- _≈_ is greater than B.
    ∀ {xs ys} → B xs ys → xs ≈ ys

------------------------------------------------------------------------------
-- Auxiliary definition.
_≉_ : D → D → Set
x ≉ y = ¬ x ≈ y
{-# ATP definition _≉_ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Modified: Andreas, 2011-04-11 freezing metas

module Issue151 where

record A : Set₁ where
  field
    El : Set

data B (a : A) : Set₁ where
  b : ∀ a′ → B a′ → B a

data C a : B a → B a → Set₁ where
  c  : ∀ a′ (p : B a′) → C a (b record{ El = A.El a′ } p) (b a′ p)
  c′ : ∀ a′ (p : B a′) → C a (b a′ p) (b a′ p)

-- In order to type check the second clause the unifier
-- needs to eta contract the record in the target of the c
-- constructor.
foo : ∀ a (p : B a) (p′ : B a) → C a (b a p) p′ → Set₁
foo a p (b .a .p) (c′ .a .p) = Set
foo a p (b .a .p) (c .a .p)  = Set

postulate
  D : A → Set
  d : (a : A) → D a

-- The following definition generates a constraint
--   α record{ El = A.El a } == D a
-- on the metavariable above. To solve this the constraint
-- solver has to eta contract the record to see that the
-- left hand side is a proper Miller pattern.
bar : (test : (a : A) -> _) -> (a : A) → D a
bar test a = test record{ El = A.El a }

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
id : forall {k}{X : Set k} -> X -> X
id x = x

_o_ : forall {i j k}
  {A : Set i}{B : A -> Set j}{C : (a : A) -> B a -> Set k} ->
  (f : {a : A}(b : B a) -> C a b) ->
  (g : (a : A) -> B a) ->
  (a : A) -> C a (g a)
f o g = \ a -> f (g a)

data List (X : Set) : Set where
  [] : List X
  _,_ : X → List X → List X

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

data Vec (X : Set) : Nat -> Set where
  [] : Vec X 0
  _,_ : { n : Nat } → X → Vec X n → Vec X (suc n)

vec : forall { n X } → X → Vec X n
vec {zero} a = []
vec {suc n} a = a , vec a

vapp : forall { n S T } → Vec (S → T) n → Vec S n → Vec T n
vapp [] [] = []
vapp (x , st) (x₁ , s) = x x₁ , vapp st s

record Applicative (F : Set → Set) : Set₁ where
  infixl 2 _⊛_
  field
    pure : forall { X } → X → F X
    _⊛_ : forall { S T } → F (S → T) → F S → F T

open Applicative {{...}} public

instance
  applicativeVec : forall { n } → Applicative (λ X → Vec X n)
  applicativeVec = record { pure = vec; _⊛_ = vapp }

instance
  applicativeComp : forall {F G} {{_ : Applicative F}} {{_ : Applicative G}} → Applicative (F o G)
  applicativeComp {{af}} {{ag}} =
    record
    { pure = λ z → Applicative.pure af (Applicative.pure ag z)
    ; _⊛_ = λ z → {!!}
    }

record Traversable (T : Set → Set) : Set1 where
  field
    traverse : forall { F A B } {{ AF : Applicative F }} → (A → F B) → T A → F (T B)

open Traversable {{...}} public

instance
  traversableVec : forall {n} → Traversable (\X → Vec X n)
  traversableVec = record { traverse = vtr } where
    vtr : forall { n F A B } {{ AF : Applicative F }} → (A → F B) → Vec A n → F (Vec B n)
    vtr {{AF}} f [] = Applicative.pure AF []
    vtr {{AF}} f (x , v) =
      Applicative._⊛_ AF (Applicative._⊛_ AF (Applicative.pure AF _,_) (f x)) (vtr f v)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of functions, such as associativity and
-- commutativity (specialised to propositional equality)
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Algebra.FunctionProperties.Consequences.Propositional
       {a} {A : Set a} where

open import Data.Sum using (inj₁; inj₂)
open import Relation.Binary using (Rel; Setoid; Symmetric; Total)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (Pred)

open import Algebra.FunctionProperties {A = A} _≡_
import Algebra.FunctionProperties.Consequences (setoid A) as FP⇒

------------------------------------------------------------------------
-- Re-export all proofs that don't require congruence or substitutivity

open FP⇒ public
  hiding
  ( assoc+distribʳ+idʳ+invʳ⇒zeˡ
  ; assoc+distribˡ+idʳ+invʳ⇒zeʳ
  ; assoc+id+invʳ⇒invˡ-unique
  ; assoc+id+invˡ⇒invʳ-unique
  ; comm+distrˡ⇒distrʳ
  ; comm+distrʳ⇒distrˡ
  ; comm⇒sym[distribˡ]
  ; subst+comm⇒sym
  ; wlog
  ; sel⇒idem
  )

------------------------------------------------------------------------
-- Group-like structures

module _ {_•_ _⁻¹ ε} where

  assoc+id+invʳ⇒invˡ-unique : Associative _•_ → Identity ε _•_ →
                              RightInverse ε _⁻¹ _•_ →
                              ∀ x y → (x • y) ≡ ε → x ≡ (y ⁻¹)
  assoc+id+invʳ⇒invˡ-unique = FP⇒.assoc+id+invʳ⇒invˡ-unique (cong₂ _)

  assoc+id+invˡ⇒invʳ-unique : Associative _•_ → Identity ε _•_ →
                              LeftInverse ε _⁻¹ _•_ →
                              ∀ x y → (x • y) ≡ ε → y ≡ (x ⁻¹)
  assoc+id+invˡ⇒invʳ-unique = FP⇒.assoc+id+invˡ⇒invʳ-unique (cong₂ _)

------------------------------------------------------------------------
-- Ring-like structures

module _ {_+_ _*_ -_ 0#} where

  assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
                                RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                LeftZero 0# _*_
  assoc+distribʳ+idʳ+invʳ⇒zeˡ =
    FP⇒.assoc+distribʳ+idʳ+invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)

  assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
                                RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                RightZero 0# _*_
  assoc+distribˡ+idʳ+invʳ⇒zeʳ =
    FP⇒.assoc+distribˡ+idʳ+invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)

------------------------------------------------------------------------
-- Bisemigroup-like structures

module _ {_•_ _◦_ : Op₂ A} (•-comm : Commutative _•_) where

  comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
  comm+distrˡ⇒distrʳ = FP⇒.comm+distrˡ⇒distrʳ (cong₂ _) •-comm

  comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
  comm+distrʳ⇒distrˡ = FP⇒.comm+distrʳ⇒distrˡ (cong₂ _) •-comm

  comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≡ ((x ◦ y) • (x ◦ z)))
  comm⇒sym[distribˡ] = FP⇒.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm

------------------------------------------------------------------------
-- Selectivity

module _ {_•_ : Op₂ A} where

  sel⇒idem : Selective _•_ → Idempotent _•_
  sel⇒idem = FP⇒.sel⇒idem _≡_

------------------------------------------------------------------------
-- Without Loss of Generality

module _ {p} {P : Pred A p} where

  subst+comm⇒sym : ∀ {f} (f-comm : Commutative f) →
                   Symmetric (λ a b → P (f a b))
  subst+comm⇒sym = FP⇒.subst+comm⇒sym {P = P} subst

  wlog : ∀ {f} (f-comm : Commutative f) →
         ∀ {r} {_R_ : Rel _ r} → Total _R_ →
         (∀ a b → a R b → P (f a b)) →
         ∀ a b → P (f a b)
  wlog = FP⇒.wlog {P = P} subst


text:
------------------------------------------------------------------------
-- Application of substitutions to normal and neutral terms
------------------------------------------------------------------------

open import Level using (zero)
open import Data.Universe

module README.DependentlyTyped.NormalForm.Substitution
  (Uni₀ : Universe zero zero) where

open import Data.Product as Prod renaming (curry to c; uncurry to uc)
open import deBruijn.Substitution.Data
open import Function.Base as F renaming (const to k)
import README.DependentlyTyped.NormalForm as NF; open NF Uni₀
import README.DependentlyTyped.Term.Substitution as S
open S Uni₀ using (module Apply)
import README.DependentlyTyped.Term as Term; open Term Uni₀
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

-- Code for applying substitutions containing terms which can be
-- transformed into /neutral/ terms.

module Apply-n {T : Term-like Level.zero} (T↦Ne : T ↦ Tm-n ne) where

  open _↦_ T↦Ne hiding (var)

  T↦Tm : T ↦ Tm
  T↦Tm = record
    { trans  = forget-n [∘] trans
    ; simple = simple
    }

  open Apply T↦Tm using (_/⊢_; _/⊢t_; app)

  -- Applies a substitution to an atomic type.

  infixl 8 _/⊢a_

  _/⊢a_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
          Γ ⊢ σ atomic-type → (ρ : Sub T ρ̂) → Δ ⊢ σ / ρ atomic-type
  ⋆  /⊢a ρ = ⋆
  el /⊢a ρ = el

  mutual

    -- Applies a renaming to a normal or neutral term.

    infixl 8 _/⊢n_ _/⊢n-lemma_

    _/⊢n_ : ∀ {Γ Δ σ k} {ρ̂ : Γ ⇨̂ Δ} →
            Γ ⊢ σ ⟨ k ⟩ → (ρ : Sub T ρ̂) → Δ ⊢ σ / ρ ⟨ k ⟩
    ne σ′ t /⊢n ρ = ne (σ′ /⊢a ρ) (t /⊢n ρ)
    var x   /⊢n ρ = trans ⊙ (x /∋ ρ)
    ƛ t     /⊢n ρ = ƛ (t /⊢n ρ ↑)
    t₁ · t₂ /⊢n ρ = [ t₁ · t₂ ]/⊢n ρ

    -- The body of the last case above. (At the time of writing the
    -- termination checker complains if [ t₁ · t₂ ]/⊢n ρ is replaced
    -- by t₁ · t₂ /⊢n ρ in the type signature of ·-/⊢n below.)

    [_·_]/⊢n :
      ∀ {Γ Δ sp₁ sp₂ σ} {ρ̂ : Γ ⇨̂ Δ}
      (t₁ : Γ ⊢ π sp₁ sp₂ , σ ⟨ ne ⟩) (t₂ : Γ ⊢ fst σ ⟨ no ⟩)
      (ρ : Sub T ρ̂) →
      Δ ⊢ snd σ /̂ ŝub ⟦ t₂ ⟧n /̂ ρ̂ ⟨ ne ⟩
    [_·_]/⊢n {σ = σ} t₁ t₂ ρ =
      P.subst (λ v → _ ⊢ snd σ /̂ ⟦ ρ ⟧⇨ ↑̂ /̂ ŝub v ⟨ ne ⟩)
              (≅-Value-⇒-≡ $ P.sym (t₂ /⊢n-lemma ρ))
              ((t₁ /⊢n ρ) · (t₂ /⊢n ρ))

    abstract

      -- An unfolding lemma.

      ·-/⊢n :
        ∀ {Γ Δ sp₁ sp₂ σ} {ρ̂ : Γ ⇨̂ Δ}
        (t₁ : Γ ⊢ π sp₁ sp₂ , σ ⟨ ne ⟩) (t₂ : Γ ⊢ fst σ ⟨ no ⟩)
        (ρ : Sub T ρ̂) →
        [ t₁ · t₂ ]/⊢n ρ ≅-⊢n (t₁ /⊢n ρ) · (t₂ /⊢n ρ)
      ·-/⊢n {σ = σ} t₁ t₂ ρ =
        drop-subst-⊢n (λ v → snd σ /̂ ⟦ ρ ⟧⇨ ↑̂ /̂ ŝub v)
                      (≅-Value-⇒-≡ $ P.sym $ t₂ /⊢n-lemma ρ)

      -- The application operation is well-behaved.

      _/⊢n-lemma_ : ∀ {Γ Δ σ k} {ρ̂ : Γ ⇨̂ Δ}
                    (t : Γ ⊢ σ ⟨ k ⟩) (ρ : Sub T ρ̂) →
                    ⟦ t ⟧n /Val ρ ≅-Value ⟦ t /⊢n ρ ⟧n
      ne σ′ t /⊢n-lemma ρ = begin
        [ ⟦ t ⟧n /Val ρ ]  ≡⟨ t /⊢n-lemma ρ ⟩
        [ ⟦ t /⊢n ρ ⟧n  ]  ∎
      var x /⊢n-lemma ρ = /̂∋-⟦⟧⇨ x ρ
      ƛ t   /⊢n-lemma ρ = begin
        [ c ⟦ t ⟧n /Val ρ     ]  ≡⟨ P.refl ⟩
        [ c (⟦ t ⟧n /Val ρ ↑) ]  ≡⟨ curry-cong (t /⊢n-lemma (ρ ↑)) ⟩
        [ c ⟦ t /⊢n ρ ↑ ⟧n    ]  ∎
      t₁ · t₂ /⊢n-lemma ρ = begin
        [ ⟦ t₁ · t₂ ⟧n /Val ρ                 ]  ≡⟨ P.refl ⟩
        [ (⟦ t₁ ⟧n /Val ρ) ˢ (⟦ t₂ ⟧n /Val ρ) ]  ≡⟨ ˢ-cong (t₁ /⊢n-lemma ρ) (t₂ /⊢n-lemma ρ) ⟩
        [ ⟦ t₁ /⊢n ρ ⟧n ˢ ⟦ t₂ /⊢n ρ ⟧n       ]  ≡⟨ P.refl ⟩
        [ ⟦ (t₁ /⊢n ρ) · (t₂ /⊢n ρ) ⟧n        ]  ≡⟨ ⟦⟧n-cong (P.sym $ ·-/⊢n t₁ t₂ ρ) ⟩
        [ ⟦ t₁ · t₂ /⊢n ρ ⟧n                  ]  ∎

  app-n : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → [ Tm-n ne ⟶ Tm-n ne ] ρ̂
  app-n ρ = record
    { function    = λ _ t → t /⊢n ρ
    ; corresponds = λ _ t → t /⊢n-lemma ρ
    }

substitution₁-n : Substitution₁ (Tm-n ne)
substitution₁-n = record
  { var      = record { function    = λ _ → var
                      ; corresponds = λ _ _ → P.refl
                      }
  ; app′     = Apply-n.app-n
  ; app′-var = λ _ _ _ → P.refl
  }

open Substitution₁ substitution₁-n public hiding (var)

-- Let us make _/⊢n_ and friends immediately available for use with
-- /renamings/.

open Apply-n (Translation-from.translation Var-↦) public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
-- Andreas, 2015-02-07 Failed with-abstraction in rewrite-generated with.
-- {-# OPTIONS -v tc.rewrite.top:25 -v tc.with.top:25 -v tc.with.abstract:50 #-}

{-# OPTIONS --type-in-type #-}

module Issue1420 where

open import Common.Equality

postulate
  ▶    : Set → Set
  ▷    : ▶ Set → Set
  next : ∀{A}   → A → ▶ A
  _∗_  : ∀{A B} → ▶(A → B) → ▶ A → ▶ B

  ▶-def : ∀ A → ▷ (next A) ≡ ▶ A

  next∗ : ∀{A B : Set} (f : A → B) (a : A) →
          (next f ∗ next a) ≡ next (f a)

  Name : Set

data Tm : Set where
  name  : Name → Tm

data R : Tm → Set where
  name : ∀{x : Name} → R (name x)

print : Tm → ▶ Tm
print (name x) = next (name x)

-- Manually expanded with
test : ∀ (t : Tm) → ▷ (next R ∗ (print t))
test (name x) with next R ∗ next (name x) | next∗ R (name x)
... | ._ | refl rewrite ▶-def (R (name x)) = next name

-- Original rewrite
fails : ∀ (t : Tm) → ▷ (next R ∗ (print t))
fails (name x) rewrite next∗ R (name x) | ▶-def (R (name x)) = next name

-- should succeed

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.String where

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.Equality

postulate String : Set
{-# BUILTIN STRING String #-}

primitive
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringAppend   : String → String → String
  primStringEquality : String → String → Bool
  primShowChar       : Char → String
  primShowString     : String → String
  primStringToListInjective : ∀ a b → primStringToList a ≡ primStringToList b → a ≡ b

{-# COMPILE JS primStringToList = function(x) { return x.split(""); } #-}
{-# COMPILE JS primStringFromList = function(x) { return x.join(""); } #-}
{-# COMPILE JS primStringAppend = function(x) { return function(y) { return x+y; }; } #-}
{-# COMPILE JS primStringEquality = function(x) { return function(y) { return x===y; }; } #-}
{-# COMPILE JS primShowChar = function(x) { return JSON.stringify(x); } #-}
{-# COMPILE JS primShowString = function(x) { return JSON.stringify(x); } #-}

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
{-# OPTIONS --safe --warning=error --without-K --guardedness #-}

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Groups.Homomorphisms.Definition
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order

module Fields.CauchyCompletion.Group {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open TotallyOrderedRing order
open Field F
open Group (Ring.additiveGroup R)
open Ring R

open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Addition order F
open import Fields.CauchyCompletion.Setoid order F

abstract
  +CCommutative : (a b : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (a +C b) (b +C a)
  +CCommutative a b ε 0<e = 0 , ans
    where
      foo : {x y : A} → (x + y) + inverse (y + x) ∼ 0G
      foo = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (inverseWellDefined additiveGroup groupIsAbelian)) invRight
      ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (a +C b)) (map inverse (CauchyCompletion.elts (b +C a)))) m) < ε
      ans {m} 0<m rewrite indexAndApply (CauchyCompletion.elts (a +C b)) (map inverse (CauchyCompletion.elts (b +C a))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _+_ {m} | equalityCommutative (mapAndIndex (apply _+_ (CauchyCompletion.elts b) (CauchyCompletion.elts a)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts a) _+_ {m} = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ foo) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e

private
  abstract
    additionWellDefinedLeft : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a +C c) (b +C c)
    additionWellDefinedLeft record { elts = a ; converges = aConv } record { elts = b ; converges = bConv } record { elts = c ; converges = cConv } a=b ε 0<e with a=b ε 0<e
    ... | Na-b , prA-b = Na-b , ans
      where
        ans : {m : ℕ} → Na-b <N m → abs (index (apply _+_ (apply _+_ a c) (map inverse (apply _+_ b c))) m) < ε
        ans {m} mBig with prA-b {m} mBig
        ... | bl rewrite indexAndApply (apply _+_ a c) (map inverse (apply _+_ b c)) _+_ {m} | indexAndApply a c _+_ {m} | equalityCommutative (mapAndIndex (apply _+_ b c) inverse m) | indexAndApply b c _+_ {m} = <WellDefined (absWellDefined _ _ t) (Equivalence.reflexive eq) bl
          where
            t : index (apply _+_ a (map inverse b)) m ∼ ((index a m + index c m) + inverse (index b m + index c m))
            t rewrite indexAndApply a (map inverse b) _+_ {m} | equalityCommutative (mapAndIndex b inverse m) = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq identLeft) (+WellDefined (Equivalence.symmetric eq invRight) (Equivalence.reflexive eq))) (Equivalence.symmetric eq +Associative)) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (invContravariant additiveGroup))))) (+Associative {index a m})

    additionPreservedLeft : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (injection a +C c) (injection b +C c)
    additionPreservedLeft {a} {b} {c} a=b = additionWellDefinedLeft (injection a) (injection b) c (injectionPreservesSetoid a b a=b)

    additionPreservedRight : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (c +C injection a) (c +C injection b)
    additionPreservedRight {a} {b} {c} a=b = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {c +C injection a} {injection a +C c} {c +C injection b} (+CCommutative c (injection a)) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a +C c} {injection b +C c} {c +C injection b} (additionPreservedLeft {a} {b} {c} a=b) (+CCommutative (injection b) c))

    additionPreserved : {a b c d : A} → (a ∼ b) → (c ∼ d) → Setoid._∼_ cauchyCompletionSetoid (injection a +C injection c) (injection b +C injection d)
    additionPreserved {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a +C injection c} {injection a +C injection d} {injection b +C injection d} (additionPreservedRight {c} {d} {injection a} c=d) (additionPreservedLeft {a} {b} {injection d} a=b)

    additionWellDefinedRight : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid b c → Setoid._∼_ cauchyCompletionSetoid (a +C b) (a +C c)
    additionWellDefinedRight a b c b=c = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a +C b} {b +C a} {a +C c} (+CCommutative a b) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {b +C a} {c +C a} {a +C c} (additionWellDefinedLeft b c a b=c) (+CCommutative c a))

    additionWellDefined : {a b c d : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid c d → Setoid._∼_ cauchyCompletionSetoid (a +C c) (b +C d)
    additionWellDefined {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a +C c} {a +C d} {b +C d} (additionWellDefinedRight a c d c=d) (additionWellDefinedLeft a b d a=b)

    additionHom : (x y : A) → Setoid._∼_ cauchyCompletionSetoid (injection (x + y)) (injection x +C injection y)
    additionHom x y ε 0<e = 0 , ans
      where
        ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (injection (x + y))) (map inverse (CauchyCompletion.elts (injection x +C injection y)))) m) < ε
        ans {m} 0<m rewrite indexAndApply (CauchyCompletion.elts (injection (x + y))) (map inverse (CauchyCompletion.elts (injection x +C injection y))) _+_ {m} | equalityCommutative (mapAndIndex (apply _+_ (constSequence x) (constSequence y)) inverse m) | indexAndConst (x + y) m | indexAndApply (constSequence x) (constSequence y) _+_ {m} | indexAndConst x m | indexAndConst y m = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ invRight) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e

    Cassoc : {a b c : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a +C (b +C c)) ((a +C b) +C c)
    Cassoc {a} {b} {c} ε 0<e = 0 , ans
      where
        ans : {m : ℕ} → 0 <N m → abs (index (CauchyCompletion.elts ((a +C (b +C c)) +C (-C ((a +C b) +C c)))) m) < ε
        ans {m} 0<m rewrite indexAndApply (CauchyCompletion.elts (a +C (b +C c))) (map inverse (CauchyCompletion.elts ((a +C b) +C c))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (apply _+_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)) _+_ {m} | equalityCommutative (mapAndIndex (apply _+_ (apply _+_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (CauchyCompletion.elts c)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts c) _+_ {m} | indexAndApply (apply _+_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (CauchyCompletion.elts c) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _+_ {m} = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (transferToRight'' (Ring.additiveGroup R) +Associative)) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e

    CidentRight : {a : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a +C injection 0G) a
    CidentRight {a} ε 0<e = 0 , ans
      where
        ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (a +C injection 0G)) (map inverse (CauchyCompletion.elts a))) m) < ε
        ans {m} 0<m rewrite indexAndApply (CauchyCompletion.elts (a +C injection 0G)) (map inverse (CauchyCompletion.elts a)) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (constSequence 0G) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) | indexAndConst 0G m = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.transitive eq (+WellDefined (identRight) (Equivalence.reflexive eq)) (invRight))) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e

    CidentLeft : {a : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (injection 0G +C a) a
    CidentLeft {a} = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection 0G +C a} {a +C injection 0G} {a} (+CCommutative (injection 0G) a) (CidentRight {a})

    CinvRight : {a : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a +C (-C a)) (injection 0G)
    CinvRight {a} ε 0<e = 0 , ans
      where
        ans : {m : ℕ} → (0 <N m) → abs (index (apply _+_ (CauchyCompletion.elts (a +C (-C a))) (map inverse (CauchyCompletion.elts (injection 0G)))) m) < ε
        ans {m} 0<m rewrite indexAndApply (CauchyCompletion.elts (a +C (-C a))) (map inverse (CauchyCompletion.elts (injection 0G))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts a)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) | equalityCommutative (mapAndIndex (constSequence 0G) inverse m) | indexAndConst 0G m = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.transitive eq (+WellDefined invRight (invIdent (Ring.additiveGroup R))) identRight)) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e

CGroup : Group cauchyCompletionSetoid _+C_
Group.+WellDefined CGroup {a} {b} {c} {d} x y = additionWellDefined {a} {c} {b} {d} x y
Group.0G CGroup = injection 0G
Group.inverse CGroup = -C_
Group.+Associative CGroup {a} {b} {c} = Cassoc {a} {b} {c}
Group.identRight CGroup {a} = CidentRight {a}
Group.identLeft CGroup {a} = CidentLeft {a}
Group.invLeft CGroup {a} = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {(-C a) +C a} {a +C (-C a)} {injection 0G} (+CCommutative (-C a) a) (CinvRight {a})
Group.invRight CGroup {a} = CinvRight {a}

CInjectionGroupHom : GroupHom (Ring.additiveGroup R) CGroup injection
GroupHom.groupHom CInjectionGroupHom {x} {y} = additionHom x y
GroupHom.wellDefined CInjectionGroupHom {x} {y} x=y = SetoidInjection.wellDefined CInjection {x} {y} x=y


text:
module vector-test where

open import bool
open import nat
open import list
open import vector

test-vector : 𝕍 𝔹 4
test-vector = ff :: tt :: ff :: ff :: []

test-vector2 : 𝕃 (𝕍 𝔹 2)
test-vector2 = (ff :: tt :: []) ::
               (tt :: ff :: []) ::
               (tt :: ff :: []) :: []

test-vector3 : 𝕍 (𝕍 𝔹 3) 2
test-vector3 = (tt :: tt :: tt :: []) ::
               (ff :: ff :: ff :: []) :: []

test-vector-append : 𝕍 𝔹 8
test-vector-append = test-vector ++𝕍 test-vector

test-set-vector : 𝕍 Set 3
test-set-vector = ℕ :: 𝔹 :: (𝔹 → 𝔹) :: []

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.two-semi-categories.Functor
open import lib.two-semi-categories.FundamentalCategory
open import lib.two-semi-categories.FunctorInverse
open import lib.types.Pi using ()

module lib.two-semi-categories.FunextFunctors where

module FunextFunctors {i j} (A : Type i) (B : Type j) {{B-level : has-level 2 B}} where

  open import lib.two-semi-categories.FunCategory

  private

    app=-pres-comp : ∀ {f g h : A → B} (α : f == g) (β : g == h) → app= (α ∙ β) == (λ a → app= α a ∙ app= β a)
    app=-pres-comp α β = λ= (λ a → ap-∙ (λ f → f a) α β)

    abstract
      app=-pres-comp-coh : ∀ {f g h i : A → B} (α : f == g) (β : g == h) (γ : h == i)
        → app=-pres-comp (α ∙ β) γ ◃∙
          ap (λ s a → s a ∙ app= γ a) (app=-pres-comp α β) ◃∙
          λ= (λ a → ∙-assoc (app= α a) (app= β a) (app= γ a)) ◃∎
          =ₛ
          ap app= (∙-assoc α β γ) ◃∙
          app=-pres-comp α (β ∙ γ) ◃∙
          ap (λ s a → app= α a ∙ s a) (app=-pres-comp β γ) ◃∎
      app=-pres-comp-coh {f} idp idp γ =
        app=-pres-comp idp γ ◃∙
        ap (λ s a → s a ∙ app= γ a) (app=-pres-comp idp idp) ◃∙
        λ= (λ a → idp) ◃∎
          =ₛ⟨ 2 & 1 & =ₛ-in {t = []} (! (λ=-η idp)) ⟩
        app=-pres-comp idp γ ◃∙
        ap (λ s a → s a ∙ app= γ a) (λ= (λ a → idp {a = idp {a = f a}})) ◃∎
          =ₛ₁⟨ 1 & 1 & ap (ap (λ s a → s a ∙ app= γ a)) (! (λ=-η idp)) ⟩
        app=-pres-comp idp γ ◃∙
        idp ◃∎
          =ₛ₁⟨ 1 & 1 & ap (ap (λ s → s)) (λ=-η idp) ⟩
        app=-pres-comp idp γ ◃∙
        ap (λ s → s) (λ= (λ a → idp {a = app= γ a})) ◃∎
          =ₛ⟨ 0 & 0 & contract ⟩
        idp ◃∙
        app=-pres-comp idp γ ◃∙
        ap (λ s → s) (λ= (λ a → idp {a = app= γ a})) ◃∎ ∎ₛ

  app=-functor : TwoSemiFunctor (2-type-fundamental-cat (A → B))
                                (fun-cat A (2-type-fundamental-cat B))
  app=-functor =
    record
    { F₀ = idf (A → B)
    ; F₁ = app=
    ; pres-comp = app=-pres-comp
    ; pres-comp-coh = app=-pres-comp-coh
    }

  private
    module app=-functor =
      TwoSemiFunctor app=-functor
    module app=-inverse =
      FunctorInverse
        app=-functor
        (idf-is-equiv _)
        (λ f g → snd app=-equiv)

  λ=-functor : TwoSemiFunctor (fun-cat A (2-type-fundamental-cat B))
                              (2-type-fundamental-cat (A → B))
  λ=-functor = app=-inverse.functor

  module λ=-functor = TwoSemiFunctor λ=-functor

  abstract
    λ=-functor-pres-comp=λ=-∙ : ∀ {f g h : A → B} (α : f ∼ g) (β : g ∼ h)
      → λ=-functor.pres-comp α β == =ₛ-out (λ=-∙ α β)
    λ=-functor-pres-comp=λ=-∙ α β = =ₛ-out {t = =ₛ-out (λ=-∙ α β) ◃∎} $
      λ=-functor.pres-comp α β ◃∎
        =ₛ⟨ app=-inverse.pres-comp-β α β ⟩
      idp ◃∙
      ap2 (λ s t → λ= (λ a → s a ∙ t a)) (! (λ= (app=-β α))) (! (λ= (app=-β β))) ◃∙
      ap λ= (! (λ= (λ a → ap-∙ (λ f → f a) (λ= α) (λ= β)))) ◃∙
      ! (λ=-η (λ= α ∙ λ= β)) ◃∎
        =ₛ⟨ 0 & 1 & expand [] ⟩
      ap2 (λ s t → λ= (λ a → s a ∙ t a)) (! (λ= (app=-β α))) (! (λ= (app=-β β))) ◃∙
      ap λ= (! (λ= (λ a → ap-∙ (λ f → f a) (λ= α) (λ= β)))) ◃∙
      ! (λ=-η (λ= α ∙ λ= β)) ◃∎
        =ₛ₁⟨ 0 & 1 & step₈ ⟩
      ap λ= (! (λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a')))) ◃∙
      ap λ= (! (λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β)))) ◃∙
      ! (λ=-η (λ= α ∙ λ= β)) ◃∎
        =ₛ⟨ 0 & 2 &
            ap-seq-=ₛ λ= $ ∙-!-seq $
            λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β)) ◃∙
            λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a')) ◃∎ ⟩
      ap λ= (! (λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β)) ∙
                λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a')))) ◃∙
      ! (λ=-η (λ= α ∙ λ= β)) ◃∎
        =ₛ₁⟨ 0 & 1 & ap-! λ= (λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β)) ∙
                              λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a'))) ⟩
      ! (ap λ= (λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β)) ∙
                λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a')))) ◃∙
      ! (λ=-η (λ= α ∙ λ= β)) ◃∎
        =ₛ₁⟨ 0 & 1 &
            ap (! ∘ ap λ=) $ =ₛ-out $
            ∙-λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β))
                  (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a')) ⟩
      ! (ap λ= (λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β) ∙
                          ap2 _∙_ (app=-β α a') (app=-β β a')))) ◃∙
      ! (λ=-η (λ= α ∙ λ= β)) ◃∎
        =ₛ⟨ =ₛ-in $
            ∙-! (ap λ= (λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β) ∙
                                          ap2 _∙_ (app=-β α a') (app=-β β a'))))
                (λ=-η (λ= α ∙ λ= β)) ⟩
      ! (λ=-η (λ= α ∙ λ= β) ∙
        ap λ= (λ= (λ a' → ap-∙ (λ γ → γ a') (λ= α) (λ= β) ∙
                          ap2 _∙_ (app=-β α a') (app=-β β a')))) ◃∎ ∎ₛ
      where
      step₈' : ap2 (λ s t a → s a ∙ t a) (λ= (app=-β α)) (λ= (app=-β β)) ==
              λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a'))
      step₈' =
        –>-is-inj app=-equiv _ _ $ λ= $ λ a →
        app= (ap2 (λ s t a' → s a' ∙ t a') (λ= (app=-β α)) (λ= (app=-β β))) a
          =⟨ ap-ap2 (λ f → f a) (λ s t a' → s a' ∙ t a') (λ= (app=-β α)) (λ= (app=-β β)) ⟩
        ap2 (λ s t → s a ∙ t a) (λ= (app=-β α)) (λ= (app=-β β))
          =⟨ ! (ap2-ap-lr _∙_ (λ f → f a) (λ f → f a) (λ= (app=-β α)) (λ= (app=-β β))) ⟩
        ap2 _∙_ (app= (λ= (app=-β α)) a) (app= (λ= (app=-β β)) a)
          =⟨ ap2 (ap2 _∙_) (app=-β (app=-β α) a) (app=-β (app=-β β) a) ⟩
        ap2 _∙_ (app=-β α a) (app=-β β a)
          =⟨ ! (app=-β (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a')) a) ⟩
        app= (λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a'))) a =∎
      step₈ : ap2 (λ s t → λ= (λ a → s a ∙ t a)) (! (λ= (app=-β α))) (! (λ= (app=-β β))) ==
              ap λ= (! (λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a'))))
      step₈ =
        ap2 (λ s t → λ= (λ a → s a ∙ t a)) (! (λ= (app=-β α))) (! (λ= (app=-β β)))
          =⟨ ! (ap-ap2 λ= (λ s t a → s a ∙ t a) (! (λ= (app=-β α))) (! (λ= (app=-β β)))) ⟩
        ap λ= (ap2 (λ s t a → s a ∙ t a) (! (λ= (app=-β α))) (! (λ= (app=-β β))))
          =⟨ ap (ap λ=) (ap2-! (λ s t a → s a ∙ t a) (λ= (app=-β α)) (λ= (app=-β β))) ⟩
        ap λ= (! (ap2 (λ s t a → s a ∙ t a) (λ= (app=-β α)) (λ= (app=-β β))))
          =⟨ ap (ap λ= ∘ !) step₈' ⟩
        ap λ= (! (λ= (λ a' → ap2 _∙_ (app=-β α a') (app=-β β a')))) =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------------
-- An inductive predicate for representing functions
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Data.Fun where

open import FOTC.Base

------------------------------------------------------------------------------
-- 2012-03-13. I don't see how we can distinguish between data
-- elements and functions in FOTC. The following inductive predicate
-- is true for any element d : D.
data Fun : D → Set where
  fun : (f : D) → Fun f

-- But using a λ-abstraction we could make a distinguish:
postulate lam : (D → D) → D  -- LTC-PCF λ-abstraction.

data Fun₁ : D → Set where
  fun₁ : (f : D → D) → Fun₁ (lam f)


text:
-- Andreas, 2020-03-20, issue #4482, reported by gallai
-- Precise range for unexpected implicit argument.

_ : Set → {A : Set} → {B : Set} → {C : Set} → Set
_ = λ { _ {B = B} {A = A} → {!!} }

-- Unexpected implicit argument
-- when checking the clause left hand side
-- .extendedlambda0 _ {B = B} {A = A}
--                                 ^ highlight this

max_forks_repo_name: shlevy/agda