text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc)

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

+-assoc′ : ∀ m n p → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

{-
Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
-}

{-
Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ
-}


text:
{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Coinduction
open import Agda.Builtin.IO
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.String
open import Agda.Builtin.Unit

private
  variable
    A : Set

postulate
  putStrLn : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn #-}

record Stream₁ (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    head : A
    tail : Stream₁ A

open Stream₁

repeat₁ : A → Stream₁ A
repeat₁ x .head = x
repeat₁ x .tail = repeat₁ x

take₁ : Nat → Stream₁ A → List A
take₁ zero    xs = []
take₁ (suc n) xs = xs .head ∷ take₁ n (xs .tail)

data List′ (A : Set) : Set where
  []  : List′ A
  _∷_ : A → List′ A → List′ A

to-list : List′ A → List A
to-list []       = []
to-list (x ∷ xs) = x ∷ to-list xs

data Stream₂ (A : Set) : Set where
  _∷_ : A → ∞ (Stream₂ A) → Stream₂ A

repeat₂ : A → Stream₂ A
repeat₂ x = x ∷ ♯ repeat₂ x

take₂ : Nat → Stream₂ A → List′ A
take₂ zero    _        = []
take₂ (suc n) (x ∷ xs) = x ∷ take₂ n (♭ xs)

_++_ : List A → List′ A → List A
[]       ++ ys = to-list ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

main : IO ⊤
main =
  putStrLn
    (primStringFromList
       (take₁ 3 (repeat₁ '(') ++ take₂ 3 (repeat₂ ')')))

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type
------------------------------------------------------------------------

module Data.Maybe where

open import Level

------------------------------------------------------------------------
-- The type

open import Data.Maybe.Core public

------------------------------------------------------------------------
-- Some operations

open import Data.Bool using (Bool; true; false; not)
open import Data.Unit using (⊤)
open import Function
open import Relation.Nullary

boolToMaybe : Bool → Maybe ⊤
boolToMaybe true  = just _
boolToMaybe false = nothing

is-just : ∀ {a} {A : Set a} → Maybe A → Bool
is-just (just _) = true
is-just nothing  = false

is-nothing : ∀ {a} {A : Set a} → Maybe A → Bool
is-nothing = not ∘ is-just

decToMaybe : ∀ {a} {A : Set a} → Dec A → Maybe A
decToMaybe (yes x) = just x
decToMaybe (no _)  = nothing

-- A dependent eliminator.

maybe : ∀ {a b} {A : Set a} {B : Maybe A → Set b} →
        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

-- A non-dependent eliminator.

maybe′ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Maybe A → B
maybe′ = maybe

-- A safe variant of "fromJust". If the value is nothing, then the
-- return type is the unit type.

From-just : ∀ {a} (A : Set a) → Maybe A → Set a
From-just A (just _) = A
From-just A nothing  = Lift ⊤

from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just A x
from-just (just x) = x
from-just nothing  = _

------------------------------------------------------------------------
-- Maybe monad

open import Category.Functor
open import Category.Monad
open import Category.Monad.Identity

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Maybe A → Maybe B
map f = maybe (just ∘ f) nothing

functor : ∀ {f} → RawFunctor (Maybe {a = f})
functor = record
  { _<$>_ = map
  }

monadT : ∀ {f} {M : Set f → Set f} →
         RawMonad M → RawMonad (λ A → M (Maybe A))
monadT M = record
  { return = M.return ∘ just
  ; _>>=_  = λ m f → M._>>=_ m (maybe f (M.return nothing))
  }
  where module M = RawMonad M

monad : ∀ {f} → RawMonad (Maybe {a = f})
monad = monadT IdentityMonad

monadZero : ∀ {f} → RawMonadZero (Maybe {a = f})
monadZero = record
  { monad = monad
  ; ∅     = nothing
  }

monadPlus : ∀ {f} → RawMonadPlus (Maybe {a = f})
monadPlus {f} = record
  { monadZero = monadZero
  ; _∣_       = _∣_
  }
  where
  _∣_ : {A : Set f} → Maybe A → Maybe A → Maybe A
  nothing ∣ y = y
  just x  ∣ y = just x

------------------------------------------------------------------------
-- Equality

open import Relation.Binary as B

data Eq {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Rel (Maybe A) (a ⊔ ℓ) where
  just    : ∀ {x y} (x≈y : x ≈ y) → Eq _≈_ (just x) (just y)
  nothing : Eq _≈_ nothing nothing

drop-just : ∀ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} {x y : A} →
            just x ⟨ Eq _≈_ ⟩ just y → x ≈ y
drop-just (just x≈y) = x≈y

setoid : ∀ {ℓ₁ ℓ₂} → Setoid ℓ₁ ℓ₂ → Setoid _ _
setoid S = record
  { Carrier       = Maybe S.Carrier
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  module S = Setoid S
  _≈_ = Eq S._≈_

  refl : ∀ {x} → x ≈ x
  refl {just x}  = just S.refl
  refl {nothing} = nothing

  sym : ∀ {x y} → x ≈ y → y ≈ x
  sym (just x≈y) = just (S.sym x≈y)
  sym nothing    = nothing

  trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
  trans (just x≈y) (just y≈z) = just (S.trans x≈y y≈z)
  trans nothing    nothing    = nothing

decSetoid : ∀ {ℓ₁ ℓ₂} → DecSetoid ℓ₁ ℓ₂ → DecSetoid _ _
decSetoid D = record
  { isDecEquivalence = record
    { isEquivalence = Setoid.isEquivalence (setoid (DecSetoid.setoid D))
    ; _≟_           = _≟_
    }
  }
  where
  _≟_ : B.Decidable (Eq (DecSetoid._≈_ D))
  just x  ≟ just y  with DecSetoid._≟_ D x y
  just x  ≟ just y  | yes x≈y = yes (just x≈y)
  just x  ≟ just y  | no  x≉y = no (x≉y ∘ drop-just)
  just x  ≟ nothing = no λ()
  nothing ≟ just y  = no λ()
  nothing ≟ nothing = yes nothing

------------------------------------------------------------------------
-- Any and All

open Data.Bool using (T)
open import Data.Empty using (⊥)
import Relation.Nullary.Decidable as Dec
open import Relation.Unary as U

data Any {a p} {A : Set a} (P : A → Set p) : Maybe A → Set (a ⊔ p) where
  just : ∀ {x} (px : P x) → Any P (just x)

data All {a p} {A : Set a} (P : A → Set p) : Maybe A → Set (a ⊔ p) where
  just    : ∀ {x} (px : P x) → All P (just x)
  nothing : All P nothing

Is-just : ∀ {a} {A : Set a} → Maybe A → Set a
Is-just = Any (λ _ → ⊤)

Is-nothing : ∀ {a} {A : Set a} → Maybe A → Set a
Is-nothing = All (λ _ → ⊥)

to-witness : ∀ {p} {P : Set p} {m : Maybe P} → Is-just m → P
to-witness (just {x = p} _) = p

to-witness-T : ∀ {p} {P : Set p} (m : Maybe P) → T (is-just m) → P
to-witness-T (just p) _  = p
to-witness-T nothing  ()

anyDec : ∀ {a p} {A : Set a} {P : A → Set p} →
         U.Decidable P → U.Decidable (Any P)
anyDec p nothing  = no λ()
anyDec p (just x) = Dec.map′ just (λ { (Any.just px) → px }) (p x)

allDec : ∀ {a p} {A : Set a} {P : A → Set p} →
         U.Decidable P → U.Decidable (All P)
allDec p nothing  = yes nothing
allDec p (just x) = Dec.map′ just (λ { (All.just px) → px }) (p x)


text:
module Issue2762-2 where

open import Agda.Builtin.List
open import Agda.Builtin.Equality

pattern [_] x = x ∷ []

singleton : {A : Set} → A → List A
singleton x = x ∷ []

{-# DISPLAY _∷_ x [] = singleton x #-}

_ : ∀ {A} (x : A) → singleton x ≡ [ x ]
_ = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
import Lvl

module Type.Functions.Proofs {ℓₗ : Lvl.Level} where

open import Functional
import      Function.Domains
import      Lang.Irrelevance
import      Logic.Predicate
import      Logic.Predicate.Theorems
import      Relator.Equals
import      Relator.Equals.Proofs
open import Type
open import Type.Properties.Empty
import      Type.Functions
import      Type.Singleton.Proofs
open import Type.Properties.Singleton
open import Type.Properties.Singleton.Proofs

module _ {ℓₒ₁}{ℓₒ₂} {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} {f : X → Y} where
  open Type.Functions {ℓₗ}{ℓₒ₁}{ℓₒ₂} {X}{Y}

  bijective-to-injective : ⦃ bij : Bijective(f) ⦄ → Injective(f)
  Injective.proof (bijective-to-injective ⦃ intro proof ⦄) {y} =
    unit-is-prop {ℓₒ₁} ⦃ proof{y} ⦄

  bijective-to-surjective : ⦃ bij : Bijective(f) ⦄ → Surjective(f)
  Surjective.proof (bijective-to-surjective ⦃ intro proof ⦄) {y} =
    unit-is-pos {ℓₗ Lvl.⊔ ℓₒ₁} ⦃ proof{y} ⦄

  injective-surjective-to-bijective : ⦃ inj : Injective(f) ⦄ → ⦃ surj : Surjective(f) ⦄ → Bijective(f)
  Bijective.proof(injective-surjective-to-bijective ⦃ intro inj ⦄ ⦃ intro surj ⦄) {y} =
    pos-prop-is-unit {ℓₗ Lvl.⊔ ℓₒ₁} ⦃ surj{y} ⦄ ⦃ inj{y} ⦄

module _ {ℓₒ₁}{ℓₒ₂} {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} {f : X → Y} where
  open Function.Domains
  open Type.Functions {ℓₗ}{ℓₒ₁}{ℓₒ₂} {X}{Y}
  open Relator.Equals

  private
    _≡₁_ = _≡_ {ℓₗ Lvl.⊔ ℓₒ₁}

  Injective-apply : ⦃ _ : Injective(f) ⦄ → ∀{x y} → (f(x) ≡₁ f(y)) → (x ≡₁ y)
  Injective-apply ⦃ Injective.intro proof ⦄ {x}{y} (fxfy) with proof{f(y)}
  ... | MereProposition.intro uniqueness with uniqueness{Unapply.intro x ⦃ fxfy ⦄} {Unapply.intro y ⦃ [≡]-intro ⦄}
  ...   | [≡]-intro = [≡]-intro

module _ {ℓₒ : Lvl.Level} {X : Type{ℓₒ}} where
  open Type.Functions {ℓₗ Lvl.⊔ ℓₒ}{ℓₒ}{ℓₒ} {X}{X}
  open Type.Singleton.Proofs {ℓₗ}{ℓₒ} {X}

  instance
    id-is-bijective : Bijective(id)
    id-is-bijective = intro Singleton-is-unit

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Agda.Builtin.Nat

record C (A : Set) : Set where

module M (X : Set) where
  module Ci = C {{...}}

module CiNat = M.Ci Nat -- error: The module M.Ci is not parameterized...


text:
module map-is-fold-Tree where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning

open import map-Tree using (Tree; leaf; node; map-Tree)
open import fold-Tree using (fold-Tree)

postulate
  -- 外延性の公理
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- 外延性の公理を利用した証明のための補題
lemma : ∀ {A B C D : Set} → (f : A → C) → (g : B → D) → (tree : Tree A B)
  → map-Tree f g tree ≡ fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ) tree
lemma f g (leaf a) =
  begin
    map-Tree f g (leaf a)
  ≡⟨⟩
    leaf (f a)
  ≡⟨⟩
    fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ) (leaf a)
  ∎
lemma f g (node treeˡ b treeʳ) =
  begin
    map-Tree f g (node treeˡ b treeʳ)
  ≡⟨⟩
    node (map-Tree f g treeˡ) (g b) (map-Tree f g treeʳ)
  ≡⟨ cong (λ treeʳ′ → node (map-Tree f g treeˡ) (g b) treeʳ′) (lemma f g treeʳ) ⟩
    node (map-Tree f g treeˡ)
         (g b)
         (fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ) treeʳ)
  ≡⟨ cong (λ treeˡ′ → node treeˡ′
                           (g b)
                           (fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ) treeʳ))
          (lemma f g treeˡ) ⟩
    node (fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ) treeˡ)
         (g b)
         (fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ) treeʳ)
  ≡⟨⟩
    fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ) (node treeˡ b treeʳ)
  ∎

-- Treeのmapが畳み込みで表現できることの証明
map-is-fold-Tree : ∀ {A B C D : Set} → (f : A → C) → (g : B → D)
  → map-Tree f g ≡ fold-Tree (λ a → leaf (f a)) (λ treeˡ b treeʳ → node treeˡ (g b) treeʳ)
map-is-fold-Tree f g = extensionality (lemma f g)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Type(s) used (only) when calling out to Haskell via the FFI
------------------------------------------------------------------------

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

module Foreign.Haskell where

open import Level

------------------------------------------------------------------------
-- Pairs

open import Foreign.Haskell.Pair public
  renaming
  ( toForeign   to toForeignPair
  ; fromForeign to fromForeignPair
  )

------------------------------------------------------------------------
-- Sums

open import Foreign.Haskell.Either public
  renaming
  ( toForeign   to toForeignEither
  ; fromForeign to fromForeignEither
  )

------------------------------------------------------------------------
-- Maybe

open import Foreign.Haskell.Maybe public
  renaming
  ( toForeign   to toForeignMaybe
  ; fromForeign to fromForeignMaybe
  )

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

open import Data.Unit using (⊤; tt)

-- Version 1.1

Unit = ⊤
{-# WARNING_ON_USAGE Unit
"Warning: Unit was deprecated in v1.1.
Please use ⊤ from Data.Unit instead."
#-}
unit = tt
{-# WARNING_ON_USAGE unit
"Warning: unit was deprecated in v1.1.
Please use tt from Data.Unit instead."
#-}


text:
open import Nat
open import Prelude
open import List
open import contexts

module core where
  -- types
  data typ : Set where
    b     : typ
    ⦇·⦈    : typ
    _==>_ : typ → typ → typ
    _⊗_   : typ → typ → typ

  -- arrow type constructors bind very tightly
  infixr 25  _==>_
  infixr 25  _⊗_

  -- we use natural numbers as names throughout the development. here we
  -- provide some aliases to that the definitions below are more readable
  -- about what's being named, even though the underlying implementations
  -- are the same and there's no abstraction protecting you from breaking
  -- invariants.

  -- written `x` in math
  varname : Set
  varname = Nat

  -- written `u` in math
  holename : Set
  holename = Nat

  -- written `a` in math
  livelitname : Set
  livelitname = Nat

  -- "external expressions", or the middle layer of expressions. presented
  -- first because of the dependence structure below.
  data eexp : Set where
    c       : eexp
    _·:_    : eexp → typ → eexp
    X       : varname → eexp
    ·λ      : varname → eexp → eexp
    ·λ_[_]_ : varname → typ → eexp → eexp
    ⦇⦈[_]   : holename → eexp
    ⦇⌜_⌟⦈[_] : eexp → holename → eexp
    _∘_     : eexp → eexp → eexp
    ⟨_,_⟩   : eexp → eexp → eexp
    fst     : eexp → eexp
    snd     : eexp → eexp

  -- the type of type contexts, i.e. Γs in the judegments below
  tctx : Set
  tctx = typ ctx

  mutual
    -- identity substitution, substitition environments
    data env : Set where
      Id : (Γ : tctx) → env
      Subst : (d : iexp) → (y : varname) → env → env

    -- internal expressions, the bottom most layer of expresions. these are
    -- what the elaboration phase targets and the expressions on which
    -- evaluation is given.
    data iexp : Set where
      c         : iexp
      X         : varname → iexp
      ·λ_[_]_   : varname → typ → iexp → iexp
      ⦇⦈⟨_⟩     : (holename × env) → iexp
      ⦇⌜_⌟⦈⟨_⟩    : iexp → (holename × env) → iexp
      _∘_       : iexp → iexp → iexp
      _⟨_⇒_⟩    : iexp → typ → typ → iexp
      _⟨_⇒⦇⦈⇏_⟩ : iexp → typ → typ → iexp
      ⟨_,_⟩   : iexp → iexp → iexp
      fst     : iexp → iexp
      snd     : iexp → iexp

  -- convenient notation for chaining together two agreeable casts
  _⟨_⇒_⇒_⟩ : iexp → typ → typ → typ → iexp
  d ⟨ τ1 ⇒ τ2 ⇒ τ3 ⟩ = d ⟨ τ1 ⇒ τ2 ⟩ ⟨ τ2 ⇒ τ3 ⟩

  record livelitdef : Set where
    field
      expand : iexp
      model-type : typ
      expansion-type : typ

  -- unexpanded expressions, the outermost layer of expressions: a langauge
  -- exactly like eexp, but also with livelits
  mutual
    data uexp : Set where
      c       : uexp
      _·:_    : uexp → typ → uexp
      X       : varname → uexp
      ·λ      : varname → uexp → uexp
      ·λ_[_]_ : varname → typ → uexp → uexp
      ⦇⦈[_]   : holename → uexp
      ⦇⌜_⌟⦈[_]  : uexp → holename → uexp
      _∘_     : uexp → uexp → uexp
      ⟨_,_⟩   : uexp → uexp → uexp
      fst     : uexp → uexp
      snd     : uexp → uexp
      -- new forms below
      ＄_⟨_⁏_⟩[_] : (a : livelitname) → (d : iexp) → (ϕᵢ : List splice) → (u : holename) → uexp

    splice : Set
    splice = typ × uexp

  -- type consistency
  data _~_ : (t1 t2 : typ) → Set where
    TCRefl  : {τ : typ} → τ ~ τ
    TCHole1 : {τ : typ} → τ ~ ⦇·⦈
    TCHole2 : {τ : typ} → ⦇·⦈ ~ τ
    TCArr   : {τ1 τ2 τ1' τ2' : typ} →
               τ1 ~ τ1' →
               τ2 ~ τ2' →
               τ1 ==> τ2 ~ τ1' ==> τ2'
    TCProd  : {τ1 τ2 τ1' τ2' : typ} →
               τ1 ~ τ1' →
               τ2 ~ τ2' →
               (τ1 ⊗ τ2) ~ (τ1' ⊗ τ2')

  -- type inconsistency
  data _~̸_ : (τ1 τ2 : typ) → Set where
    ICBaseArr1 : {τ1 τ2 : typ} → b ~̸ τ1 ==> τ2
    ICBaseArr2 : {τ1 τ2 : typ} → τ1 ==> τ2 ~̸ b
    ICArr1 : {τ1 τ2 τ3 τ4 : typ} →
               τ1 ~̸ τ3 →
               τ1 ==> τ2 ~̸ τ3 ==> τ4
    ICArr2 : {τ1 τ2 τ3 τ4 : typ} →
               τ2 ~̸ τ4 →
               τ1 ==> τ2 ~̸ τ3 ==> τ4
    ICBaseProd1 : {τ1 τ2 : typ} → b ~̸ τ1 ⊗ τ2
    ICBaseProd2 : {τ1 τ2 : typ} → τ1 ⊗ τ2 ~̸ b
    ICProdArr1 : {τ1 τ2 τ3 τ4 : typ} →
                τ1 ==> τ2 ~̸ τ3 ⊗ τ4
    ICProdArr2 : {τ1 τ2 τ3 τ4 : typ} →
                τ1 ⊗ τ2 ~̸ τ3 ==> τ4
    ICProd1 : {τ1 τ2 τ3 τ4 : typ} →
               τ1 ~̸ τ3 →
               τ1 ⊗ τ2 ~̸ τ3 ⊗ τ4
    ICProd2 : {τ1 τ2 τ3 τ4 : typ} →
               τ2 ~̸ τ4 →
               τ1 ⊗ τ2 ~̸ τ3 ⊗ τ4

  --- matching for arrows
  data _▸arr_ : typ → typ → Set where
    MAHole : ⦇·⦈ ▸arr ⦇·⦈ ==> ⦇·⦈
    MAArr  : {τ1 τ2 : typ} → τ1 ==> τ2 ▸arr τ1 ==> τ2

  -- matching for products
  data _▸prod_ : typ → typ → Set where
    MPHole : ⦇·⦈ ▸prod ⦇·⦈ ⊗ ⦇·⦈
    MPProd  : {τ1 τ2 : typ} → τ1 ⊗ τ2 ▸prod τ1 ⊗ τ2

  -- the type of hole contexts, i.e. Δs in the judgements
  hctx : Set
  hctx = (typ ctx × typ) ctx

  -- notation for a triple to match the CMTT syntax
  _::_[_] : holename → typ → tctx → (holename × (tctx × typ))
  u :: τ [ Γ ] = u , (Γ , τ)

  -- the hole name u does not appear in the term e
  data hole-name-new : (e : eexp) (u : holename) → Set where
    HNConst : ∀{u} → hole-name-new c u
    HNAsc : ∀{e τ u} →
            hole-name-new e u →
            hole-name-new (e ·: τ) u
    HNVar : ∀{x u} → hole-name-new (X x) u
    HNLam1 : ∀{x e u} →
             hole-name-new e u →
             hole-name-new (·λ x e) u
    HNLam2 : ∀{x e u τ} →
             hole-name-new e u →
             hole-name-new (·λ x [ τ ] e) u
    HNHole : ∀{u u'} →
             u' ≠ u →
             hole-name-new (⦇⦈[ u' ]) u
    HNNEHole : ∀{u u' e} →
               u' ≠ u →
               hole-name-new e u →
               hole-name-new (⦇⌜ e ⌟⦈[ u' ]) u
    HNAp : ∀{ u e1 e2 } →
           hole-name-new e1 u →
           hole-name-new e2 u →
           hole-name-new (e1 ∘ e2) u
    HNFst  : ∀{ u e } →
           hole-name-new e u →
           hole-name-new (fst e) u
    HNSnd  : ∀{ u e } →
           hole-name-new e u →
           hole-name-new (snd e) u
    HNPair : ∀{ u e1 e2 } →
           hole-name-new e1 u →
           hole-name-new e2 u →
           hole-name-new ⟨ e1 , e2 ⟩ u

  -- two terms that do not share any hole names
  data holes-disjoint : (e1 : eexp) → (e2 : eexp) → Set where
    HDConst : ∀{e} → holes-disjoint c e
    HDAsc : ∀{e1 e2 τ} → holes-disjoint e1 e2 → holes-disjoint (e1 ·: τ) e2
    HDVar : ∀{x e} → holes-disjoint (X x) e
    HDLam1 : ∀{x e1 e2} → holes-disjoint e1 e2 → holes-disjoint (·λ x e1) e2
    HDLam2 : ∀{x e1 e2 τ} → holes-disjoint e1 e2 → holes-disjoint (·λ x [ τ ] e1) e2
    HDHole : ∀{u e2} → hole-name-new e2 u → holes-disjoint (⦇⦈[ u ]) e2
    HDNEHole : ∀{u e1 e2} → hole-name-new e2 u → holes-disjoint e1 e2 → holes-disjoint (⦇⌜ e1 ⌟⦈[ u ]) e2
    HDAp :  ∀{e1 e2 e3} → holes-disjoint e1 e3 → holes-disjoint e2 e3 → holes-disjoint (e1 ∘ e2) e3
    HDFst  : ∀{e1 e2} → holes-disjoint e1 e2 → holes-disjoint (fst e1) e2
    HDSnd  : ∀{e1 e2} → holes-disjoint e1 e2 → holes-disjoint (snd e1) e2
    HDPair : ∀{e1 e2 e3} → holes-disjoint e1 e3 → holes-disjoint e2 e3 → holes-disjoint ⟨ e1 , e2 ⟩ e3

  -- bidirectional type checking judgements for eexp
  mutual
    -- synthesis
    data _⊢_=>_ : (Γ : tctx) (e : eexp) (τ : typ) → Set where
      SConst  : {Γ : tctx} → Γ ⊢ c => b
      SAsc    : {Γ : tctx} {e : eexp} {τ : typ} →
                 Γ ⊢ e <= τ →
                 Γ ⊢ (e ·: τ) => τ
      SVar    : {Γ : tctx} {τ : typ} {x : varname} →
                 (x , τ) ∈ Γ →
                 Γ ⊢ X x => τ
      SAp     : {Γ : tctx} {e1 e2 : eexp} {τ τ1 τ2 : typ} →
                 holes-disjoint e1 e2 →
                 Γ ⊢ e1 => τ1 →
                 τ1 ▸arr τ2 ==> τ →
                 Γ ⊢ e2 <= τ2 →
                 Γ ⊢ (e1 ∘ e2) => τ
      SEHole  : {Γ : tctx} {u : holename} → Γ ⊢ ⦇⦈[ u ] => ⦇·⦈
      SNEHole : {Γ : tctx} {e : eexp} {τ : typ} {u : holename} →
                 hole-name-new e u →
                 Γ ⊢ e => τ →
                 Γ ⊢ ⦇⌜ e ⌟⦈[ u ] => ⦇·⦈
      SLam    : {Γ : tctx} {e : eexp} {τ1 τ2 : typ} {x : varname} →
                 x # Γ →
                 (Γ ,, (x , τ1)) ⊢ e => τ2 →
                 Γ ⊢ ·λ x [ τ1 ] e => τ1 ==> τ2
      SFst    : ∀{ e τ τ1 τ2 Γ} →
                Γ ⊢ e => τ →
                τ ▸prod τ1 ⊗ τ2 →
                Γ ⊢ fst e => τ1
      SSnd    : ∀{ e τ τ1 τ2 Γ} →
                Γ ⊢ e => τ →
                τ ▸prod τ1 ⊗ τ2 →
                Γ ⊢ snd e => τ2
      SPair   : ∀{ e1 e2 τ1 τ2 Γ} →
                holes-disjoint e1 e2 →
                Γ ⊢ e1 => τ1 →
                Γ ⊢ e2 => τ2 →
                Γ ⊢ ⟨ e1 , e2 ⟩ => τ1 ⊗ τ2

    -- analysis
    data _⊢_<=_ : (Γ : tctx) (e : eexp) (τ : typ) → Set where
      ASubsume : {Γ : tctx} {e : eexp} {τ τ' : typ} →
                 Γ ⊢ e => τ' →
                 τ ~ τ' →
                 Γ ⊢ e <= τ
      ALam : {Γ : tctx} {e : eexp} {τ τ1 τ2 : typ} {x : varname} →
                 x # Γ →
                 τ ▸arr τ1 ==> τ2 →
                 (Γ ,, (x , τ1)) ⊢ e <= τ2 →
                 Γ ⊢ (·λ x e) <= τ

  -- those types without holes
  data _tcomplete : typ → Set where
    TCBase : b tcomplete
    TCArr : ∀{τ1 τ2} → τ1 tcomplete → τ2 tcomplete → (τ1 ==> τ2) tcomplete
    TCProd : ∀{τ1 τ2} → τ1 tcomplete → τ2 tcomplete → (τ1 ⊗ τ2) tcomplete

  -- those external expressions without holes
  data _ecomplete : eexp → Set where
    ECConst : c ecomplete
    ECAsc : ∀{τ e} → τ tcomplete → e ecomplete → (e ·: τ) ecomplete
    ECVar : ∀{x} → (X x) ecomplete
    ECLam1 : ∀{x e} → e ecomplete → (·λ x e) ecomplete
    ECLam2 : ∀{x e τ} → e ecomplete → τ tcomplete → (·λ x [ τ ] e) ecomplete
    ECAp : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → (e1 ∘ e2) ecomplete
    ECFst : ∀{e} → e ecomplete → (fst e) ecomplete
    ECSnd : ∀{e} → e ecomplete → (snd e) ecomplete
    ECPair : ∀{e1 e2} → e1 ecomplete → e2 ecomplete → ⟨ e1 , e2 ⟩ ecomplete

  -- those internal expressions without holes
  data _dcomplete : iexp → Set where
    DCVar : ∀{x} → (X x) dcomplete
    DCConst : c dcomplete
    DCLam : ∀{x τ d} → d dcomplete → τ tcomplete → (·λ x [ τ ] d) dcomplete
    DCAp : ∀{d1 d2} → d1 dcomplete → d2 dcomplete → (d1 ∘ d2) dcomplete
    DCCast : ∀{d τ1 τ2} → d dcomplete → τ1 tcomplete → τ2 tcomplete → (d ⟨ τ1 ⇒ τ2 ⟩) dcomplete
    DCFst : ∀{d} → d dcomplete → (fst d) dcomplete
    DCSnd : ∀{d} → d dcomplete → (snd d) dcomplete
    DCPair : ∀{d1 d2} → d1 dcomplete → d2 dcomplete → ⟨ d1 , d2 ⟩ dcomplete

  -- contexts that only produce complete types
  _gcomplete : tctx → Set
  Γ gcomplete = (x : varname) (τ : typ) → (x , τ) ∈ Γ → τ tcomplete

  -- those internal expressions where every cast is the identity cast and
  -- there are no failed casts
  data cast-id : iexp → Set where
    CIConst  : cast-id c
    CIVar    : ∀{x} → cast-id (X x)
    CILam    : ∀{x τ d} → cast-id d → cast-id (·λ x [ τ ] d)
    CIHole   : ∀{u} → cast-id (⦇⦈⟨ u ⟩)
    CINEHole : ∀{d u} → cast-id d → cast-id (⦇⌜ d ⌟⦈⟨ u ⟩)
    CIAp     : ∀{d1 d2} → cast-id d1 → cast-id d2 → cast-id (d1 ∘ d2)
    CICast   : ∀{d τ} → cast-id d → cast-id (d ⟨ τ ⇒ τ ⟩)
    CIFst    : ∀{d} → cast-id d → cast-id (fst d)
    CISnd    : ∀{d} → cast-id d → cast-id (snd d)
    CIPair   : ∀{d1 d2} → cast-id d1 → cast-id d2 → cast-id ⟨ d1 , d2 ⟩

  -- expansion
  mutual
    -- synthesis
    data _⊢_⇒_~>_⊣_ : (Γ : tctx) (e : eexp) (τ : typ) (d : iexp) (Δ : hctx) → Set where
      ESConst : ∀{Γ} → Γ ⊢ c ⇒ b ~> c ⊣ ∅
      ESVar   : ∀{Γ x τ} → (x , τ) ∈ Γ →
                         Γ ⊢ X x ⇒ τ ~> X x ⊣ ∅
      ESLam   : ∀{Γ x τ1 τ2 e d Δ } →
                     (x # Γ) →
                     (Γ ,, (x , τ1)) ⊢ e ⇒ τ2 ~> d ⊣ Δ →
                      Γ ⊢ ·λ x [ τ1 ] e ⇒ (τ1 ==> τ2) ~> ·λ x [ τ1 ] d ⊣ Δ
      ESAp : ∀{Γ e1 τ τ1 τ1' τ2 τ2' d1 Δ1 e2 d2 Δ2 } →
              holes-disjoint e1 e2 →
              Δ1 ## Δ2 →
              Γ ⊢ e1 => τ1 →
              τ1 ▸arr τ2 ==> τ →
              Γ ⊢ e1 ⇐ (τ2 ==> τ) ~> d1 :: τ1' ⊣ Δ1 →
              Γ ⊢ e2 ⇐ τ2 ~> d2 :: τ2' ⊣ Δ2 →
              Γ ⊢ e1 ∘ e2 ⇒ τ ~> (d1 ⟨ τ1' ⇒ τ2 ==> τ ⟩) ∘ (d2 ⟨ τ2' ⇒ τ2 ⟩) ⊣ (Δ1 ∪ Δ2)
      ESEHole : ∀{ Γ u } →
                Γ ⊢ ⦇⦈[ u ] ⇒ ⦇·⦈ ~> ⦇⦈⟨ u , Id Γ ⟩ ⊣  ■ (u :: ⦇·⦈ [ Γ ])
      ESNEHole : ∀{ Γ e τ d u Δ } →
                 Δ ## (■ (u , Γ , ⦇·⦈)) →
                 Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                 Γ ⊢ ⦇⌜ e ⌟⦈[ u ] ⇒ ⦇·⦈ ~> ⦇⌜ d ⌟⦈⟨ u , Id Γ  ⟩ ⊣ (Δ ,, u :: ⦇·⦈ [ Γ ])
      ESAsc : ∀ {Γ e τ d τ' Δ} →
                 Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                 Γ ⊢ (e ·: τ) ⇒ τ ~> d ⟨ τ' ⇒ τ ⟩ ⊣ Δ
      ESFst  : ∀{Γ e τ τ' d τ1 τ2 Δ} →
                 Γ ⊢ e => τ →
                 τ ▸prod τ1 ⊗ τ2 →
                 Γ ⊢ e ⇐ τ1 ⊗ τ2 ~> d :: τ' ⊣ Δ →
                 Γ ⊢ fst e ⇒ τ1 ~> fst (d ⟨ τ' ⇒ τ1 ⊗ τ2 ⟩) ⊣ Δ
      ESSnd  : ∀{Γ e τ τ' d τ1 τ2 Δ} →
                 Γ ⊢ e => τ →
                 τ ▸prod τ1 ⊗ τ2 →
                 Γ ⊢ e ⇐ τ1 ⊗ τ2 ~> d :: τ' ⊣ Δ →
                 Γ ⊢ snd e ⇒ τ2 ~> snd (d ⟨ τ' ⇒ τ1 ⊗ τ2 ⟩) ⊣ Δ
      ESPair : ∀{Γ e1 τ1 d1 Δ1 e2 τ2 d2 Δ2} →
                 holes-disjoint e1 e2 →
                 Δ1 ## Δ2 →
                 Γ ⊢ e1 ⇒ τ1 ~> d1 ⊣ Δ1 →
                 Γ ⊢ e2 ⇒ τ2 ~> d2 ⊣ Δ2 →
                 Γ ⊢ ⟨ e1 , e2 ⟩ ⇒ τ1 ⊗ τ2 ~> ⟨ d1 , d2 ⟩ ⊣ (Δ1 ∪ Δ2)

    -- analysis
    data _⊢_⇐_~>_::_⊣_ : (Γ : tctx) (e : eexp) (τ : typ) (d : iexp) (τ' : typ) (Δ : hctx) → Set where
      EALam : ∀{Γ x τ τ1 τ2 e d τ2' Δ } →
              (x # Γ) →
              τ ▸arr τ1 ==> τ2 →
              (Γ ,, (x , τ1)) ⊢ e ⇐ τ2 ~> d :: τ2' ⊣ Δ →
              Γ ⊢ ·λ x e ⇐ τ ~> ·λ x [ τ1 ] d :: τ1 ==> τ2' ⊣ Δ
      EASubsume : ∀{e Γ τ' d Δ τ} →
                  ((u : holename) → e ≠ ⦇⦈[ u ]) →
                  ((e' : eexp) (u : holename) → e ≠ ⦇⌜ e' ⌟⦈[ u ]) →
                  Γ ⊢ e ⇒ τ' ~> d ⊣ Δ →
                  τ ~ τ' →
                  Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ
      EAEHole : ∀{ Γ u τ  } →
                Γ ⊢ ⦇⦈[ u ] ⇐ τ ~> ⦇⦈⟨ u , Id Γ  ⟩ :: τ ⊣ ■ (u :: τ [ Γ ])
      EANEHole : ∀{ Γ e u τ d τ' Δ  } →
                 Δ ## (■ (u , Γ , τ)) →
                 Γ ⊢ e ⇒ τ' ~> d ⊣ Δ →
                 Γ ⊢ ⦇⌜ e ⌟⦈[ u ] ⇐ τ ~> ⦇⌜ d ⌟⦈⟨ u , Id Γ  ⟩ :: τ ⊣ (Δ ,, u :: τ [ Γ ])

  -- ground types
  data _ground : (τ : typ) → Set where
    GBase : b ground
    GHole : ⦇·⦈ ==> ⦇·⦈ ground
    GProd : ⦇·⦈ ⊗ ⦇·⦈ ground

  mutual
    -- substitution typing
    data _,_⊢_:s:_ : hctx → tctx → env → tctx → Set where
      STAId : ∀{Γ Γ' Δ} →
                  ((x : varname) (τ : typ) → (x , τ) ∈ Γ' → (x , τ) ∈ Γ) →
                  Δ , Γ ⊢ Id Γ' :s: Γ'
      STASubst : ∀{Γ Δ σ y Γ' d τ } →
               Δ , Γ ,, (y , τ) ⊢ σ :s: Γ' →
               Δ , Γ ⊢ d :: τ →
               Δ , Γ ⊢ Subst d y σ :s: Γ'

    -- type assignment
    data _,_⊢_::_ : (Δ : hctx) (Γ : tctx) (d : iexp) (τ : typ) → Set where
      TAConst : ∀{Δ Γ} → Δ , Γ ⊢ c :: b
      TAVar : ∀{Δ Γ x τ} → (x , τ) ∈ Γ → Δ , Γ ⊢ X x :: τ
      TALam : ∀{ Δ Γ x τ1 d τ2} →
              x # Γ →
              Δ , (Γ ,, (x , τ1)) ⊢ d :: τ2 →
              Δ , Γ ⊢ ·λ x [ τ1 ] d :: (τ1 ==> τ2)
      TAAp : ∀{ Δ Γ d1 d2 τ1 τ} →
             Δ , Γ ⊢ d1 :: τ1 ==> τ →
             Δ , Γ ⊢ d2 :: τ1 →
             Δ , Γ ⊢ d1 ∘ d2 :: τ
      TAEHole : ∀{ Δ Γ σ u Γ' τ} →
                (u , (Γ' , τ)) ∈ Δ →
                Δ , Γ ⊢ σ :s: Γ' →
                Δ , Γ ⊢ ⦇⦈⟨ u , σ ⟩ :: τ
      TANEHole : ∀ { Δ Γ d τ' Γ' u σ τ } →
                 (u , (Γ' , τ)) ∈ Δ →
                 Δ , Γ ⊢ d :: τ' →
                 Δ , Γ ⊢ σ :s: Γ' →
                 Δ , Γ ⊢ ⦇⌜ d ⌟⦈⟨ u , σ ⟩ :: τ
      TACast : ∀{ Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 →
             τ1 ~ τ2 →
             Δ , Γ ⊢ d ⟨ τ1 ⇒ τ2 ⟩ :: τ2
      TAFailedCast : ∀{Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 →
             τ1 ground →
             τ2 ground →
             τ1 ≠ τ2 →
             Δ , Γ ⊢ d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩ :: τ2
      TAFst : ∀{Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 ⊗ τ2 →
             Δ , Γ ⊢ fst d :: τ1
      TASnd : ∀{Δ Γ d τ1 τ2} →
             Δ , Γ ⊢ d :: τ1 ⊗ τ2 →
             Δ , Γ ⊢ snd d :: τ2
      TAPair : ∀{Δ Γ d1 d2 τ1 τ2} →
             Δ , Γ ⊢ d1 :: τ1 →
             Δ , Γ ⊢ d2 :: τ2 →
             Δ , Γ ⊢ ⟨ d1 , d2 ⟩ :: τ1 ⊗ τ2

  -- substitution
  [_/_]_ : iexp → varname → iexp → iexp
  [ d / y ] c = c
  [ d / y ] X x
    with natEQ x y
  [ d / y ] X .y | Inl refl = d
  [ d / y ] X x  | Inr neq = X x
  [ d / y ] (·λ x [ x₁ ] d')
    with natEQ x y
  [ d / y ] (·λ .y [ τ ] d') | Inl refl = ·λ y [ τ ] d'
  [ d / y ] (·λ x [ τ ] d')  | Inr x₁ = ·λ x [ τ ] ( [ d / y ] d')
  [ d / y ] ⦇⦈⟨ u , σ ⟩ = ⦇⦈⟨ u , Subst d y σ ⟩
  [ d / y ] ⦇⌜ d' ⌟⦈⟨ u , σ  ⟩ =  ⦇⌜ [ d / y ] d' ⌟⦈⟨ u , Subst d y σ ⟩
  [ d / y ] (d1 ∘ d2) = ([ d / y ] d1) ∘ ([ d / y ] d2)
  [ d / y ] (d' ⟨ τ1 ⇒ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒ τ2 ⟩
  [ d / y ] (d' ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩
  [ d / y ] ⟨ d1 , d2 ⟩ = ⟨ [ d / y ] d1 , [ d / y ] d2 ⟩
  [ d / y ] (fst d') = fst ([ d / y ] d')
  [ d / y ] (snd d') = snd ([ d / y ] d')

  -- applying an environment to an expression
  apply-env : env → iexp → iexp
  apply-env (Id Γ) d = d
  apply-env (Subst d y σ) d' = [ d / y ] ( apply-env σ d')

  -- values
  data _val : (d : iexp) → Set where
    VConst : c val
    VLam   : ∀{x τ d} → (·λ x [ τ ] d) val
    VPair  : ∀{d1 d2} → d1 val → d2 val → ⟨ d1 , d2 ⟩ val

  -- boxed values
  data _boxedval : (d : iexp) → Set where
    BVVal : ∀{d} → d val → d boxedval
    BVPair : ∀{d1 d2} → d1 boxedval → d2 boxedval → ⟨ d1 , d2 ⟩ boxedval
    BVArrCast : ∀{ d τ1 τ2 τ3 τ4 } →
                τ1 ==> τ2 ≠ τ3 ==> τ4 →
                d boxedval →
                d ⟨ (τ1 ==> τ2) ⇒ (τ3 ==> τ4) ⟩ boxedval
    BVProdCast : ∀{ d τ1 τ2 τ3 τ4 } →
                τ1 ⊗ τ2 ≠ τ3 ⊗ τ4 →
                d boxedval →
                d ⟨ (τ1 ⊗ τ2) ⇒ (τ3 ⊗ τ4) ⟩ boxedval
    BVHoleCast : ∀{ τ d } → τ ground → d boxedval → d ⟨ τ ⇒ ⦇·⦈ ⟩ boxedval

  mutual
    -- indeterminate forms
    data _indet : (d : iexp) → Set where
      IEHole : ∀{u σ} → ⦇⦈⟨ u , σ ⟩ indet
      INEHole : ∀{d u σ} → d final → ⦇⌜ d ⌟⦈⟨ u , σ ⟩ indet
      IAp : ∀{d1 d2} → ((τ1 τ2 τ3 τ4 : typ) (d1' : iexp) →
                       d1 ≠ (d1' ⟨(τ1 ==> τ2) ⇒ (τ3 ==> τ4)⟩)) →
                       d1 indet →
                       d2 final →
                       (d1 ∘ d2) indet
      IFst   : ∀{d} →
               d indet →
               (∀{d1 d2} → d ≠ ⟨ d1 , d2 ⟩) →
               (∀{d' τ1 τ2 τ3 τ4} → d ≠ (d' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩)) →
               (fst d) indet
      ISnd   : ∀{d} →
               d indet →
               (∀{d1 d2} → d ≠ ⟨ d1 , d2 ⟩) →
               (∀{d' τ1 τ2 τ3 τ4} → d ≠ (d' ⟨ τ1 ⊗ τ2 ⇒ τ3 ⊗ τ4 ⟩)) →
               (snd d) indet
      IPair1 : ∀{d1 d2} →
               d1 indet →
               d2 final →
               ⟨ d1 , d2 ⟩ indet
      IPair2 : ∀{d1 d2} →
               d1 final →
               d2 indet →
               ⟨ d1 , d2 ⟩ indet
      ICastArr : ∀{d τ1 τ2 τ3 τ4} →
                 τ1 ==> τ2 ≠ τ3 ==> τ4 →
                 d indet →
                 d ⟨ (τ1 ==> τ2) ⇒ (τ3 ==> τ4) ⟩ indet
      ICastProd : ∀{d τ1 τ2 τ3 τ4} →
                 τ1 ⊗ τ2 ≠ τ3 ⊗ τ4 →
                 d indet →
                 d ⟨ (τ1 ⊗ τ2) ⇒ (τ3 ⊗ τ4) ⟩ indet
      ICastGroundHole : ∀{ τ d } →
                        τ ground →
                        d indet →
                        d ⟨ τ ⇒  ⦇·⦈ ⟩ indet
      ICastHoleGround : ∀ { d τ } →
                        ((d' : iexp) (τ' : typ) → d ≠ (d' ⟨ τ' ⇒ ⦇·⦈ ⟩)) →
                        d indet →
                        τ ground →
                        d ⟨ ⦇·⦈ ⇒ τ ⟩ indet
      IFailedCast : ∀{ d τ1 τ2 } →
                    d final →
                    τ1 ground →
                    τ2 ground →
                    τ1 ≠ τ2 →
                    d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩ indet

    -- final expressions
    data _final : (d : iexp) → Set where
      FBoxedVal : ∀{d} → d boxedval → d final
      FIndet    : ∀{d} → d indet    → d final

  -- contextual dynamics

  -- evaluation contexts
  data ectx : Set where
    ⊙ : ectx
    _∘₁_ : ectx → iexp → ectx
    _∘₂_ : iexp → ectx → ectx
    ⦇⌜_⌟⦈⟨_⟩ : ectx → (holename × env ) → ectx
    fst·_ : ectx → ectx
    snd·_ : ectx → ectx
    ⟨_,_⟩₁ : ectx → iexp → ectx
    ⟨_,_⟩₂ : iexp → ectx → ectx
    _⟨_⇒_⟩ : ectx → typ → typ → ectx
    _⟨_⇒⦇·⦈⇏_⟩ : ectx → typ → typ → ectx

  -- note: this judgement is redundant: in the absence of the premises in
  -- the red brackets, all syntactically well formed ectxs are valid. with
  -- finality premises, that's not true, and that would propagate through
  -- additions to the calculus. so we leave it here for clarity but note
  -- that, as written, in any use case its either trival to prove or
  -- provides no additional information

   --ε is an evaluation context
  data _evalctx : (ε : ectx) → Set where
    ECDot : ⊙ evalctx
    ECAp1 : ∀{d ε} →
            ε evalctx →
            (ε ∘₁ d) evalctx
    ECAp2 : ∀{d ε} →
            -- d final → -- red brackets
            ε evalctx →
            (d ∘₂ ε) evalctx
    ECNEHole : ∀{ε u σ} →
               ε evalctx →
               ⦇⌜ ε ⌟⦈⟨ u , σ ⟩ evalctx
    ECFst   : ∀{ε} →
              (fst· ε) evalctx
    ECSnd   : ∀{ε} →
              (snd· ε) evalctx
    ECPair1 : ∀{d ε} →
              ε evalctx →
              ⟨ ε , d ⟩₁ evalctx
    ECPair2 : ∀{d ε} →
              -- d final → -- red brackets
              ε evalctx →
              ⟨ d , ε ⟩₂ evalctx
    ECCast : ∀{ ε τ1 τ2} →
             ε evalctx →
             (ε ⟨ τ1 ⇒ τ2 ⟩) evalctx
    ECFailedCast : ∀{ ε τ1 τ2 } →
                   ε evalctx →
                   ε ⟨ τ1 ⇒⦇·⦈⇏ τ2 ⟩ evalctx

  -- d is the result of filling the hole in ε with d'
  data _==_⟦_⟧ : (d : iexp) (ε : ectx) (d' : iexp) → Set where
    FHOuter : ∀{d} → d == ⊙ ⟦ d ⟧
    FHAp1 : ∀{d1 d1' d2 ε} →
           d1 == ε ⟦ d1' ⟧ →
           (d1 ∘ d2) == (ε ∘₁ d2) ⟦ d1' ⟧
    FHAp2 : ∀{d1 d2 d2' ε} →
           -- d1 final → -- red brackets
           d2 == ε ⟦ d2' ⟧ →
           (d1 ∘ d2) == (d1 ∘₂ ε) ⟦ d2' ⟧
    FHNEHole : ∀{ d d' ε u σ} →
              d == ε ⟦ d' ⟧ →
              ⦇⌜ d ⌟⦈⟨ (u , σ ) ⟩ ==  ⦇⌜ ε ⌟⦈⟨ (u , σ ) ⟩ ⟦ d' ⟧
    FHFst   : ∀{d d' ε} →
              d == ε ⟦ d' ⟧ →
              fst d == (fst· ε) ⟦ d' ⟧
    FHSnd   : ∀{d d' ε} →
              d == ε ⟦ d' ⟧ →
              snd d == (snd· ε) ⟦ d' ⟧
    FHPair1 : ∀{d1 d1' d2 ε} →
              d1 == ε ⟦ d1' ⟧ →
              ⟨ d1 , d2 ⟩ == ⟨ ε , d2 ⟩₁ ⟦ d1' ⟧
    FHPair2 : ∀{d1 d2 d2' ε} →
              d2 == ε ⟦ d2' ⟧ →
              ⟨ d1 , d2 ⟩ == ⟨ d1 , ε ⟩₂ ⟦ d2' ⟧
    FHCast : ∀{ d d' ε τ1 τ2 } →
            d == ε ⟦ d' ⟧ →
            d ⟨ τ1 ⇒ τ2 ⟩ == ε ⟨ τ1 ⇒ τ2 ⟩ ⟦ d' ⟧
    FHFailedCast : ∀{ d d' ε τ1 τ2} →
            d == ε ⟦ d' ⟧ →
            (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩) == (ε ⟨ τ1 ⇒⦇·⦈⇏ τ2 ⟩) ⟦ d' ⟧

  -- matched ground types
  data _▸gnd_ : typ → typ → Set where
    MGArr : ∀{τ1 τ2} →
            (τ1 ==> τ2) ≠ (⦇·⦈ ==> ⦇·⦈) →
            (τ1 ==> τ2) ▸gnd (⦇·⦈ ==> ⦇·⦈)
    MGProd : ∀{τ1 τ2} →
            (τ1 ⊗ τ2) ≠ (⦇·⦈ ⊗ ⦇·⦈) →
            (τ1 ⊗ τ2) ▸gnd (⦇·⦈ ⊗ ⦇·⦈)

  -- instruction transition judgement
  data _→>_ : (d d' : iexp) → Set where
    ITLam : ∀{ x τ d1 d2 } →
            -- d2 final → -- red brackets
            ((·λ x [ τ ] d1) ∘ d2) →> ([ d2 / x ] d1)
    ITFst : ∀{d1 d2} →
            -- d1 final → -- red brackets
            -- d2 final → -- red brackets
            fst ⟨ d1 , d2 ⟩ →> d1
    ITSnd : ∀{d1 d2} →
            -- d1 final → -- red brackets
            -- d2 final → -- red brackets
            snd ⟨ d1 , d2 ⟩ →> d2
    ITCastID : ∀{d τ } →
               -- d final → -- red brackets
               (d ⟨ τ ⇒ τ ⟩) →> d
    ITCastSucceed : ∀{d τ } →
                    -- d final → -- red brackets
                    τ ground →
                    (d ⟨ τ ⇒ ⦇·⦈ ⇒ τ ⟩) →> d
    ITCastFail : ∀{ d τ1 τ2} →
                 -- d final → -- red brackets
                 τ1 ground →
                 τ2 ground →
                 τ1 ≠ τ2 →
                 (d ⟨ τ1 ⇒ ⦇·⦈ ⇒ τ2 ⟩) →> (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩)
    ITApCast : ∀{d1 d2 τ1 τ2 τ1' τ2' } →
               -- d1 final → -- red brackets
               -- d2 final → -- red brackets
               ((d1 ⟨ (τ1 ==> τ2) ⇒ (τ1' ==> τ2')⟩) ∘ d2) →> ((d1 ∘ (d2 ⟨ τ1' ⇒ τ1 ⟩)) ⟨ τ2 ⇒ τ2' ⟩)
    ITFstCast : ∀{d τ1 τ2 τ1' τ2' } →
               -- d final → -- red brackets
               fst (d ⟨ τ1 ⊗ τ2 ⇒ τ1' ⊗ τ2' ⟩) →> ((fst d) ⟨ τ1 ⇒ τ1' ⟩)
    ITSndCast : ∀{d τ1 τ2 τ1' τ2' } →
               -- d final → -- red brackets
               snd (d ⟨ τ1 ⊗ τ2 ⇒ τ1' ⊗ τ2' ⟩) →> ((snd d) ⟨ τ2 ⇒ τ2' ⟩)
    ITGround : ∀{ d τ τ'} →
               -- d final → -- red brackets
               τ ▸gnd τ' →
               (d ⟨ τ ⇒ ⦇·⦈ ⟩) →> (d ⟨ τ ⇒ τ' ⇒ ⦇·⦈ ⟩)
    ITExpand : ∀{d τ τ' } →
               -- d final → -- red brackets
               τ ▸gnd τ' →
               (d ⟨ ⦇·⦈ ⇒ τ ⟩) →> (d ⟨ ⦇·⦈ ⇒ τ' ⇒ τ ⟩)

  -- single step (in contextual evaluation sense)
  data _↦_ : (d d' : iexp) → Set where
    Step : ∀{ d d0 d' d0' ε} →
           d == ε ⟦ d0 ⟧ →
           d0 →> d0' →
           d' == ε ⟦ d0' ⟧ →
           d ↦ d'

  -- reflexive transitive closure of single steps into multi steps
  data _↦*_ : (d d' : iexp) → Set where
    MSRefl : ∀{d} → d ↦* d
    MSStep : ∀{d d' d''} →
                 d ↦ d' →
                 d' ↦* d'' →
                 d  ↦* d''

  -- freshness
  mutual
    -- ... with respect to a hole context
    data envfresh : varname → env → Set where
      EFId : ∀{x Γ} → x # Γ → envfresh x (Id Γ)
      EFSubst : ∀{x d σ y} → fresh x d
                           → envfresh x σ
                           → x ≠ y
                           → envfresh x (Subst d y σ)

    -- ... for inernal expressions
    data fresh : varname → iexp → Set where
      FConst : ∀{x} → fresh x c
      FVar   : ∀{x y} → x ≠ y → fresh x (X y)
      FLam   : ∀{x y τ d} → x ≠ y → fresh x d → fresh x (·λ y [ τ ] d)
      FHole  : ∀{x u σ} → envfresh x σ → fresh x (⦇⦈⟨ u , σ ⟩)
      FNEHole : ∀{x d u σ} → envfresh x σ → fresh x d → fresh x (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      FAp     : ∀{x d1 d2} → fresh x d1 → fresh x d2 → fresh x (d1 ∘ d2)
      FCast   : ∀{x d τ1 τ2} → fresh x d → fresh x (d ⟨ τ1 ⇒ τ2 ⟩)
      FFailedCast : ∀{x d τ1 τ2} → fresh x d → fresh x (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩)
      FFst  : ∀{x d} → fresh x d → fresh x (fst d)
      FSnd  : ∀{x d} → fresh x d → fresh x (snd d)
      FPair : ∀{x d1 d2} → fresh x d1 → fresh x d2 → fresh x ⟨ d1 , d2 ⟩

  -- ... for external expressions
  data freshe : varname → eexp → Set where
    FRHConst : ∀{x} → freshe x c
    FRHAsc   : ∀{x e τ} → freshe x e → freshe x (e ·: τ)
    FRHVar   : ∀{x y} → x ≠ y → freshe x (X y)
    FRHLam1  : ∀{x y e} → x ≠ y → freshe x e → freshe x (·λ y e)
    FRHLam2  : ∀{x τ e y} → x ≠ y → freshe x e → freshe x (·λ y [ τ ] e)
    FRHEHole : ∀{x u} → freshe x (⦇⦈[ u ])
    FRHNEHole : ∀{x u e} → freshe x e → freshe x (⦇⌜ e ⌟⦈[ u ])
    FRHAp : ∀{x e1 e2} → freshe x e1 → freshe x e2 → freshe x (e1 ∘ e2)
    FRHFst  : ∀{x e} → freshe x e → freshe x (fst e)
    FRHSnd  : ∀{x e} → freshe x e → freshe x (snd e)
    FRHPair : ∀{x e1 e2} → freshe x e1 → freshe x e2 → freshe x ⟨ e1 , e2 ⟩

  -- with respect to all bindings in a context
  freshΓ : {A : Set} → (Γ : A ctx) → (e : eexp) → Set
  freshΓ {A} Γ e = (x : varname) → dom Γ x → freshe x e

  -- x is not used in a binding site in d
  mutual
    data unbound-in-σ : varname → env → Set where
      UBσId : ∀{x Γ} → unbound-in-σ x (Id Γ)
      UBσSubst : ∀{x d y σ} → unbound-in x d
                            → unbound-in-σ x σ
                            → x ≠ y
                            → unbound-in-σ x (Subst d y σ)

    data unbound-in : (x : varname) (d : iexp) → Set where
      UBConst : ∀{x} → unbound-in x c
      UBVar : ∀{x y} → unbound-in x (X y)
      UBLam2 : ∀{x d y τ} → x ≠ y
                           → unbound-in x d
                           → unbound-in x (·λ_[_]_ y τ d)
      UBHole : ∀{x u σ} → unbound-in-σ x σ
                         → unbound-in x (⦇⦈⟨ u , σ ⟩)
      UBNEHole : ∀{x u σ d }
                  → unbound-in-σ x σ
                  → unbound-in x d
                  → unbound-in x (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      UBAp : ∀{ x d1 d2 } →
            unbound-in x d1 →
            unbound-in x d2 →
            unbound-in x (d1 ∘ d2)
      UBCast : ∀{x d τ1 τ2} → unbound-in x d → unbound-in x (d ⟨ τ1 ⇒ τ2 ⟩)
      UBFailedCast : ∀{x d τ1 τ2} → unbound-in x d → unbound-in x (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩)
      UBFst  : ∀{x d} → unbound-in x d → unbound-in x (fst d)
      UBSnd  : ∀{x d} → unbound-in x d → unbound-in x (snd d)
      UBPair : ∀{x d1 d2} → unbound-in x d1 → unbound-in x d2 → unbound-in x ⟨ d1 , d2 ⟩

  mutual
    remove-from-free' : varname → eexp → List varname
    remove-from-free' x e = remove-all natEQ (free-vars e) x

    free-vars : (e : eexp) → List varname
    free-vars c = []
    free-vars (e ·: τ) = free-vars e
    free-vars (X x) = x :: []
    free-vars (·λ x e) = remove-from-free' x e
    free-vars (·λ x [ τ ] e) = remove-from-free' x e
    free-vars ⦇⦈[ u ] = []
    free-vars ⦇⌜ e ⌟⦈[ u ] = free-vars e
    free-vars (e₁ ∘ e₂) = free-vars e₁ ++ free-vars e₂
    free-vars ⟨ x , x₁ ⟩ = free-vars x ++ free-vars x₁
    free-vars (fst x) = free-vars x
    free-vars (snd x) = free-vars x

  mutual
    data binders-disjoint-σ : env → iexp → Set where
      BDσId : ∀{Γ d} → binders-disjoint-σ (Id Γ) d
      BDσSubst : ∀{d1 d2 y σ} → binders-disjoint d1 d2
                              → binders-disjoint-σ σ d2
                              → binders-disjoint-σ (Subst d1 y σ) d2

    -- two terms that do not share any binders
    data binders-disjoint : (d1 : iexp) → (d2 : iexp) → Set where
      BDConst : ∀{d} → binders-disjoint c d
      BDVar : ∀{x d} → binders-disjoint (X x) d
      BDLam : ∀{x τ d1 d2} → binders-disjoint d1 d2
                            → unbound-in x d2
                            → binders-disjoint (·λ_[_]_ x τ d1) d2
      BDHole : ∀{u σ d2} → binders-disjoint-σ σ d2
                         → binders-disjoint (⦇⦈⟨ u , σ ⟩) d2
      BDNEHole : ∀{u σ d1 d2} → binders-disjoint-σ σ d2
                              → binders-disjoint d1 d2
                              → binders-disjoint (⦇⌜ d1 ⌟⦈⟨ u , σ ⟩) d2
      BDAp :  ∀{d1 d2 d3} → binders-disjoint d1 d3
                          → binders-disjoint d2 d3
                          → binders-disjoint (d1 ∘ d2) d3
      BDCast : ∀{d1 d2 τ1 τ2} → binders-disjoint d1 d2 → binders-disjoint (d1 ⟨ τ1 ⇒ τ2 ⟩) d2
      BDFailedCast : ∀{d1 d2 τ1 τ2} → binders-disjoint d1 d2 → binders-disjoint (d1 ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩) d2
      BDFst  : ∀{d1 d2} → binders-disjoint d1 d2 → binders-disjoint (fst d1) d2
      BDSnd  : ∀{d1 d2} → binders-disjoint d1 d2 → binders-disjoint (snd d1) d2
      BDPair : ∀{d1 d2 d3} →
               binders-disjoint d1 d3 →
               binders-disjoint d2 d3 →
               binders-disjoint ⟨ d1 , d2 ⟩ d3

  mutual
  -- each term has to be binders unique, and they have to be pairwise
  -- disjoint with the collection of bound vars
    data binders-unique-σ : env → Set where
      BUσId : ∀{Γ} → binders-unique-σ (Id Γ)
      BUσSubst : ∀{d y σ} → binders-unique d
                          → binders-unique-σ σ
                          → binders-disjoint-σ σ d
                          → binders-unique-σ (Subst d y σ)

    -- all the variable names in the term are unique
    data binders-unique : iexp → Set where
      BUHole : binders-unique c
      BUVar : ∀{x} → binders-unique (X x)
      BULam : {x : varname} {τ : typ} {d : iexp} → binders-unique d
                                                → unbound-in x d
                                                → binders-unique (·λ_[_]_ x τ d)
      BUEHole : ∀{u σ} → binders-unique-σ σ
                        → binders-unique (⦇⦈⟨ u , σ ⟩)
      BUNEHole : ∀{u σ d} → binders-unique d
                           → binders-unique-σ σ
                           → binders-unique (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      BUAp : ∀{d1 d2} → binders-unique d1
                       → binders-unique d2
                       → binders-disjoint d1 d2
                       → binders-unique (d1 ∘ d2)
      BUCast : ∀{d τ1 τ2} → binders-unique d
                           → binders-unique (d ⟨ τ1 ⇒ τ2 ⟩)
      BUFailedCast : ∀{d τ1 τ2} → binders-unique d
                                 → binders-unique (d ⟨ τ1 ⇒⦇⦈⇏ τ2 ⟩)
      BUFst  : ∀{d} →
               binders-unique d →
               binders-unique (fst d)
      BUSnd  : ∀{d} →
               binders-unique d →
               binders-unique (snd d)
      BUPair : ∀{d1 d2} →
               binders-unique d1 →
               binders-unique d2 →
               binders-disjoint d1 d2 →
               binders-unique ⟨ d1 , d2 ⟩

  _⇓_ : iexp → iexp → Set
  d1 ⇓ d2 = (d1 ↦* d2 × d2 final)

  -- this is the decoding function, so half the iso. this won't work long term
  postulate
    _↑_ : iexp → eexp → Set
    _↓_ : eexp → iexp → Set
    iso : Set
    Exp : typ

-- naming conventions:
--
-- type contexts, tctx, are named Γ (because they always are)
-- hole contextst, ??, are named Δ
--
-- types, typ, are named τ
-- unexpanded expressions, uexp, are named ê (for "_e_xpression but also following the POPL17 notation)
-- expanded expressions, eexp, are named e (for "_e_xpression")
-- internal expressions, iexp, are named d (because they have a _d_ynamics)
-- splices are named ψ

  -- function-like livelit context well-formedness
  mutual
    livelitctx = Σ[ Φ' ∈ livelitdef ctx ] (Φ' livelitctx')

    data _livelitctx' : (Φ' : livelitdef ctx) → Set where
      PhiWFEmpty     : ∅ livelitctx'
      PhiWFMac       : ∀{a π} →
                          (Φ : livelitctx) →
                           a # π1 Φ →
                           (π1 Φ ,, (a , π)) livelitctx'

  _₁ : (Φ : livelitctx) → livelitdef ctx
  _₁ = π1

  infixr 25 _₁

  _,,_::_⦅given_⦆ : (Φ : livelitctx) →
                 (a : livelitname) →
                 livelitdef →
                 a # (Φ)₁ →
                 livelitctx
  Φ ,, a :: π ⦅given #h ⦆ = ((Φ)₁ ,, (a , π) , PhiWFMac Φ #h)

  -- livelit expansion
  mutual
    data _,_⊢_~~>_⇒_ : (Φ : livelitctx) →
                       (Γ : tctx) →
                       (ê : uexp) →
                       (e : eexp) →
                       (τ : typ) →
                       Set
      where
        SPEConst : ∀{Φ Γ} → Φ , Γ ⊢ c ~~> c ⇒ b
        SPEAsc   : ∀{Φ Γ ê e τ} →
                           Φ , Γ ⊢ ê ~~> e ⇐ τ →
                           Φ , Γ ⊢ (ê ·: τ) ~~> e ·: τ ⇒ τ
        SPEVar   : ∀{Φ Γ x τ} →
                           (x , τ) ∈ Γ →
                           Φ , Γ ⊢ (X x) ~~> (X x) ⇒ τ
        SPELam   : ∀{Φ Γ x e τ1 τ2 ê} →
                           x # Γ →
                           Φ , Γ ,, (x , τ1) ⊢ ê ~~> e ⇒ τ2 →
                           Φ , Γ ⊢ (·λ_[_]_ x τ1 ê) ~~> (·λ x [ τ1 ] e) ⇒ (τ1 ==> τ2)
        SPEAp    : ∀{Φ Γ ê1 ê2 τ1 τ2 τ e1 e2} →
                           Φ , Γ ⊢ ê1 ~~> e1 ⇒ τ1 →
                           τ1 ▸arr τ2 ==> τ →
                           Φ , Γ ⊢ ê2 ~~> e2 ⇐ τ2 →
                           holes-disjoint e1 e2 →
                           Φ , Γ ⊢ ê1 ∘ ê2 ~~> e1 ∘ e2 ⇒ τ
        SPEHole  : ∀{Φ Γ u} → Φ , Γ ⊢ ⦇⦈[ u ] ~~> ⦇⦈[ u ] ⇒ ⦇·⦈
        SPNEHole : ∀{Φ Γ ê e τ u} →
                           hole-name-new e u →
                           Φ , Γ ⊢ ê ~~> e ⇒ τ →
                           Φ , Γ ⊢ ⦇⌜ ê ⌟⦈[ u ] ~~> ⦇⌜ e ⌟⦈[ u ] ⇒ ⦇·⦈
        SPEFst   : ∀{Φ Γ ê e τ τ1 τ2} →
                           Φ , Γ ⊢ ê ~~> e ⇒ τ →
                           τ ▸prod τ1 ⊗ τ2 →
                           Φ , Γ ⊢ fst ê ~~> fst e ⇒ τ1
        SPESnd   : ∀{Φ Γ ê e τ τ1 τ2} →
                           Φ , Γ ⊢ ê ~~> e ⇒ τ →
                           τ ▸prod τ1 ⊗ τ2 →
                           Φ , Γ ⊢ snd ê ~~> snd e ⇒ τ2
        SPEPair  : ∀{Φ Γ ê1 ê2 τ1 τ2 e1 e2} →
                           Φ , Γ ⊢ ê1 ~~> e1 ⇒ τ1 →
                           Φ , Γ ⊢ ê2 ~~> e2 ⇒ τ2 →
                           holes-disjoint e1 e2 →
                           Φ , Γ ⊢ ⟨ ê1 , ê2 ⟩ ~~> ⟨ e1 , e2 ⟩ ⇒ τ1 ⊗ τ2
        SPEApLivelit  : ∀{Φ Γ a dm π denc eexpanded τsplice psplice esplice u} →
                         holes-disjoint eexpanded esplice →
                         freshΓ Γ eexpanded →
                         (a , π) ∈ (Φ)₁ →
                         ∅ , ∅ ⊢ dm :: (livelitdef.model-type π) →
                         ((livelitdef.expand π) ∘ dm) ⇓ denc →
                         denc ↑ eexpanded →
                         Φ , Γ ⊢ psplice ~~> esplice ⇐ τsplice →
                         ∅ ⊢ eexpanded <= τsplice ==> (livelitdef.expansion-type π) →
                         Φ , Γ ⊢ ＄ a ⟨ dm ⁏ (τsplice , psplice) :: [] ⟩[ u ] ~~> ((eexpanded ·: τsplice ==> livelitdef.expansion-type π) ∘ esplice) ⇒ livelitdef.expansion-type π

    data _,_⊢_~~>_⇐_ : (Φ : livelitctx) →
                       (Γ : tctx) →
                       (ê : uexp) →
                       (e : eexp) →
                       (τ : typ) →
                       Set
      where
        APELam     : ∀{Φ Γ x e τ τ1 τ2 ê} →
                           x # Γ →
                           τ ▸arr τ1 ==> τ2 →
                           Φ , Γ ,, (x , τ1) ⊢ ê ~~> e ⇐ τ2 →
                           Φ , Γ ⊢ (·λ x ê) ~~> (·λ x e) ⇐ τ
        APESubsume : ∀{Φ Γ ê e τ τ'} →
                           Φ , Γ ⊢ ê ~~> e ⇒ τ' →
                           τ ~ τ' →
                           Φ , Γ ⊢ ê ~~> e ⇐ τ

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
open import Prelude

module Implicits.Resolution.Finite.Expressiveness where

open import Coinduction
open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Resolution.Deterministic.Resolution as D
open import Implicits.Resolution.Ambiguous.Resolution as A
open import Implicits.Resolution.Finite.Resolution as F
open import Implicits.Resolution.Infinite.Resolution as ∞
open import Implicits.Resolution.Termination

module Finite⊆Infinite where

  p : ∀ {ν} {a} {Δ : ICtx ν} → Δ F.⊢ᵣ a → Δ ∞.⊢ᵣ a
  p (r-simp a a↓τ) = r-simp a (lem a↓τ)
    where
      lem : ∀ {ν} {a τ} {Δ : ICtx ν} → Δ F.⊢ a ↓ τ → Δ ∞.⊢ a ↓ τ
      lem (i-simp τ) = i-simp τ
      lem (i-iabs _ ⊢ᵣa b↓τ) = i-iabs (p ⊢ᵣa) (lem b↓τ)
      lem (i-tabs b a[/b]↓τ) = i-tabs b (lem a[/b]↓τ)
  p (r-iabs x) = r-iabs (p x)
  p (r-tabs x) = r-tabs (p x)

module Finite⊆Ambiguous where

  p : ∀ {ν} {a} {Δ : ICtx ν} → Δ F.⊢ᵣ a → Δ A.⊢ᵣ a
  p (r-simp a a↓τ) = lem a↓τ (r-ivar a)
    where
      lem : ∀ {ν} {a τ} {Δ : ICtx ν} → Δ F.⊢ a ↓ τ → Δ A.⊢ᵣ a → Δ A.⊢ᵣ simpl τ
      lem (i-simp τ) K⊢ᵣτ = K⊢ᵣτ
      lem (i-iabs _ ⊢ᵣa b↓τ) K⊢ᵣa⇒b = lem b↓τ (r-iapp K⊢ᵣa⇒b (p ⊢ᵣa))
      lem (i-tabs b a[/b]↓τ) K⊢ᵣ∀a = lem a[/b]↓τ (r-tapp b K⊢ᵣ∀a)
  p (r-iabs x) = r-iabs (p x)
  p (r-tabs x) = r-tabs (p x)

module Deterministic⊆Finite where

  open import Extensions.ListFirst

  -- Oliveira's termination condition is part of the well-formdness of types
  -- So we assume here that ⊢term x holds for all types x
  p : ∀ {ν} {a : Type ν} {Δ : ICtx ν} → (∀ {ν} (a : Type ν) → ⊢term a) → Δ D.⊢ᵣ a → Δ F.⊢ᵣ a
  p term (r-simp {ρ = r} x r↓a) =
    r-simp (proj₁ $ first⟶∈ x) (lem r↓a)
    where
      lem : ∀ {ν} {Δ : ICtx ν} {a r} → Δ D.⊢ r ↓ a → Δ F.⊢ r ↓ a
      lem (i-simp a) = i-simp a
      lem (i-iabs {ρ₁ = ρ₁} {ρ₂ = ρ₂} ⊢ᵣρ₁ ρ₂↓τ) with term (ρ₁ ⇒ ρ₂)
      lem (i-iabs ⊢ᵣρ₁ ρ₂↓τ) | term-iabs _ _ a-ρ<-b _ = i-iabs a-ρ<-b (p term ⊢ᵣρ₁) (lem ρ₂↓τ)
      lem (i-tabs b x₁) = i-tabs b (lem x₁)
  p term (r-iabs ρ₁ {ρ₂ = ρ₂} x) = r-iabs (p term x)
  p term (r-tabs x) = r-tabs (p term x)


text:
module Numeral.Natural.LinearSearchDecidable where -- TODO: Maybe move and rename to Numeral.Natural.Sequence.BoundedSearch
-- TODO: Maybe more natural to use 𝕟 (finite naturals) instead of ℕ (naturals)?

open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.List
import      Data.List.Functions as List
open import Data.List.Relation.Membership using (_∈_)
open import Data.List.Relation.Membership.Proofs
open import Data.List.Relation.Quantification
open import Data.List.Relation.Quantification.Proofs
open import Data.List.Sorting
open import Data.Option
import      Data.Option.Functions as Option
open import Functional
open import Logic.Propositional
open import Numeral.Finite
import      Numeral.Finite.LinearSearch as 𝕟
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation.Order
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function

private variable a b n i j : ℕ
private variable f : ℕ → Bool

{-
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.Option
import      Data.Option.Functions as Option
open import Functional
open import Logic
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Relation.Order
open import Structure.Relator.Ordering

-- Finds the maximal argument satisfying the given argument within the given search upper bound by searching linearly.
-- Examples:
--   findUpperBoundedMax(10 ∣?_) 5   = None
--   findUpperBoundedMax(10 ∣?_) 20  = Some 20
--   findUpperBoundedMax(10 ∣?_) 22  = Some 20
--   findUpperBoundedMax(10 ∣?_) 100 = Some 100
--   findUpperBoundedMax(10 ∣?_) 102 = Some 100
findUpperBoundedMax : (ℕ → Bool) → ℕ → Option(ℕ)
findUpperBoundedMax f(i) with f(i)
findUpperBoundedMax f(i)    | 𝑇 = Some i
findUpperBoundedMax f(𝟎)    | 𝐹 = None
findUpperBoundedMax f(𝐒(i)) | 𝐹 = findUpperBoundedMax f(i)

findMaxIndexInRange : (ℕ → Bool) → ℕ → ℕ → Option(ℕ)
findMaxIndexInRange f min max = Option.map (_+ min) (findUpperBoundedMax (f ∘ (_+ min)) (max −₀ min))

-- Finds the minimal argument satisfying the given argument within the given search upper bound by searching linearly.
-- Examples:
--   findUpperBoundedMin(10 ∣?_) 5   = None
--   findUpperBoundedMin(10 ∣?_) 20  = Some 10
--   findUpperBoundedMin(10 ∣?_) 22  = Some 10
--   findUpperBoundedMin(10 ∣?_) 100 = Some 10
--   findUpperBoundedMax(10 ∣?_) 102 = Some 10
findUpperBoundedMin : (ℕ → Bool) → ℕ → Option(ℕ)
findUpperBoundedMin f(i) with f(𝟎)
findUpperBoundedMin f(i)    | 𝑇 = Some 𝟎
findUpperBoundedMin f(𝟎)    | 𝐹 = None
findUpperBoundedMin f(𝐒(i)) | 𝐹 = Option.map 𝐒 (findUpperBoundedMin (f ∘ 𝐒)(i))

open import Data
open import Data.Boolean.Stmt.Proofs
open import Data.Option.Equiv.Id
open import Lang.Inspect
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function.Domain
open import Structure.Relator.Properties
open import Structure.Relator

findUpperBoundedMax-correctness : ∀{f}{max i} → (findUpperBoundedMax f(max) ≡ Some(i)) → ((i ≤ max) ∧ IsTrue(f(i)))
findUpperBoundedMax-correctness {f} {max}    {i} p with f(max) | inspect f(max)
findUpperBoundedMax-correctness {f} {max}    {.max} [≡]-intro | 𝑇 | intro eq = [∧]-intro (reflexivity(_≤_)) (substitute₁ₗ(IsTrue) eq <>)
findUpperBoundedMax-correctness {f} {𝟎}      {i}    ()        | 𝐹 | _
findUpperBoundedMax-correctness {f} {𝐒(max)} {i}    p         | 𝐹 | intro eq with findUpperBoundedMax-correctness {f} {max} {i} p
... | [∧]-intro a b = [∧]-intro ([≤]-successor a) b

findUpperBoundedMin-correctness : ∀{f}{max i} → (findUpperBoundedMin f(max) ≡ Some(i)) → ((i ≤ max) ∧ IsTrue(f(i)))
findUpperBoundedMin-correctness {f} {max}   {i}   p with f(𝟎) | inspect f(𝟎)
findUpperBoundedMin-correctness {f} {max}   {.𝟎}  [≡]-intro | 𝑇 | intro eq = [∧]-intro [≤]-minimum ([↔]-to-[←] IsTrue.is-𝑇 eq)
findUpperBoundedMin-correctness {f} {𝐒 max} {𝟎}   p         | 𝐹 | intro eq with findUpperBoundedMin (f ∘ 𝐒) max
findUpperBoundedMin-correctness {f} {𝐒 max} {𝟎}   ()        | 𝐹 | intro eq | None
findUpperBoundedMin-correctness {f} {𝐒 max} {𝟎}   ()        | 𝐹 | intro eq | Some _
findUpperBoundedMin-correctness {f} {𝐒 max} {𝐒 i} p         | 𝐹 | intro eq = [∧]-map (\p → [≤]-with-[𝐒] ⦃ p ⦄) id (findUpperBoundedMin-correctness {f ∘ 𝐒} {max} {i} (injective(Option.map 𝐒) ⦃ map-injectivity ⦄ p))

findUpperBoundedMin-minimal : ∀{f}{max i j} → (findUpperBoundedMin f(max) ≡ Some(i)) → IsTrue(f(j)) → (i ≤ j)
findUpperBoundedMin-minimal {i = 𝟎} {_} p q = [≤]-minimum
findUpperBoundedMin-minimal {i = 𝐒 i} {𝟎} p q = {!!}
findUpperBoundedMin-minimal {i = 𝐒 i} {𝐒 j} p q = [≤]-with-[𝐒] ⦃ findUpperBoundedMin-minimal {i = i}{j} {!!} q ⦄

-- foldRange : ()

{-
searchUntilUpperBound : (f : ℕ → Bool) → ∃(IsTrue ∘ f) → ℕ
searchUntilUpperBound f ([∃]-intro upperBound ⦃ proof ⦄) = {!fold!}

searchUntilUpperBoundProof : ∀{f}{upperBound} → (IsTrue ∘ f)(searchUntilUpperBound f upperBound)
searchUntilUpperBoundProof = {!!}

bruteforceMinExistence : ∀{ℓ} → (P : ℕ → Stmt{ℓ}) → ⦃ ComputablyDecidable(P) ⦄ → ∃(P) → ∃(Weak.Properties.MinimumOf(_≤_)(P))
∃.witness (bruteforceMinExistence P upperBound) = {!!}
∃.proof   (bruteforceMinExistence P upperBound) = {!!}
-}
-}


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

open import lib.Basics
open import lib.types.Paths

module lib.types.Unit where

pattern tt = unit

⊙Unit : Ptd₀
⊙Unit = ⊙[ Unit , unit ]

-- Unit is contractible
instance
  Unit-level : {n : ℕ₋₂} → has-level n Unit
  Unit-level {n = ⟨-2⟩} = has-level-in (unit , λ y → idp)
  Unit-level {n = S n} = raise-level n Unit-level

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Prelude

module Implicits.Resolution.Termination.Stack
  where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Data.List
open import Data.List.All
open import Data.List.Any
open Membership-≡

open import Implicits.Resolution.Termination.SizeMeasures

-- on the stack we maintain, for each rule in Δ,
-- the last goal type that resulted from using the rule
Stack : ∀ {ν} → ICtx ν → Set
Stack {ν} Δ = All (const $ Type ν) Δ

----------------------------------------------------------------
-- basic stack operations

_push_for_ : ∀ {ν r} {Δ : ICtx ν} → Stack Δ → Type ν → r ∈ Δ → Stack Δ
(a All.∷ s) push a' for here _ = a' All.∷ s
(b All.∷ s) push a for there r∈Δ = b All.∷ s push a for r∈Δ

_prepend_ : ∀ {ν r} {Δ : ICtx ν} → Stack Δ → Type ν → Stack (r ∷ Δ)
s prepend a = a All.∷ s

_get_ : ∀ {ν r} {Δ : ICtx ν} → Stack Δ → r ∈ Δ → Type ν
(a All.∷ s) get here _ = a
(a All.∷ s) get there r∈Δ = s get r∈Δ

ssum : ∀ {ν} {Δ : ICtx ν} → Stack Δ → ℕ
ssum All.[] = 0
ssum (a All.∷ s) = h|| a || + ssum s

stack-weaken : ∀ {ν} {Δ : ICtx ν} → Stack Δ → Stack (ictx-weaken Δ)
stack-weaken All.[] = All.[]
stack-weaken (px All.∷ s) = (tp-weaken px) All.∷ (stack-weaken s)

----------------------------------------------------------------
-- stack ordering

_s<_ : ∀ {ν} {Δ : ICtx ν} → (s s' : Stack Δ) → Set
s s< s' = ssum s < ssum s'

_for_⊬dom_ : ∀ {ν r} {Δ : ICtx ν} → Type ν → r ∈ Δ → Stack Δ → Set
a for r∈Δ ⊬dom s = (s push a for r∈Δ) s< s


text:
{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

open import Agda.Primitive using (Level; _⊔_; Setω; lzero; lsuc)

module Issue4032 where

infix 4 _≡_

data _≡_ {ℓ : Level} {A : Set ℓ} (a : A) : A → Set ℓ where
  refl : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

run : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
run refl x = x

nur : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → B → A
nur refl x = x

convert : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) (a : A) → nur p (run p a) ≡ a
convert refl a = refl

trevnoc : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) (b : B) → run p (nur p b) ≡ b
trevnoc refl b = refl

ap : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {a₁ a₂} → a₁ ≡ a₂ → f a₁ ≡ f a₂
ap f refl = refl

transport : ∀ {a b} {A : Set a} (B : A → Set b) {x y : A} (p : x ≡ y) → B x → B y
transport B p = run (ap B p)

apD : ∀ {a b} {A : Set a} {B : A → Set b} (f : (x : A) → B x) {a₁ a₂} → (p : a₁ ≡ a₂) → transport B p (f a₁) ≡ f a₂
apD f refl = refl

ap2 : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c} (f : (x : A) → B x → C) {a₁ a₂} (pa : a₁ ≡ a₂) {b₁ b₂} → transport B pa b₁ ≡ b₂ → f a₁ b₁ ≡ f a₂ b₂
ap2 f refl refl = refl

postulate fromIso : ∀ {ℓ} {A B : Set ℓ} (f : A → B) (g : B → A) (η : (x : A) → g (f x) ≡ x) (ε : (x : B) → f (g x) ≡ x) (τ : (x : A) → ap f (η x) ≡ ε (f x)) → A ≡ B
postulate fromIso-refl : ∀ {ℓ} {A : Set ℓ} → fromIso {ℓ} {A} {A} (λ x → x) (λ x → x) (λ x → refl) (λ x → refl) (λ x → refl) ≡ refl
{-# REWRITE fromIso-refl #-}

J : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {a : A} (P : (b : A) → a ≡ b → Set ℓ₂) {b : A} (p : a ≡ b) → P a refl → P b p
J R refl r = r

module foo {-ℓ₁-} {ℓ} {Γ : Set ℓ{-₁-}} {xs ys : Γ} (ps : xs ≡ ys) (tA : Γ → Set ℓ) (tB : (γ : Γ) → tA γ → Set ℓ) where
  module pf where
    iso-f : ((a : tA xs) → (tB xs) a) → ((a : tA ys) → (tB ys) a)
    iso-f var1 var0 = run (ap2 tB ps (trevnoc (ap tA ps) var0)) (var1 (nur (ap tA ps) var0))

    iso-g : ((a : tA ys) → (tB ys) a) → ((a : tA xs) → (tB xs) a)
    iso-g var1 var0 = nur (ap2 tB ps refl) (var1 (run (ap tA ps) var0))

    iso-η : (var0 : _) → iso-g (iso-f var0) ≡ var0
    iso-η var0 = J (λ ys (ps : xs ≡ ys) → (λ var1 → nur (ap2 tB ps refl) (run (ap2 tB ps (trevnoc (ap tA ps) (run (ap tA ps) var1))) (var0 (nur (ap tA ps) (run (ap tA ps) var1))))) ≡ var0) ps refl

    iso-ε : (var0 : _) → iso-f (iso-g var0) ≡ var0
    iso-ε = J (λ ys (ps : xs ≡ ys) → (var0 : (a : tA ys) → tB ys a) → (λ var1 → run (ap2 tB ps (trevnoc (ap tA ps) var1)) (nur (ap2 tB ps refl) (var0 (run (ap tA ps) (nur (ap tA ps) var1))))) ≡ var0) ps (λ var0 → refl)
    iso-τ : (var0 : _) → ap iso-f (iso-η var0) ≡ iso-ε (iso-f var0)
    iso-τ var0 = J
                   (λ ys (ps : xs ≡ ys) →
                      ap
                      (λ var1 var2 →
                         run (ap2 tB ps (trevnoc (ap tA ps) var2))
                         (var1 (nur (ap tA ps) var2)))
                      (J
                       (λ ys₁ ps₁ →
                          (λ var1 →
                             nur (ap2 tB ps₁ refl)
                             (run (ap2 tB ps₁ (trevnoc (ap tA ps₁) (run (ap tA ps₁) var1)))
                              (var0 (nur (ap tA ps₁) (run (ap tA ps₁) var1)))))
                          ≡ var0)
                       ps refl)
                      ≡
                      J
                      (λ ys₁ ps₁ →
                         (var1 : (a : tA ys₁) → tB ys₁ a) →
                         (λ var2 →
                            run (ap2 tB ps₁ (trevnoc (ap tA ps₁) var2))
                            (nur (ap2 tB ps₁ refl)
                             (var1 (run (ap tA ps₁) (nur (ap tA ps₁) var2)))))
                         ≡ var1)
                      ps (λ var1 → refl)
                      (λ var1 →
                         run (ap2 tB ps (trevnoc (ap tA ps) var1))
                         (var0 (nur (ap tA ps) var1))))
                   ps refl

  open pf

  pf : ((a : tA xs) → (tB xs) a) ≡ ((a : tA ys) → (tB ys) a)
  pf = fromIso iso-f iso-g iso-η iso-ε iso-τ

module bar {ℓ} {Γ : Set ℓ} {γ : Γ} {A : Γ → Set ℓ} {B : (γ : Γ) → A γ → Set ℓ} where
  g1 : ((a : A γ) → B γ a) → (a : A γ) → B γ a
  g2 : ((a : A γ) → B γ a) → (a : A γ) → B γ a

  g1 = foo.pf.iso-g {xs = γ} refl A B
  g2 = λ f x → f x

  pfg : g1 ≡ g2
  pfg = refl

  baz : foo.pf {xs = γ} refl A B ≡ refl
  baz = pf
    where
      pf : fromIso {_} {(x : A γ) → B γ x} (λ f x → f x) g2 (foo.pf.iso-η refl A B) (foo.pf.iso-ε refl A B) (foo.pf.iso-τ refl A B) ≡ refl
      pf = refl

{- WAS:
refl !=
fromIso (foo.pf.iso-f refl A B) (foo.pf.iso-g refl A B)
(foo.pf.iso-η refl A B) (foo.pf.iso-ε refl A B)
(foo.pf.iso-τ refl A B)
of type ((x : A γ) → B γ x) ≡ ((x : A γ) → B γ x)
when checking that the expression pf has type
foo.pf refl A B ≡ refl
-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Predicate transformers
------------------------------------------------------------------------

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

module Relation.Unary.PredicateTransformer where

open import Level hiding (_⊔_)
open import Function
open import Data.Product
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary using (REL)

------------------------------------------------------------------------

-- Heterogeneous and homogeneous predicate transformers

PT : ∀ {a b} → Set a → Set b → (ℓ₁ ℓ₂ : Level) → Set _
PT A B ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred B ℓ₂

Pt : ∀ {a} → Set a → (ℓ : Level) → Set _
Pt A ℓ = PT A A ℓ ℓ

-- Composition and identity

_⍮_ : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
      PT B C ℓ₂ ℓ₃ → PT A B ℓ₁ ℓ₂ → PT A C ℓ₁ _
S ⍮ T = S ∘ T

skip : ∀ {a ℓ} {A : Set a} → PT A A ℓ ℓ
skip P = P

------------------------------------------------------------------------
-- Operations on predicates extend pointwise to predicate transformers

module _ {a b} {A : Set a} {B : Set b} where

  -- The bottom and the top of the predicate transformer lattice.

  abort : PT A B zero zero
  abort = λ _ → ∅

  magic : PT A B zero zero
  magic = λ _ → U

  -- Negation.

  ∼_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
  ∼ T = ∁ ∘ T

  -- Refinement.

  infix 4 _⊑_ _⊒_ _⊑′_ _⊒′_

  _⊑_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
  S ⊑ T = ∀ {X} → S X ⊆ T X

  _⊑′_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
  S ⊑′ T = ∀ X → S X ⊆ T X

  _⊒_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
  T ⊒ S = T ⊑ S

  _⊒′_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
  T ⊒′ S = S ⊑′ T

  -- The dual of refinement.

  infix 4 _⋢_

  _⋢_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
  S ⋢ T = ∃ λ X → S X ≬ T X

  -- Union.

  infixl 6 _⊓_

  _⊓_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
  S ⊓ T = λ X → S X ∪ T X

  -- Intersection.

  infixl 7 _⊔_

  _⊔_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
  S ⊔ T = λ X → S X ∩ T X

  -- Implication.

  infixl 8 _⇛_

  _⇛_ : ∀ {ℓ₁ ℓ₂} → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
  S ⇛ T = λ X → S X ⇒ T X

  -- Infinitary union and intersection.

  infix 9 ⨆ ⨅

  ⨆ : ∀ {ℓ₁ ℓ₂ i} (I : Set i) → (I → PT A B ℓ₁ ℓ₂) → PT A B ℓ₁ _
  ⨆ I T = λ X → ⋃[ i ∶ I ] T i X

  syntax ⨆ I (λ i → T) = ⨆[ i ∶ I ] T

  ⨅ : ∀ {ℓ₁ ℓ₂ i} (I : Set i) → (I → PT A B ℓ₁ ℓ₂) → PT A B ℓ₁ _
  ⨅ I T = λ X → ⋂[ i ∶ I ] T i X

  syntax ⨅ I (λ i → T) = ⨅[ i ∶ I ] T

  -- Angelic and demonic update.

  ⟨_⟩ : ∀ {ℓ} → REL A B ℓ → PT B A ℓ _
  ⟨ R ⟩ P = λ x → R x ≬ P

  [_] : ∀ {ℓ} → REL A B ℓ → PT B A ℓ _
  [ R ] P = λ x → R x ⊆ P