text:
open import Data.Nat
module OpenTheory where

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

data Vec (A : Set) : ℕ → Set₁ where
  nil : Vec A zero
  cons : (n : ℕ) (x : A) (xs : Vec A n) → Vec A (suc n)

data Vec2 : Set → ℕ → Set₁ where
  nil : (A : Set) → Vec2 A zero
  cons : (A : Set) (n : ℕ) (x : A) (xs : Vec2 A n) → Vec2 A (suc n)

elimVec : {A : Set} (P : (n : ℕ) → Vec A n → Set)
  (pnil : P zero nil)
  (pcnons : (n : ℕ) (x : A) (xs : Vec A n) → P n xs → P (suc n) (cons n x xs))
  (n : ℕ) (xs : Vec A n) → P n xs
elimVec P pnil pcons .zero nil = pnil
elimVec P pnil pcons .(suc n) (cons n x xs) = pcons n x xs (elimVec P pnil pcons n xs)

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

data Tree (A B : Set) : ℕ → ℕ → Set where
  leaf₁ : A → Tree A B (suc zero) zero
  leaf₂ : B → Tree A B zero (suc zero)
  branch : (m n x y : ℕ)
    → Tree A B m n → Tree A B x y
    → Tree A B (m + x) (n + y)

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

max_stars_repo_name: larrytheliquid/generic-elim

max_issues_repo_name: larrytheliquid/generic-elim

max_forks_repo_name: larrytheliquid/generic-elim


text:
module PiQ.Everything where
open import PiQ.Syntax     -- Syntax of PiQ
open import PiQ.Opsem      -- Abstract machine semantics of PiQ
open import PiQ.AuxLemmas  -- Some auxiliary lemmas about opsem for forward/backward deterministic proof
open import PiQ.NoRepeat   -- Forward/backward deterministic lemmas and Non-repeating lemma
open import PiQ.Invariants -- Some invariants about abstract machine semantics
open import PiQ.Eval       -- Evaluator for PiQ
open import PiQ.Interp     -- Big-step intepreter
open import PiQ.Properties -- Properties of PiQ
open import PiQ.Examples   -- Examples
open import PiQ.SAT        -- SAT solver

ext: agda


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

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Sets.EquivalenceRelations

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

module Rings.IntegralDomains.Definition {m n : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Setoid S
open Equivalence eq
open Ring R

record IntegralDomain : Set (lsuc m ⊔ n) where
  field
    intDom : {a b : A} → (a * b) ∼ (Ring.0R R) → ((a ∼ (Ring.0R R)) → False) → b ∼ (Ring.0R R)
    nontrivial : Setoid._∼_ S (Ring.1R R) (Ring.0R R) → False

decidedIntDom : ({a b : A} → (a * b) ∼ (Ring.0R R) → (a ∼ 0R) || (b ∼ 0R)) → ({a b : A} → (a * b) ∼ 0R → ((a ∼ (Ring.0R R)) → False) → b ∼ (Ring.0R R))
decidedIntDom f ab=0 a!=0 with f ab=0
decidedIntDom f ab=0 a!=0 | inl x = exFalso (a!=0 x)
decidedIntDom f ab=0 a!=0 | inr x = x


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

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
open import homotopy.WedgeExtension

module homotopy.Pi2HSusp where

module Pi2HSusp {i} (A : Type i) (gA : has-level 1 A)
  (cA : is-connected 0 A) (A-H : HSS A)
  where

  {- TODO this belongs somewhere else, but where? -}
  private
    Type=-ext : ∀ {i} {A B : Type i} (p q : A == B)
      → ((x : A) → coe p x == coe q x) → p == q
    Type=-ext p q α =
      ! (ua-η p)
      ∙ ap ua (pair= (λ= α) (prop-has-all-paths-↓ (is-equiv-is-prop (coe q))))
      ∙ ua-η q

  open HSS A-H
  open ConnectedHSpace A cA A-H

  P : Suspension A → Type i
  P x = Trunc 1 (north == x)

  module Codes = SuspensionRec A A (λ a → ua (μ-e-r-equiv a))

  Codes : Suspension A → Type i
  Codes = Codes.f

  Codes-level : (x : Suspension A) → has-level 1 (Codes x)
  Codes-level = Suspension-elim gA gA
    (λ _ → prop-has-all-paths-↓ has-level-is-prop)

  encode₀ : {x : Suspension A} → (north == x) → Codes x
  encode₀ α = transport Codes α e

  encode : {x : Suspension A} → P x → Codes x
  encode {x} = Trunc-rec (Codes-level x) encode₀

  decode' : A → P north
  decode' a = [ (merid a ∙ ! (merid e)) ]

  abstract
    transport-Codes-mer : (a a' : A)
      → transport Codes (merid a) a' == μ a a'
    transport-Codes-mer a a' =
      coe (ap Codes (merid a)) a'
        =⟨ Codes.merid-β a |in-ctx (λ w → coe w a') ⟩
      coe (ua (μ-e-r-equiv a)) a'
        =⟨ coe-β (μ-e-r-equiv a) a' ⟩
      μ a a' ∎

    transport-Codes-mer-e-! : (a : A)
      → transport Codes (! (merid e)) a == a
    transport-Codes-mer-e-! a =
      coe (ap Codes (! (merid e))) a
        =⟨ ap-! Codes (merid e) |in-ctx (λ w → coe w a) ⟩
      coe (! (ap Codes (merid e))) a
        =⟨ Codes.merid-β e |in-ctx (λ w → coe (! w) a) ⟩
      coe (! (ua (μ-e-r-equiv e))) a
        =⟨ Type=-ext (ua (μ-e-r-equiv e)) idp (λ x → coe-β _ x ∙ μ-e-l x)
          |in-ctx (λ w → coe (! w) a) ⟩
      coe (! idp) a ∎

  abstract
    encode-decode' : (a : A) → encode (decode' a) == a
    encode-decode' a =
      transport Codes (merid a ∙ ! (merid e)) e
        =⟨ trans-∙ {B = Codes} (merid a) (! (merid e)) e ⟩
      transport Codes (! (merid e)) (transport Codes (merid a) e)
        =⟨ transport-Codes-mer a e ∙ μ-e-r a
          |in-ctx (λ w → transport Codes (! (merid e)) w) ⟩
      transport Codes (! (merid e)) a
        =⟨ transport-Codes-mer-e-! a ⟩
      a ∎

  abstract
    homomorphism : (a a' : A)
      → Path {A = Trunc 1 (north == south)}
        [ merid (μ a a' ) ] [ merid a' ∙ ! (merid e) ∙ merid a ]
    homomorphism = WedgeExt.ext args
      where
      args : WedgeExt.args {a₀ = e} {b₀ = e}
      args = record {m = -2; n = -2; cA = cA; cB = cA;
        P = λ a a' → (_ , Trunc-level {n = 1} _ _);
        f = λ a →  ap [_] $
              merid (μ a e)
                =⟨ ap merid (μ-e-r a) ⟩
              merid a
                =⟨ ap (λ w → w ∙ merid a) (! (!-inv-r (merid e)))
                   ∙ ∙-assoc (merid e) (! (merid e)) (merid a)  ⟩
              merid e ∙ ! (merid e) ∙ merid a ∎;
        g = λ a' → ap [_] $
              merid (μ e a')
                =⟨ ap merid (μ-e-l a') ⟩
              merid a'
                =⟨ ! (∙-unit-r (merid a'))
                   ∙ ap (λ w → merid a' ∙ w) (! (!-inv-l (merid e))) ⟩
              merid a' ∙ ! (merid e) ∙ merid e ∎ ;
        p = ap (λ {(p₁ , p₂) → ap [_] $
              merid (μ e e) =⟨ p₁ ⟩
              merid e       =⟨ p₂ ⟩
              merid e ∙ ! (merid e) ∙ merid e ∎})
             (pair×= (ap (λ x → ap merid x) (! μ-coh)) (coh (merid e)))}
        where coh : {B : Type i} {b b' : B} (p : b == b')
                → ap (λ w → w ∙ p) (! (!-inv-r p)) ∙ ∙-assoc p (! p) p
                  == ! (∙-unit-r p) ∙ ap (λ w → p ∙ w) (! (!-inv-l p))
              coh idp = idp

  decode : {x : Suspension A} → Codes x → P x
  decode {x} = Suspension-elim {P = λ x → Codes x → P x}
                 decode'
                 (λ a → [ merid a ])
                 (λ a → ↓-→-from-transp (λ= $ STS a))
                 x
    where
    abstract
      STS : (a a' : A) → transport P (merid a) (decode' a')
                         == [ merid (transport Codes (merid a) a') ]
      STS a a' =
        transport P (merid a) [ merid a' ∙ ! (merid e) ]
          =⟨ transport-Trunc (north ==_) (merid a) _ ⟩
        [ transport (north ==_) (merid a) (merid a' ∙ ! (merid e)) ]
          =⟨ ap [_] (trans-pathfrom {A = Suspension A} (merid a) _) ⟩
        [ (merid a' ∙ ! (merid e)) ∙ merid a ]
          =⟨ ap [_] (∙-assoc (merid a') (! (merid e)) (merid a)) ⟩
        [ merid a' ∙ ! (merid e) ∙ merid a ]
          =⟨ ! (homomorphism a a') ⟩
        [ merid (μ a a') ]
          =⟨ ap ([_] ∘ merid) (! (transport-Codes-mer a a')) ⟩
        [ merid (transport Codes (merid a) a') ] ∎

  abstract
    decode-encode : {x : Suspension A} (tα : P x)
      → decode {x} (encode {x} tα) == tα
    decode-encode {x} = Trunc-elim
      {P = λ tα → decode {x} (encode {x} tα) == tα}
      (λ _ → =-preserves-level 1 Trunc-level)
      (J (λ y p → decode {y} (encode {y} [ p ]) == [ p ])
         (ap [_] (!-inv-r (merid e))))

  main-lemma-eq : Trunc 1 (north' A == north) ≃ A
  main-lemma-eq = equiv encode decode' encode-decode' decode-encode

  ⊙main-lemma : ⊙Trunc 1 (⊙Ω (⊙Susp (A , e))) == (A , e)
  ⊙main-lemma = ⊙ua (⊙≃-in main-lemma-eq idp)

  abstract
    main-lemma-iso : Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp (A , e)))) Trunc-level
                  ≃ᴳ Ω^S-group 0 (⊙Trunc 1 (A , e)) Trunc-level
    main-lemma-iso = (record {f = f; pres-comp = pres-comp} , ie)
      where
      h : fst (⊙Trunc 1 (⊙Ω (⊙Susp (A , e)))
            ⊙→ ⊙Trunc 1 (A , e))
      h = (λ x → [ encode x ]) , idp

      f : Ω (⊙Trunc 1 (⊙Ω (⊙Susp (A , e)))) → Ω (⊙Trunc 1 (A , e))
      f = fst (ap^ 1 h)

      pres-comp : (p q : Ω^ 1 (⊙Trunc 1 (⊙Ω (⊙Susp (A , e)))))
        → f (conc^S 0 p q) == conc^S 0 (f p) (f q)
      pres-comp = ap^S-conc^S 0 h

      ie : is-equiv f
      ie = is-equiv-ap^ 1 h (snd $ ((unTrunc-equiv A gA)⁻¹ ∘e main-lemma-eq))

  abstract
    π₂-Suspension : πS 1 (⊙Susp (A , e)) == πS 0 (A , e)
    π₂-Suspension =
      πS 1 (⊙Susp (A , e))
        =⟨ πS-inner-iso 0 (⊙Susp (A , e)) ⟩
      πS 0 (⊙Ω (⊙Susp (A , e)))
        =⟨ ! (πS-Trunc-shift-iso 0 (⊙Ω (⊙Susp (A , e)))) ⟩
      Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp (A , e)))) Trunc-level
        =⟨ group-ua main-lemma-iso ⟩
      Ω^S-group 0 (⊙Trunc 1 (A , e)) Trunc-level
        =⟨ πS-Trunc-shift-iso 0 (A , e) ⟩
      πS 0 (A , e) ∎

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import Prelude
open import RW.Language.RTerm
open import RW.Language.FinTerm

module RW.Language.RTermIdx where

  open Eq {{...}}

  data RTermᵢ {a}(A : Set a) : Set a where
    ovarᵢ : (x : A) → RTermᵢ A
    ivarᵢ : (n : ℕ) → RTermᵢ A
    rlitᵢ : (l : Literal) → RTermᵢ A
    rlamᵢ : RTermᵢ A
    rappᵢ : (n : RTermName) → RTermᵢ A

  ovarᵢ-inj : ∀{a}{A : Set a}{x y : A} → ovarᵢ x ≡ ovarᵢ y → x ≡ y
  ovarᵢ-inj refl = refl

  ivarᵢ-inj : ∀{a}{A : Set a}{x y : ℕ} → ivarᵢ {a} {A} x ≡ ivarᵢ {a} y → x ≡ y
  ivarᵢ-inj refl = refl

  rlitᵢ-inj : ∀{a}{A : Set a}{x y : Literal} → rlitᵢ {a} {A} x ≡ rlitᵢ {a} y → x ≡ y
  rlitᵢ-inj refl = refl

  rappᵢ-inj : ∀{a}{A : Set a}{x y : RTermName} → rappᵢ {a} {A} x ≡ rappᵢ {a} y → x ≡ y
  rappᵢ-inj refl = refl

  _≟-RTermᵢ_ : {A : Set}{{eqA : Eq A}}
               → (t₁ t₂ : RTermᵢ A) → Dec (t₁ ≡ t₂)
  _≟-RTermᵢ_ {{eq _≟_}} (ovarᵢ x) (ovarᵢ y)
    with x ≟ y
  ...| yes x≡y = yes (cong ovarᵢ x≡y)
  ...| no  x≢y = no (x≢y ∘ ovarᵢ-inj)
  _≟-RTermᵢ_ (ovarᵢ _) (ivarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (ovarᵢ _) (rlitᵢ _) = no (λ ())
  _≟-RTermᵢ_ (ovarᵢ _) (rlamᵢ  ) = no (λ ())
  _≟-RTermᵢ_ (ovarᵢ _) (rappᵢ _) = no (λ ())
  _≟-RTermᵢ_ (ivarᵢ _) (ovarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (ivarᵢ x) (ivarᵢ y)
    with x ≟-ℕ y
  ...| yes x≡y = yes (cong ivarᵢ x≡y)
  ...| no  x≢y = no (x≢y ∘ ivarᵢ-inj)
  _≟-RTermᵢ_ (ivarᵢ _) (rlitᵢ _) = no (λ ())
  _≟-RTermᵢ_ (ivarᵢ _) (rlamᵢ  ) = no (λ ())
  _≟-RTermᵢ_ (ivarᵢ _) (rappᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rlitᵢ _) (ivarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rlitᵢ _) (ovarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rlitᵢ x) (rlitᵢ y)
    with x ≟-Lit y
  ...| yes x≡y = yes (cong rlitᵢ x≡y)
  ...| no  x≢y = no (x≢y ∘ rlitᵢ-inj)
  _≟-RTermᵢ_ (rlitᵢ _) (rlamᵢ  ) = no (λ ())
  _≟-RTermᵢ_ (rlitᵢ _) (rappᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rlamᵢ  ) (ovarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rlamᵢ  ) (ivarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rlamᵢ  ) (rlitᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rlamᵢ  ) (rlamᵢ  ) = yes refl
  _≟-RTermᵢ_ (rlamᵢ  ) (rappᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rappᵢ _) (ovarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rappᵢ _) (ivarᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rappᵢ _) (rlitᵢ _) = no (λ ())
  _≟-RTermᵢ_ (rappᵢ _) (rlamᵢ  ) = no (λ ())
  _≟-RTermᵢ_ (rappᵢ x) (rappᵢ y)
    with x ≟-RTermName y
  ...| yes x≡y = yes (cong rappᵢ x≡y)
  ...| no  x≢y = no (x≢y ∘ rappᵢ-inj)

  -----------------------------------
  -- Utilities

  out : ∀{a}{A : Set a} → RTerm A → RTermᵢ A × List (RTerm A)
  out (ovar x)    = ovarᵢ x , []
  out (ivar n)    = ivarᵢ n , []
  out (rlit l)    = rlitᵢ l , []
  out (rlam t)    = rlamᵢ , t ∷ []
  out (rapp n ts) = rappᵢ n , ts

  toSymbol : ∀{a}{A : Set a} → RTermᵢ A → Maybe A
  toSymbol (ovarᵢ a) = just a
  toSymbol _         = nothing

  idx-cast : ∀{a b}{A : Set a}{B : Set b}
           → (i : RTermᵢ A) → (toSymbol i ≡ nothing)
           → RTermᵢ B
  idx-cast (ovarᵢ x) ()
  idx-cast (ivarᵢ n) _ = ivarᵢ n
  idx-cast (rlitᵢ l) _ = rlitᵢ l
  idx-cast (rlamᵢ  ) _ = rlamᵢ
  idx-cast (rappᵢ n) _ = rappᵢ n

  instance
    eq-RTermᵢ : {A : Set}{{eqA : Eq A}} → Eq (RTermᵢ A)
    eq-RTermᵢ = eq _≟-RTermᵢ_

  {-
  instance

    RTerm-isTrie : {A : Set}{{eqA : Eq A}}{{enA : Enum A}}
                 → IsTrie (RTerm A)
    RTerm-isTrie {A} {{enA = enum aℕ ℕa}} = record
      { Idx     = RTermᵢ A
      ; idx≡    = eq _≟-RTermᵢ_
      ; toSym   = toSymAux
      ; fromSym = fromSymAux
      ; inₜ     = inAux
      ; outₜ    = outAux
      }
      where
        postulate
          fixme : ∀{a}{A : Set a} → A

        toSymAux : RTermᵢ A → Maybe ℕ
        toSymAux (ovarᵢ n) = aℕ n
        toSymAux _         = nothing

        fromSymAux : ℕ → Maybe (RTermᵢ A)
        fromSymAux n = maybe (λ x → just (ovarᵢ x)) nothing (ℕa n)

        inAux : RTermᵢ A × List (RTerm A) → RTerm A
        inAux (ovarᵢ x , []) = ovar x
        inAux (ivarᵢ x , []) = ivar x
        inAux (rlitᵢ l , []) = rlit l
        inAux (rlamᵢ , t ∷ []) = rlam t
        inAux (rappᵢ n , ts) = rapp n ts
        inAux _ = fixme -- maybe using vectors of the correct arity...

        outAux : RTerm A → RTermᵢ A × List (RTerm A)
        outAux (ovar x) = ovarᵢ x , []
        outAux (ivar n) = ivarᵢ n , []
        outAux (rlit l) = rlitᵢ l , []
        outAux (rlam t) = rlamᵢ , t ∷ []
        outAux (rapp n ts) = rappᵢ n , ts
  {-
    RTerm-isTrie : IsTrie (RTerm ⊥)
    RTerm-isTrie = record
      { Idx   = RTermᵢ ⊥
      ; idx≡  = eq _≟-RTermᵢ_
      ; toSym = toSymAux
      ; fromSym = fromSymAux
      ; inₜ   = inAux
      ; outₜ  = outAux
      } where
        postulate
          fixme : ∀{a}{A : Set a} → A

        toSymAux : RTermᵢ ⊥ → Maybe ℕ
        toSymAux (ovarᵢ ())
        toSymAux (ivarᵢ n) = just n
        toSymAux _         = nothing

        fromSymAux : ℕ → Maybe (RTermᵢ ⊥)
        fromSymAux x = just (ivarᵢ x)

        inAux : RTermᵢ ⊥ × List (RTerm ⊥) → RTerm ⊥
        inAux (ovarᵢ () , [])
        inAux (ivarᵢ x , []) = ivar x
        inAux (rlitᵢ l , []) = rlit l
        inAux (rlamᵢ , t ∷ []) = rlam t
        inAux (rappᵢ n , ts) = rapp n ts
        inAux _ = fixme -- maybe using vectors of the correct arity...

        outAux : RTerm ⊥ → RTermᵢ ⊥ × List (RTerm ⊥)
        outAux (ovar ()) -- = ovarᵢ x , []
        outAux (ivar n) = ivarᵢ n , []
        outAux (rlit l) = rlitᵢ l , []
        outAux (rlam t) = rlamᵢ , t ∷ []
        outAux (rapp n ts) = rappᵢ n , ts
  -}

  RTermTrie : (A : Set){{eqA : Eq A}}{{enA : Enum A}} → Set
  RTermTrie A = BTrie (RTerm A) Name

  insertTerm : {A : Set}{{eqA : Eq A}}{{enA : Enum A}}
             → Name → RTerm A → ℕ × RTermTrie A → ℕ × RTermTrie A
  insertTerm {A} = insert
    where
      open import RW.Data.BTrie.Insert (RTerm A) Name

  lookupTerm : {A : Set}{{eqA : Eq A}}{{enA : Enum A}}
             → RTerm ⊥ → RTermTrie A → List (ℕmap.to (RTerm A) × Name)
  lookupTerm {A} t = lookup (replace-A ⊥-elim t)
    where
      open import RW.Data.BTrie.Lookup (RTerm A) Name

  -}

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
module Syntax2 where

import Level
open import Data.Empty
open import Data.Unit as Unit renaming (tt to ∗)
open import Data.Nat
open import Data.List as List renaming ([] to Ø) hiding ([_])
open import NonEmptyList as NList
open import Data.Vec as Vec hiding ([_]; _++_)
open import Data.Product as Prod
open import Categories.Category using (Category)
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Relation.Binary using (module IsEquivalence; Setoid; module Setoid)
open ≡-Reasoning

open import Common.Context as Context

Univ = ⊤

length' : {A : Set} → List A → ℕ
length' Ø = 0
length' (x ∷ xs) = suc (length' xs)

data FP : Set where
  μ : FP
  ν : FP

RawCtx : Set
RawCtx = Ctx ⊤

RawVar : RawCtx → Set
RawVar Γ = Var Γ ∗

TyCtx : Set
TyCtx = Ctx RawCtx

TyVar : TyCtx → RawCtx → Set
TyVar = Var

CtxMor : (TyCtx → RawCtx → RawCtx → Set) → RawCtx → RawCtx → Set
CtxMor R Γ₁ Γ₂ = Vec (R Ø Γ₁ Ø) (length' Γ₂)

FpData : (TyCtx → RawCtx → RawCtx → Set) → TyCtx → RawCtx → Set
FpData R Θ Γ = NList (Σ RawCtx (λ Γ' → CtxMor R Γ' Γ × R (Γ ∷ Θ) Γ' Ø))

FpMapData : (TyCtx → RawCtx → RawCtx → Set) → Set
FpMapData R = NList (Σ RawCtx λ Γ' → R Ø (∗ ∷ Γ') Ø)

-- | Types and objects with their corresponding (untyped) type, object
-- variable contexts and parameter contexts.
data Raw : TyCtx → RawCtx → RawCtx → Set where
  ----- Common constructors
  instRaw : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} →
            Raw Θ Γ₁ (∗ ∷ Γ₂) → Raw Ø Γ₁ Ø → Raw Θ Γ₁ Γ₂

  ----- Object constructors
  unitRaw : (Γ : RawCtx) → Raw Ø Γ Ø
  objVarRaw : (Γ : RawCtx) → RawVar Γ → Raw Ø Γ Ø
  dialgRaw : {Γ Γ' : RawCtx} (Δ : RawCtx) →
             CtxMor Raw Γ' Γ → Raw (Γ ∷ Ø) Γ' Ø → FP → Raw Ø Δ (∗ ∷ Γ')
  mappingRaw : (Γ Δ : RawCtx) →
               FpMapData Raw → FP → Raw Ø Δ Γ

  ----- Type constructors
  ⊤-Raw : (Θ : TyCtx) (Γ : RawCtx) → Raw Θ Γ Ø
  tyVarRaw : {Θ : TyCtx} (Γ₁ : RawCtx) {Γ₂ : RawCtx} → TyVar Θ Γ₂ → Raw Θ Γ₁ Γ₂
  paramAbstrRaw : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) →
                  Raw Θ (∗ ∷ Γ₁) Γ₂ → Raw Θ Γ₁ (Γ₂ ++ ∗ ∷ Ø)
  -- | Constructor for fixed points. The first component is intended to be
  -- the context morphism, the second is the type.
  fpRaw : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) →
          FP → FpData Raw Θ Γ₂ → Raw Θ Γ₁ Γ₂

weaken : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} → Raw Θ Γ₁ Γ₂ → Raw Θ (∗ ∷ Γ₁) Γ₂
weaken (instRaw t s)        = instRaw (weaken t) (weaken s)
weaken (unitRaw Γ)          = unitRaw (∗ ∷ Γ)
weaken (objVarRaw Γ x)      = objVarRaw (∗ ∷ Γ) (succ ∗ x)
weaken (dialgRaw Δ f t ρ)   = dialgRaw (∗ ∷ Δ) f t ρ
weaken (mappingRaw Γ Δ gs ρ)  = mappingRaw Γ (∗ ∷ Δ) gs ρ
weaken (⊤-Raw Θ Γ)          = ⊤-Raw Θ (∗ ∷ Γ)
weaken (tyVarRaw Γ₁ X)      = tyVarRaw (∗ ∷ Γ₁) X
weaken (paramAbstrRaw Γ₁ A) = paramAbstrRaw (∗ ∷ Γ₁) (weaken A)
weaken (fpRaw Γ₁ ρ D)       = fpRaw (∗ ∷ Γ₁) ρ D

ctxid : (Γ : RawCtx) → CtxMor Raw Γ Γ
ctxid Ø = []
ctxid (x ∷ Γ) = (objVarRaw (∗ ∷ Γ) zero) ∷ (Vec.map weaken (ctxid Γ))

-- | Build the instantiation "t f" of a raw term t by a context morphism f
instWCtxMor : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} →
              Raw Θ Γ₁ Γ₂ → CtxMor Raw Γ₁ Γ₂ → Raw Θ Γ₁ Ø
instWCtxMor {Γ₂ = Ø}      t []      = t
instWCtxMor {Γ₂ = x ∷ Γ₂} t (s ∷ f) = instWCtxMor (instRaw t s) f

-- | Retrieve the term to be substituted for a variable from a context morphism
get : {R : TyCtx → RawCtx → RawCtx → Set} {Γ₁ Γ₂ : RawCtx} →
      CtxMor R Γ₂ Γ₁ → RawVar Γ₁ → R Ø Γ₂ Ø
get {R} {Ø}       []     ()
get {R} {_ ∷ Γ₁} (M ∷ f) zero        = M
get {R} {_ ∷ Γ₁} (M ∷ f) (succ .∗ x) = get {R} f x

-- | Extends a context morphism to be the identity on a new variable
extend : {Γ₁ Γ₂ : RawCtx} → CtxMor Raw Γ₂ Γ₁ → CtxMor Raw (∗ ∷ Γ₂) (∗ ∷ Γ₁)
extend f = (objVarRaw _ zero) ∷ (Vec.map weaken f)

-- | Substitution on raw terms
substRaw : ∀ {Θ Γ₁ Γ Γ₂} → Raw Θ Γ₁ Γ → CtxMor Raw Γ₂ Γ₁ → Raw Θ Γ₂ Γ
substRaw (instRaw M N)        f = instRaw (substRaw M f) (substRaw N f)
substRaw (unitRaw Γ)          f = unitRaw _
substRaw (objVarRaw Γ₁ x)     f = get {Raw} f x
substRaw (dialgRaw Δ g A ρ)   f = dialgRaw _ g A ρ
substRaw (mappingRaw Γ Δ gs ρ)  f = mappingRaw _ _ gs ρ
substRaw (⊤-Raw Θ Γ)          f = ⊤-Raw Θ _
substRaw (tyVarRaw Γ₁ X)      f = tyVarRaw _ X
substRaw (paramAbstrRaw Γ₁ A) f = paramAbstrRaw _ (substRaw A (extend f))
substRaw (fpRaw Γ₁ ρ D)       f = fpRaw _ ρ D

substTyRaw₀ : ∀ {Θ Γ₁ Γ Γ₂} →
              Raw (Γ ∷ Θ) Γ₁ Γ₂ → Raw Ø Ø Γ → Raw Θ Γ₁ Γ₂
substTyRaw₀ (instRaw A t) B = instRaw (substTyRaw₀ A B) t
substTyRaw₀ (⊤-Raw ._ Γ₁) B = ⊤-Raw _ _
substTyRaw₀ (tyVarRaw Γ₁ zero) B = {!!}
substTyRaw₀ (tyVarRaw Γ₁ (succ Γ₂ X)) B = {!!}
substTyRaw₀ (paramAbstrRaw Γ₁ A) B = {!!}
substTyRaw₀ (fpRaw Γ₁ x x₁) B = {!!}

-- | Substitute into for type variables
substTyRaw : ∀ {Θ₁ Θ₂ Γ₁ Γ Γ₂} →
             Raw (Θ₁ ++ (Γ ∷ Θ₂)) Γ₁ Γ₂ → Raw Ø Ø Γ → Raw (Θ₁ ++ Θ₂) Γ₁ Γ₂
substTyRaw {Ø} A B = {!!}
substTyRaw {x ∷ Θ₁} A B = {!!}

-- | Context morphism that projects on arbitrary prefix of a context
ctxProjRaw : (Γ₁ Γ₂ : RawCtx) → CtxMor Raw (Γ₂ ++ Γ₁) Γ₁
ctxProjRaw Γ₁ Ø = ctxid Γ₁
ctxProjRaw Γ₁ (x ∷ Γ₂) = Vec.map weaken (ctxProjRaw Γ₁ Γ₂)

-- | Extend one step weakening to weakening by arbitrary contexts
weaken' : ∀ {Θ Γ₁ Γ₃} →
          (Γ₂ : RawCtx) → Raw Θ Γ₁ Γ₃ → Raw Θ (Γ₂ ++ Γ₁) Γ₃
weaken' {Γ₁ = Γ₁} Γ₂ t = substRaw t (ctxProjRaw Γ₁ Γ₂)

-----------------------------------------
--- Examples
-----------------------------------------

_︵_ : {A : Set} → A → A → List A
a ︵ b = a ∷ b ∷ Ø

-- | Binary product type
Prod : (Γ : RawCtx) → Raw (Γ ︵ Γ) Ø Γ
Prod Γ = fpRaw {Δ} {Γ} Ø ν D
  where
    Δ = Γ ︵ Γ

    A : TyVar (Γ ∷ Δ) Γ
    A = succ Γ zero

    B : TyVar (Γ ∷ Δ) Γ
    B = succ Γ (succ Γ zero)

    D₁ = (Γ , ctxid Γ , instWCtxMor (tyVarRaw Γ A) (ctxid Γ))

    D₂ = (Γ , ctxid Γ , instWCtxMor (tyVarRaw Γ B) (ctxid Γ))

    D : FpData Raw Δ Γ
    D = D₁ ∷ [ D₂ ]

-----------------------------------------
--- Separate types and terms
-----------------------------------------

mutual
  data DecentType : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} → Raw Θ Γ₁ Γ₂ → Set where
    DT-⊤ : (Θ : TyCtx) (Γ : RawCtx) → DecentType (⊤-Raw Θ Γ)
    DT-tyVar : {Θ : TyCtx} (Γ₁ : RawCtx) {Γ₂ : RawCtx} →
               (X : TyVar Θ Γ₂) → DecentType (tyVarRaw Γ₁ X)
    DT-inst : ∀{Θ Γ₁ Γ₂} →
              (A : Raw Θ Γ₁ (∗ ∷ Γ₂)) → (t : Raw Ø Γ₁ Ø) →
              DecentType A → DecentTerm t →
              DecentType (instRaw A t)
    DT-paramAbstr : ∀{Θ Γ₂} (Γ₁ : RawCtx) →
                    (A : Raw Θ (∗ ∷ Γ₁) Γ₂) →
                    DecentType A →
                    DecentType (paramAbstrRaw Γ₁ A)
    DT-fp : ∀{Θ Γ₂} (Γ₁ : RawCtx) →
            (ρ : FP) → (D : FpData Raw Θ Γ₂) →
            DecentFpData D →
            DecentType (fpRaw Γ₁ ρ D)

  data DecentTerm : {Γ₁ Γ₂ : RawCtx} → Raw Ø Γ₁ Γ₂ → Set where
    DO-unit : (Γ : RawCtx) → DecentTerm (unitRaw Γ)
    DO-objVar : (Γ : RawCtx) → (x : RawVar Γ) → DecentTerm (objVarRaw Γ x)
    DO-inst : {Γ₁ Γ₂ : RawCtx} →
              (t : Raw Ø Γ₁ (∗ ∷ Γ₂)) → (s : Raw Ø Γ₁ Ø) →
              DecentTerm t → DecentTerm s →
              DecentTerm (instRaw t s)
    DO-dialg : {Γ Γ' : RawCtx} (Δ : RawCtx) →
               (f : CtxMor Raw Γ' Γ) → (A : Raw (Γ ∷ Ø) Γ' Ø) → (ρ : FP) →
               DecentCtxMor f → DecentType A →
               DecentTerm (dialgRaw Δ f A ρ)
    DO-mapping : {Γ : RawCtx} (Δ : RawCtx) →
                 (gs : FpMapData Raw) → (ρ : FP) →
                 DecentTermList gs →
                 DecentTerm (mappingRaw Γ Δ gs ρ)

  DecentTermList : FpMapData Raw → Set
  DecentTermList [ (Γ' , t) ] = DecentTerm t
  DecentTermList ((Γ' , t) ∷ ts) = DecentTerm t × DecentTermList ts

  DecentCtxMor : {Γ₁ Γ₂ : RawCtx} → CtxMor Raw Γ₁ Γ₂ → Set
  DecentCtxMor {Γ₂ = Ø}      []      = ⊤
  DecentCtxMor {Γ₂ = x ∷ Γ₂} (t ∷ f) = DecentTerm t × DecentCtxMor f

  DecentFpData : ∀{Θ Γ₂} → FpData Raw Θ Γ₂ → Set
  DecentFpData [ Γ , f , A ] = DecentCtxMor f × DecentType A
  DecentFpData ((Γ , f , A) ∷ D)
    = (DecentCtxMor f × DecentType A) × DecentFpData D

weakenDO : {Γ₁ Γ₂ : RawCtx} {t : Raw Ø Γ₁ Γ₂} →
           DecentTerm t → DecentTerm (weaken t)

weakenDT : ∀ {Θ Γ₁ Γ₂} {A : Raw Θ Γ₁ Γ₂} →
           DecentType A → DecentType (weaken A)
weakenDT (DT-⊤ Θ Γ)             = DT-⊤ Θ _
weakenDT (DT-tyVar Γ₁ X)        = DT-tyVar _ X
weakenDT (DT-inst A t p q)      = DT-inst _ _ (weakenDT p) (weakenDO q)
weakenDT (DT-paramAbstr Γ₁ A p) = DT-paramAbstr _ _ (weakenDT p)
weakenDT (DT-fp Γ₁ ρ D p)       = DT-fp _ ρ D p

weakenDO (DO-unit Γ)            = DO-unit _
weakenDO (DO-objVar Γ x)        = DO-objVar _ (succ ∗ x)
weakenDO (DO-inst t s p q)      = DO-inst _ _ (weakenDO p) (weakenDO q)
weakenDO (DO-dialg Δ f A ρ p q) = DO-dialg _ f _ ρ p q
weakenDO (DO-mapping Δ gs ρ p)  = DO-mapping _ gs ρ p

weakenDecentCtxMor : {Γ₁ Γ₂ : RawCtx} {f : CtxMor Raw Γ₁ Γ₂} →
                     DecentCtxMor f → DecentCtxMor (Vec.map weaken f)
weakenDecentCtxMor {Γ₂ = Ø}      {f}     p        = ∗
weakenDecentCtxMor {Γ₂ = x ∷ Γ₂} {t ∷ f} (p , ps) =
  (weakenDO p , weakenDecentCtxMor ps)

-------------------------------------
------- Pre-types and terms
-------------------------------------

PreType : (Θ : TyCtx) (Γ₁ Γ₂ : RawCtx) → Set
PreType Θ Γ₁ Γ₂ = Σ (Raw Θ Γ₁ Γ₂) λ A → DecentType A

mkPreType : ∀ {Θ Γ₁ Γ₂} {A : Raw Θ Γ₁ Γ₂} → DecentType A → PreType Θ Γ₁ Γ₂
mkPreType {A = A} p = (A , p)

PreTerm : (Γ₁ Γ₂ : RawCtx) → Set
PreTerm Γ₁ Γ₂ = Σ (Raw Ø Γ₁ Γ₂) λ t → DecentTerm t

mkPreTerm : ∀ {Γ₁ Γ₂} {t : Raw Ø Γ₁ Γ₂} → DecentTerm t → PreTerm Γ₁ Γ₂
mkPreTerm {t = t} p = (t , p)

CtxMorP = CtxMor (λ _ → PreTerm)
FpMapDataP = FpMapData (λ _ → PreTerm)

mkCtxMorP : {Γ₁ Γ₂ : RawCtx} {f : CtxMor Raw Γ₁ Γ₂} →
             DecentCtxMor f → CtxMorP Γ₁ Γ₂
mkCtxMorP {Γ₂ = Ø}              p        = []
mkCtxMorP {Γ₂ = x ∷ Γ₂} {t ∷ f} (p , ps) = (t , p) ∷ (mkCtxMorP ps)

projCtxMor₁ : {Γ₁ Γ₂ : RawCtx} → CtxMorP Γ₂ Γ₁ → CtxMor Raw Γ₂ Γ₁
projCtxMor₁ = Vec.map proj₁

projCtxMor₂ : {Γ₁ Γ₂ : RawCtx} →
              (f : CtxMorP Γ₂ Γ₁) →  DecentCtxMor (projCtxMor₁ f)
projCtxMor₂ {Ø} [] = ∗
projCtxMor₂ {x ∷ Γ₁} ((t , p) ∷ f) = (p , projCtxMor₂ f)

projPTList₁ : FpMapDataP → FpMapData Raw
projPTList₁ = NList.map (Prod.map id proj₁)

projPTList₂ : (gs : FpMapDataP) → DecentTermList (projPTList₁ gs)
projPTList₂ [ (Γ' , t , p) ] = p
projPTList₂ ((Γ' , t , p) ∷ gs) = (p , projPTList₂ gs)

-----------------------------------------
----- Constructors for pre terms
-----------------------------------------

unitPT : (Γ : RawCtx) → PreTerm Γ Ø
unitPT Γ = mkPreTerm (DO-unit _)

varPT : (Γ : RawCtx) → RawVar Γ → PreTerm Γ Ø
varPT Γ x = mkPreTerm (DO-objVar _ x)

instPT : {Γ₁ : RawCtx} {Γ₂ : RawCtx} →
         PreTerm Γ₁ (∗ ∷ Γ₂) → PreTerm Γ₁ Ø → PreTerm Γ₁ Γ₂
instPT (t , p) (s , q) = mkPreTerm (DO-inst _ _ p q)

dialgPT : {Γ Γ' : RawCtx} (Δ : RawCtx) →
          CtxMorP Γ' Γ → PreType (Γ ∷ Ø) Γ' Ø → FP → PreTerm Δ (∗ ∷ Γ')
dialgPT Δ f (A , p) ρ = mkPreTerm (DO-dialg _ _ _ ρ (projCtxMor₂ f) p)

mappingPT : {Γ : RawCtx} (Δ : RawCtx) →
            FpMapDataP → FP → PreTerm Δ Γ
mappingPT Δ gs ρ = mkPreTerm (DO-mapping _ _ ρ (projPTList₂ gs))

instWCtxMorP : {Γ₁ Γ₂ : RawCtx} →
               PreTerm Γ₁ Γ₂ → CtxMorP Γ₁ Γ₂ → PreTerm Γ₁ Ø
instWCtxMorP {Γ₂ = Ø}      M []      = M
instWCtxMorP {Γ₂ = x ∷ Γ₂} M (N ∷ f) = instWCtxMorP (instPT M N) f

-----------------------------------------------------
------ Meta operations on pre-terms and pre-types
-----------------------------------------------------

weakenPT : ∀ {Θ Γ₁ Γ₂} → PreType Θ Γ₁ Γ₂ → PreType Θ (∗ ∷ Γ₁) Γ₂
weakenPT (A , p) = (weaken A , weakenDT p)

weakenPO : {Γ₁ Γ₂ : RawCtx} → PreTerm Γ₁ Γ₂ → PreTerm (∗ ∷ Γ₁) Γ₂
weakenPO (t , p) = (weaken t , weakenDO p)

get' : {Γ₁ Γ₂ : RawCtx} →
       (f : CtxMor (λ _ → PreTerm) Γ₂ Γ₁) →
       (x : RawVar Γ₁) →
       DecentTerm (get {Raw} (projCtxMor₁ f) x)
get' (t ∷ f) zero                = proj₂ t
get' (t ∷ f) (succ {b = ∗} .∗ x) = get' f x

-- | Lift substitutions to DecentTerm predicate
substDO : {Γ₁ Γ Γ₂ : RawCtx} {t : Raw Ø Γ₁ Γ} →
          (f : CtxMorP Γ₂ Γ₁) →
          DecentTerm t → DecentTerm (substRaw t (projCtxMor₁ f))
substDO f (DO-unit Γ₁)              = DO-unit _
substDO f (DO-objVar Γ₁ x)          = get' f x
substDO f (DO-inst t s p q)         = DO-inst _ _ (substDO f p) (substDO f q)
substDO f (DO-dialg Γ₁ g A ρ p q)   = DO-dialg _ _ _ _ p q
substDO f (DO-mapping Γ₁ gs ρ p)    = DO-mapping _ _ _ p

-- | Lift substRaw to pre terms
substP : {Γ₁ Γ Γ₂ : RawCtx} →
         PreTerm Γ₁ Γ → CtxMorP Γ₂ Γ₁ → PreTerm Γ₂ Γ
substP (t , p) f = (substRaw t (projCtxMor₁ f) , substDO f p)

-- | Context identity is a decent context morphism
ctxidDO : (Γ : RawCtx) → DecentCtxMor (ctxid Γ)
ctxidDO Ø       = ∗
ctxidDO (x ∷ Γ) = (DO-objVar _ zero , weakenDecentCtxMor (ctxidDO Γ))

mkCtxMorP₁ : {Γ₁ Γ₂ : RawCtx} {f : CtxMor Raw Γ₁ Γ₂} →
             (p : DecentCtxMor f) → projCtxMor₁ (mkCtxMorP p) ≡ f
mkCtxMorP₁ {Γ₂ = Ø}      {[]} p = refl
mkCtxMorP₁ {Γ₂ = x ∷ Γ₂} {t ∷ f} (p , ps) =
  begin
    projCtxMor₁ ((t , p) ∷ mkCtxMorP ps)
  ≡⟨ refl ⟩
    t ∷ projCtxMor₁ (mkCtxMorP ps)
  ≡⟨ cong (λ u → t ∷ u) (mkCtxMorP₁ ps) ⟩
    t ∷ f
  ∎

ctxidP : (Γ : RawCtx) → CtxMorP Γ Γ
ctxidP Γ = mkCtxMorP (ctxidDO Γ)

-- | Context projection is a decent context morphism
ctxProjDO : (Γ₁ Γ₂ : RawCtx) → DecentCtxMor (ctxProjRaw Γ₁ Γ₂)
ctxProjDO Γ₁ Ø        = ctxidDO Γ₁
ctxProjDO Γ₁ (x ∷ Γ₂) = weakenDecentCtxMor (ctxProjDO Γ₁ Γ₂)

ctxProjP : (Γ₁ Γ₂ : RawCtx) → CtxMorP (Γ₂ ++ Γ₁) Γ₁
ctxProjP Γ₁ Γ₂ = mkCtxMorP (ctxProjDO Γ₁ Γ₂)

weakenDO' : {Γ₁ Γ₃ : RawCtx} {t : Raw Ø Γ₁ Γ₃} →
            (Γ₂ : RawCtx) → DecentTerm t → DecentTerm (weaken' Γ₂ t)
weakenDO' {Γ₁} {t = t} Γ₂ p =
  subst DecentTerm
        (cong (substRaw t) (mkCtxMorP₁ (ctxProjDO Γ₁ Γ₂)))
        (substDO (ctxProjP Γ₁ Γ₂) p)

weakenPO' : {Γ₁ Γ₃ : RawCtx} →
            (Γ₂ : RawCtx) → PreTerm Γ₁ Γ₃ → PreTerm (Γ₂ ++ Γ₁) Γ₃
weakenPO' Γ₂ (t , p) = (weaken' Γ₂ t , weakenDO' Γ₂ p)

weakenPO'' : {Γ₁ Γ₃ : RawCtx} →
            (Γ₂ Γ₂' : RawCtx) → PreTerm Γ₁ Γ₃ → PreTerm (Γ₂' ++ Γ₁ ++ Γ₂) Γ₃
weakenPO'' = {!!}

-- | Project a specific variable out
projVar : (Γ₁ Γ₂ : RawCtx) → PreTerm (Γ₂ ++ ∗ ∷ Γ₁) Ø
projVar Γ₁ Ø        = varPT _ zero
projVar Γ₁ (∗ ∷ Γ₂) = weakenPO (projVar Γ₁ Γ₂)

-----------------------------------------------------
---- Action of types on terms
-----------------------------------------------------

shift-lemma : {A : Set} → (x y : List A) → (a : A) →
              x ++ (a ∷ y) ≡ (x ++ a ∷ Ø) ++ y
shift-lemma Ø       y a = refl
shift-lemma (b ∷ x) y a = cong (_∷_ b) (shift-lemma x y a)

Args : TyCtx → Set
Args Ø = ⊥
Args (Γ ∷ Θ) = (PreTerm (∗ ∷ Γ) Ø) × (Args Θ)

getArg : ∀ {Θ Γ₁} → TyVar Θ Γ₁ → Args Θ → PreTerm (∗ ∷ Γ₁) Ø
getArg zero        (t , ts) = t
getArg (succ Γ₁ X) (t , ts) = getArg X ts

substArgCodomTypes : ∀ {Θ Γ Γ₁} →
                Args Θ → PreType (Γ ∷ Θ) Γ₁ Ø → PreType (Γ ∷ Ø) Γ₁ Ø
substArgCodomTypes {Ø} () A
substArgCodomTypes {Γ ∷ Θ} (M , a) A = {!!}

{-# NON_TERMINATING #-}
⟪_⟫ : ∀ {Θ Γ₁ Γ₂} → PreType Θ Γ₁ Γ₂ → Args Θ → PreTerm (∗ ∷ Γ₂ ++ Γ₁) Ø
⟪_⟫ {Θ} {Γ₁} (instRaw {Γ₂ = Γ₂} A t , DT-inst .A .t dt-A do-t) ts =
  substP (⟪ A , dt-A ⟫ ts) f
  where
    -- | Substitute t for the second variable, i.e., f = (id, t, x).
    f : CtxMorP (∗ ∷ Γ₂ ++ Γ₁) (∗ ∷ ∗ ∷ Γ₂ ++ Γ₁)
    f = (varPT (∗ ∷ Γ₂ ++ Γ₁) zero)
        ∷ weakenPO' (∗ ∷ Γ₂) (t , do-t)
        ∷ ctxProjP (Γ₂ ++ Γ₁) (∗ ∷ Ø)
⟪ unitRaw Γ         , () ⟫ ts
⟪ objVarRaw Γ x     , () ⟫ ts
⟪ dialgRaw Δ x A x₁ , () ⟫ ts
⟪ mappingRaw Γ Δ x x₁ , () ⟫ ts
⟪ ⊤-Raw Θ Γ , DT-⊤ .Θ .Γ ⟫ ts = ((objVarRaw (∗ ∷ Γ) zero) , (DO-objVar _ _))
⟪ tyVarRaw Γ₁ X , DT-tyVar .Γ₁ .X ⟫ ts = weakenPO'' Γ₁ Ø (getArg X ts)
⟪ paramAbstrRaw {Γ₂ = Γ₂} Γ₁ A , DT-paramAbstr .Γ₁ .A p ⟫ ts =
  subst (λ u → PreTerm u Ø)
        (cong (_∷_ ∗) (shift-lemma Γ₂ Γ₁ ∗))
        (⟪ A , p ⟫ ts)
⟪ fpRaw {Θ} {Γ₂} Γ₁ μ D , DT-fp .Γ₁ .μ .D p ⟫ ts =
  instWCtxMorP (mappingPT _ (gs D p) μ) (ctxidP _)
  where
    -- Construction of gₖ = αₖ id (⟪ Bₖ ⟫ (ts, id))
    mkBase : ∀{Γ'} (x : CtxMor Raw Γ' Γ₂ × Raw (Γ₂ ∷ Θ) Γ' Ø) →
             (f : DecentCtxMor (proj₁ x)) →
             (A : DecentType (proj₂ x)) →
             Σ RawCtx (λ Γ' → PreTerm (∗ ∷ Γ') Ø)
    mkBase {Γ'} x f A = (Γ' , instWCtxMorP α r)
      where
        B : PreType (Γ₂ ∷ Θ) Γ' Ø
        B = mkPreType A

        A₂ : PreType (Γ₂ ∷ Ø) Γ' Ø
        A₂ = substArgCodomTypes ts B

        α : PreTerm (∗ ∷ Γ') (∗ ∷ Γ')
        α = dialgPT _ (mkCtxMorP f) A₂ μ

        r : CtxMorP (∗ ∷ Γ') (∗ ∷ Γ')
        r = (⟪ B ⟫ ((varPT _ zero) , ts)) ∷ ctxProjP Γ' (∗ ∷ Ø)

    -- Construct the g₁, ..., gₙ used in the recursion
    gs : (D : FpData Raw Θ Γ₂) → DecentFpData D → FpMapDataP
    gs [ Γ' , x ] (f , A) = [ mkBase x f A ]
    gs ((Γ' , x) ∷ D₁) ((f , A) , p₁) = mkBase x f A ∷ gs D₁ p₁

⟪_⟫ (fpRaw Γ₁ ν x₁ , DT-fp .Γ₁ .ν .x₁ x) ts = {!!}

-----------------------------------------------------
---- Reduction relation on pre-types and pre-terms
-----------------------------------------------------

data _≻_  : {Γ₁ Γ₂ : RawCtx} → (t s : PreTerm Γ₁ Γ₂) → Set where
  contract-rec : {Γ : RawCtx} → (gs : NList (PreTerm (∗ ∷ Γ) Ø)) →
    instPT
      (mappingPT {!!} {!!} μ)
      (instPT (dialgPT {!!} {!!} {!!} μ) {!!})
    ≻ {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
open import Nat
open import Prelude
open import contexts
open import core

module dynamics-core where
  open core public

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

    -- internal expressions
    data ihexp : Set where
      N          : Nat → ihexp
      _·+_       : ihexp → ihexp → ihexp
      X          : Nat → ihexp
      ·λ_·[_]_   : Nat → htyp → ihexp → ihexp
      _∘_        : ihexp → ihexp → ihexp
      inl        : htyp → ihexp → ihexp
      inr        : htyp → ihexp → ihexp
      case       : ihexp → Nat → ihexp → Nat → ihexp → ihexp
      ⟨_,_⟩      : ihexp → ihexp → ihexp
      fst        : ihexp → ihexp
      snd        : ihexp → ihexp
      ⦇-⦈⟨_⟩     : (Nat × env) → ihexp
      ⦇⌜_⌟⦈⟨_⟩   : ihexp → (Nat × env) → ihexp
      _⟨_⇒_⟩     : ihexp → htyp → htyp → ihexp
      _⟨_⇒⦇-⦈⇏_⟩ : ihexp → htyp → htyp → ihexp

  -- convenient notation for chaining together two agreeable casts
  _⟨_⇒_⇒_⟩ : ihexp → htyp → htyp → htyp → ihexp
  d ⟨ t1 ⇒ t2 ⇒ t3 ⟩ = d ⟨ t1 ⇒ t2 ⟩ ⟨ t2 ⇒ t3 ⟩

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

    -- the hole name u does not appear in the term e
  data hole-name-new : hexp → Nat → Set where
    HNNum  : ∀{n u} → hole-name-new (N n) u
    HNPlus : ∀{e1 e2 u} →
             hole-name-new e1 u →
             hole-name-new e2 u →
             hole-name-new (e1 ·+ e2) 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
    HNAp   : ∀{e1 e2 u} →
             hole-name-new e1 u →
             hole-name-new e2 u →
             hole-name-new (e1 ∘ e2) u
    HNInl  : ∀{e u} →
             hole-name-new e u →
             hole-name-new (inl e) u
    HNInr  : ∀{e u} →
             hole-name-new e u →
             hole-name-new (inr e) u
    HNCase : ∀{e x e1 y e2 u} →
             hole-name-new e u →
             hole-name-new e1 u →
             hole-name-new e2 u →
             hole-name-new (case e x e1 y e2) u
    HNPair : ∀{e1 e2 u} →
             hole-name-new e1 u →
             hole-name-new e2 u →
             hole-name-new ⟨ e1 , e2 ⟩ u
    HNFst  : ∀{e u} →
             hole-name-new e u →
             hole-name-new (fst e) u
    HNSnd  : ∀{e u} →
             hole-name-new e u →
             hole-name-new (snd 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

  -- two terms that do not share any hole names
  data holes-disjoint : hexp → hexp → Set where
    HDNum  : ∀{n e} → holes-disjoint (N n) e
    HDPlus : ∀{e1 e2 e3} →
             holes-disjoint e1 e3 →
             holes-disjoint e2 e3 →
             holes-disjoint (e1 ·+ e2) e3
    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
    HDAp   : ∀{e1 e2 e3} →
             holes-disjoint e1 e3 →
             holes-disjoint e2 e3 →
             holes-disjoint (e1 ∘ e2) e3
    HDInl  : ∀{e1 e2} →
             holes-disjoint e1 e2 →
             holes-disjoint (inl e1) e2
    HDInr  : ∀{e1 e2} →
             holes-disjoint e1 e2 →
             holes-disjoint (inr e1) e2
    HDCase : ∀{e x e1 y e2 e3} →
             holes-disjoint e e3 →
             holes-disjoint e1 e3 →
             holes-disjoint e2 e3 →
             holes-disjoint (case e x e1 y e2) e3
    HDPair : ∀{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
    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

  -- all hole names in the term are unique
  data holes-unique : hexp → Set where
    HUNum  : ∀{n} →
             holes-unique (N n)
    HUPlus : ∀{e1 e2} →
             holes-unique e1 →
             holes-unique e2 →
             holes-disjoint e1 e2 →
             holes-unique (e1 ·+ e2)
    HUAsc  : ∀{e τ} →
             holes-unique e →
             holes-unique (e ·: τ)
    HUVar  : ∀{x} →
             holes-unique (X x)
    HULam1 : ∀{x e} →
             holes-unique e →
             holes-unique (·λ x e)
    HULam2 : ∀{x e τ} →
             holes-unique e →
             holes-unique (·λ x ·[ τ ] e)
    HUAp   : ∀{e1 e2} →
             holes-unique e1 →
             holes-unique e2 →
             holes-disjoint e1 e2 →
             holes-unique (e1 ∘ e2)
    HUInl  : ∀{e} →
             holes-unique e →
             holes-unique (inl e)
    HUInr  : ∀{e} →
             holes-unique e →
             holes-unique (inr e)
    HUCase : ∀{e x e1 y e2} →
             holes-unique e →
             holes-unique e1 →
             holes-unique e2 →
             holes-disjoint e e1 →
             holes-disjoint e e2 →
             holes-disjoint e1 e2 →
             holes-unique (case e x e1 y e2)
    HUPair : ∀{e1 e2} →
             holes-unique e1 →
             holes-unique e2 →
             holes-disjoint e1 e2 →
             holes-unique ⟨ e1 , e2 ⟩
    HUFst  : ∀{e} →
             holes-unique e →
             holes-unique (fst e)
    HUSnd  : ∀{e} →
             holes-unique e →
             holes-unique (snd e)
    HUHole : ∀{u} →
             holes-unique (⦇-⦈[ u ])
    HUNEHole : ∀{u e} →
               holes-unique e →
               hole-name-new e u →
               holes-unique (⦇⌜ e ⌟⦈[ u ])

  -- freshness for external expressions
  data freshh : Nat → hexp → Set where
    FRHNum    : ∀{x n} →
                freshh x (N n)
    FRHPlus   : ∀{x d1 d2} →
                freshh x d1 →
                freshh x d2 →
                freshh x (d1 ·+ d2)
    FRHAsc    : ∀{x e τ} →
                freshh x e →
                freshh x (e ·: τ)
    FRHVar    : ∀{x y} →
                x ≠ y →
                freshh x (X y)
    FRHLam1   : ∀{x y e} →
                x ≠ y →
                freshh x e →
                freshh x (·λ y e)
    FRHLam2   : ∀{x τ e y} →
                x ≠ y →
                freshh x e →
                freshh x (·λ y ·[ τ ] e)
    FRHAp     : ∀{x e1 e2} →
                freshh x e1 →
                freshh x e2 →
                freshh x (e1 ∘ e2)
    FRHInl    : ∀{x d} →
                freshh x d →
                freshh x (inl d)
    FRHInr    : ∀{x d} →
                freshh x d →
                freshh x (inr d)
    FRHCase   : ∀{x d y d1 z d2} →
                freshh x d →
                x ≠ y →
                freshh x d1 →
                x ≠ z →
                freshh x d2 →
                freshh x (case d y d1 z d2)
    FRHPair   : ∀{x d1 d2} →
                freshh x d1 →
                freshh x d2 →
                freshh x ⟨ d1 , d2 ⟩
    FRHFst    : ∀{x d} →
                freshh x d →
                freshh x (fst d)
    FRHSnd    : ∀{x d} →
                freshh x d →
                freshh x (snd d)
    FRHEHole  : ∀{x u} →
                freshh x (⦇-⦈[ u ])
    FRHNEHole : ∀{x u e} →
                freshh x e →
                freshh x (⦇⌜ e ⌟⦈[ u ])

  -- those internal expressions without holes
  data _dcomplete : ihexp → Set where
    DCNum  : ∀{n} →
             (N n) dcomplete
    DCPlus : ∀{d1 d2} →
             d1 dcomplete →
             d2 dcomplete →
             (d1 ·+ d2) dcomplete
    DCVar  : ∀{x} →
             (X x) dcomplete
    DCLam  : ∀{x τ d} →
             d dcomplete →
             τ tcomplete →
             (·λ x ·[ τ ] d) dcomplete
    DCAp   : ∀{d1 d2} →
             d1 dcomplete →
             d2 dcomplete →
             (d1 ∘ d2) dcomplete
    DCInl  : ∀{τ d} →
             τ tcomplete →
             d dcomplete →
             (inl τ d) dcomplete
    DCInr  : ∀{τ d} →
             τ tcomplete →
             d dcomplete →
             (inr τ d) dcomplete
    DCCase : ∀{d x d1 y d2} →
             d dcomplete →
             d1 dcomplete →
             d2 dcomplete →
             (case d x d1 y d2) dcomplete
    DCPair : ∀{d1 d2} →
             d1 dcomplete →
             d2 dcomplete →
             ⟨ d1 , d2 ⟩ dcomplete
    DCFst  : ∀{d} →
             d dcomplete →
             (fst d) dcomplete
    DCSnd  : ∀{d} →
             d dcomplete →
             (snd d) dcomplete
    DCCast : ∀{d τ1 τ2} →
             d dcomplete →
             τ1 tcomplete →
             τ2 tcomplete →
             (d ⟨ τ1 ⇒ τ2 ⟩) dcomplete

  -- expansion
  mutual
    -- synthesis
    data _⊢_⇒_~>_⊣_ : (Γ : tctx) (e : hexp) (τ : htyp) (d : ihexp) (Δ : hctx) → Set where
      ESNum    : ∀{Γ n} →
                 Γ ⊢ (N n) ⇒ num ~> (N n) ⊣ ∅
      ESPlus   : ∀{Γ e1 e2 d1 d2 Δ1 Δ2 τ1 τ2} →
                 holes-disjoint e1 e2 →
                 Δ1 ## Δ2 →
                 Γ ⊢ e1 ⇐ num ~> d1 :: τ1 ⊣ Δ1 →
                 Γ ⊢ e2 ⇐ num ~> d2 :: τ2 ⊣ Δ2 →
                 Γ ⊢ e1 ·+ e2 ⇒ num ~> (d1 ⟨ τ1 ⇒ num ⟩) ·+ (d2 ⟨ τ2 ⇒ num ⟩) ⊣ (Δ1 ∪ Δ2)
      ESAsc    : ∀{Γ e τ d τ' Δ} →
                 Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                 Γ ⊢ (e ·: τ) ⇒ τ ~> d ⟨ τ' ⇒ τ ⟩ ⊣ Δ
      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)
      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)
      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 ⟩) ⊣ Δ
      ESEHole  : ∀{Γ u} →
                 Γ ⊢ ⦇-⦈[ u ] ⇒ ⦇-⦈ ~> ⦇-⦈⟨ u , Id Γ ⟩ ⊣  ■ (u :: ⦇-⦈ [ Γ ])
      ESNEHole : ∀{Γ e τ d u Δ} →
                 Δ ## (■ (u , Γ , ⦇-⦈)) →
                 Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                 Γ ⊢ ⦇⌜ e ⌟⦈[ u ] ⇒ ⦇-⦈ ~> ⦇⌜ d ⌟⦈⟨ u , Id Γ  ⟩ ⊣ (Δ ,, u :: ⦇-⦈ [ Γ ])

    -- analysis
    data _⊢_⇐_~>_::_⊣_ : (Γ : tctx) (e : hexp) (τ : htyp)
                         (d : ihexp) (τ' : htyp) (Δ : hctx) → Set where
      EASubsume : ∀{e Γ τ' d Δ τ} →
                  ((u : Nat) → e ≠ ⦇-⦈[ u ]) →
                  ((e' : hexp) (u : Nat) → e ≠ ⦇⌜ e' ⌟⦈[ u ]) →
                  Γ ⊢ e ⇒ τ' ~> d ⊣ Δ →
                  τ ~ τ' →
                  Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ
      EALam     : ∀{Γ x τ τ1 τ2 e d τ2' Δ} →
                  x # Γ →
                  τ ▸arr τ1 ==> τ2 →
                  (Γ ,, (x , τ1)) ⊢ e ⇐ τ2 ~> d :: τ2' ⊣ Δ →
                  Γ ⊢ ·λ x e ⇐ τ ~> ·λ x ·[ τ1 ] d :: τ1 ==> τ2' ⊣ Δ
      EAInl     : ∀{Γ τ τ1 τ2 e d τ1' Δ} →
                  τ ▸sum τ1 ⊕ τ2 →
                  Γ ⊢ e ⇐ τ1 ~> d :: τ1' ⊣ Δ →
                  Γ ⊢ inl e ⇐ τ ~> inl τ2 d :: τ1' ⊕ τ2 ⊣ Δ
      EAInr     : ∀{Γ τ τ1 τ2 e d τ2' Δ} →
                  τ ▸sum τ1 ⊕ τ2 →
                  Γ ⊢ e ⇐ τ2 ~> d :: τ2' ⊣ Δ →
                  Γ ⊢ inr e ⇐ τ ~> inr τ1 d :: τ1 ⊕ τ2' ⊣ Δ
      EACase    : ∀{Γ e τ+ d Δ τ1 τ2 τ x e1 d1 τr1 Δ1 y e2 d2 τr2 Δ2} →
                  holes-disjoint e e1 →
                  holes-disjoint e e2 →
                  holes-disjoint e1 e2 →
                  Δ ## Δ1 →
                  Δ ## Δ2 →
                  Δ1 ## Δ2 →
                  x # Γ →
                  y # Γ →
                  Γ ⊢ e ⇒ τ+ ~> d ⊣ Δ →
                  τ+ ▸sum τ1 ⊕ τ2 →
                  (Γ ,, (x , τ1)) ⊢ e1 ⇐ τ ~> d1 :: τr1 ⊣ Δ1 →
                  (Γ ,, (y , τ2)) ⊢ e2 ⇐ τ ~> d2 :: τr2 ⊣ Δ2 →
                  Γ ⊢ case e x e1 y e2 ⇐ τ ~>
                    case (d ⟨ τ+ ⇒ τ1 ⊕ τ2 ⟩) x (d1 ⟨ τr1 ⇒ τ ⟩) y (d2 ⟨ τr2 ⇒ τ ⟩) :: τ
                      ⊣ (Δ ∪ (Δ1 ∪ Δ2))
      EAEHole   : ∀{Γ u τ} →
                  Γ ⊢ ⦇-⦈[ u ] ⇐ τ ~> ⦇-⦈⟨ u , Id Γ  ⟩ :: τ ⊣ ■ (u :: τ [ Γ ])
      EANEHole  : ∀{Γ e u τ d τ' Δ} →
                  Δ ## (■ (u , Γ , τ)) →
                  Γ ⊢ e ⇒ τ' ~> d ⊣ Δ →
                  Γ ⊢ ⦇⌜ e ⌟⦈[ u ] ⇐ τ ~> ⦇⌜ d ⌟⦈⟨ u , Id Γ  ⟩ :: τ ⊣ (Δ ,, u :: τ [ Γ ])

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

    -- type assignment
    data _,_⊢_::_ : (Δ : hctx) (Γ : tctx) (d : ihexp) (τ : htyp) → Set where
      TANum    : ∀{Δ Γ n} →
                 Δ , Γ ⊢ (N n) :: num
      TAPlus   : ∀{Δ Γ d1 d2} →
                 Δ , Γ ⊢ d1 :: num →
                 Δ , Γ ⊢ d2 :: num →
                 Δ , Γ ⊢ (d1 ·+ d2) :: num
      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 :: τ
      TAInl    : ∀{Δ Γ d τ1 τ2} →
                 Δ , Γ ⊢ d :: τ1 →
                 Δ , Γ ⊢ inl τ2 d :: τ1 ⊕ τ2
      TAInr    : ∀{Δ Γ d τ1 τ2} →
                 Δ , Γ ⊢ d :: τ2 →
                 Δ , Γ ⊢ inr τ1 d :: τ1 ⊕ τ2
      TACase   : ∀{Δ Γ d τ1 τ2 τ x d1 y d2} →
                 Δ , Γ ⊢ d :: τ1 ⊕ τ2 →
                 x # Γ →
                 Δ , (Γ ,, (x , τ1)) ⊢ d1 :: τ →
                 y # Γ →
                 Δ , (Γ ,, (y , τ2)) ⊢ d2 :: τ →
                 Δ , Γ ⊢ case d x d1 y d2 :: τ
      TAPair   : ∀{Δ Γ d1 d2 τ1 τ2} →
                 Δ , Γ ⊢ d1 :: τ1 →
                 Δ , Γ ⊢ d2 :: τ2 →
                 Δ , Γ ⊢ ⟨ d1 , d2 ⟩ :: τ1 ⊠ τ2
      TAFst    : ∀{Δ Γ d τ1 τ2} →
                 Δ , Γ ⊢ d :: τ1 ⊠ τ2 →
                 Δ , Γ ⊢ fst d :: τ1
      TASnd    : ∀{Δ Γ d τ1 τ2} →
                 Δ , Γ ⊢ d :: τ1 ⊠ τ2 →
                 Δ , Γ ⊢ snd d :: τ2
      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

  -- substitution
  [_/_]_ : ihexp → Nat → ihexp → ihexp
  [ d / y ] (N n) = N n
  [ d / y ] (d1 ·+ d2) = ([ d / y ] d1) ·+ ([ d / y ] d2)
  [ 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 ] (d1 ∘ d2) = ([ d / y ] d1) ∘ ([ d / y ] d2)
  [ d / y ] (inl τ d') = inl τ ([ d / y ] d')
  [ d / y ] (inr τ d') = inr τ ([ d / y ] d')
  [ d / y ] (case d' x d1 z d2)
    with natEQ x y | natEQ z y
  ... | Inl refl | Inl refl = case ([ d / y ] d') x d1 z d2
  ... | Inl refl | Inr neq  = case ([ d / y ] d') x d1 z ([ d / y ] d2)
  ... | Inr neq  | Inl refl = case ([ d / y ] d') x ([ d / y ] d1) z d2
  ... | Inr neq1 | Inr neq2 = case ([ d / y ] d') x ([ d / y ] d1) z ([ d / y ] d2)
  [ 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')
  [ d / y ] ⦇-⦈⟨ u , σ ⟩ = ⦇-⦈⟨ u , Subst d y σ ⟩
  [ d / y ] ⦇⌜ d' ⌟⦈⟨ u , σ  ⟩ =  ⦇⌜ [ d / y ] d' ⌟⦈⟨ u , Subst d y σ ⟩
  [ d / y ] (d' ⟨ τ1 ⇒ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒ τ2 ⟩
  [ d / y ] (d' ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩ ) = ([ d / y ] d') ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩

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

  -- values
  data _val : (d : ihexp) → Set where
    VNum  : ∀{n} → (N n) val
    VLam  : ∀{x τ d} → (·λ x ·[ τ ] d) val
    VInl  : ∀{d τ} → d val → (inl τ d) val
    VInr  : ∀{d τ} → d val → (inr τ d) val
    VPair : ∀{d1 d2} → d1 val → d2 val → ⟨ d1 , d2 ⟩ val

  -- boxed values
  data _boxedval : (d : ihexp) → Set where
    BVVal      : ∀{d} →
                 d val →
                 d boxedval
    BVInl      : ∀{d τ} →
                 d boxedval →
                 (inl τ d) boxedval
    BVInr      : ∀{d τ} →
                 d boxedval →
                 (inr τ 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
    BVSumCast  : ∀{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 : ihexp) → Set where
      IPlus1    : ∀{d1 d2} →
                  d1 indet →
                  d2 final →
                  (d1 ·+ d2) indet
      IPlus2    : ∀{d1 d2} →
                  d1 final →
                  d2 indet →
                  (d1 ·+ d2) indet
      IAp       : ∀{d1 d2} →
                  ((τ1 τ2 τ3 τ4 : htyp) (d1' : ihexp) →
                    d1 ≠ (d1' ⟨(τ1 ==> τ2) ⇒ (τ3 ==> τ4)⟩)) →
                  d1 indet →
                  d2 final →
                  (d1 ∘ d2) indet
      IInl      : ∀{d τ} →
                  d indet →
                  (inl τ d) indet
      IInr      : ∀{d τ} →
                  d indet →
                  (inr τ d) indet
      ICase     : ∀{d x d1 y d2} →
                  ((τ : htyp) (d' : ihexp) →
                    d ≠ inl τ d') →
                  ((τ : htyp) (d' : ihexp) →
                    d ≠ inr τ d') →
                  ((τ1 τ2 τ1' τ2' : htyp) (d' : ihexp) →
                    d ≠ (d' ⟨(τ1 ⊕ τ2) ⇒ (τ1' ⊕ τ2')⟩)) →
                  d indet →
                  (case d x d1 y d2) indet
      IPair1    : ∀{d1 d2} →
                  d1 indet →
                  d2 final →
                  ⟨ d1 , d2 ⟩ indet
      IPair2    : ∀{d1 d2} →
                  d1 final →
                  d2 indet →
                  ⟨ d1 , d2 ⟩ indet
      IFst      : ∀{d} →
                  ((d1 d2 : ihexp) →
                    d ≠ ⟨ d1 , d2 ⟩) →
                  ((τ1 τ2 τ1' τ2' : htyp) (d' : ihexp) →
                    d ≠ (d' ⟨(τ1 ⊠ τ2) ⇒ (τ1' ⊠ τ2')⟩)) →
                  d indet →
                  (fst d) indet
      ISnd      : ∀{d} →
                  ((d1 d2 : ihexp) →
                    d ≠ ⟨ d1 , d2 ⟩) →
                  ((τ1 τ2 τ1' τ2' : htyp) (d' : ihexp) →
                    d ≠ (d' ⟨(τ1 ⊠ τ2) ⇒ (τ1' ⊠ τ2')⟩)) →
                  d indet →
                  (snd d) indet
      IEHole    : ∀{u σ} →
                  ⦇-⦈⟨ u , σ ⟩ indet
      INEHole   : ∀{d u σ} →
                  d final →
                  ⦇⌜ d ⌟⦈⟨ u , σ ⟩ indet
      ICastArr  : ∀{d τ1 τ2 τ3 τ4} →
                  τ1 ==> τ2 ≠ τ3 ==> τ4 →
                  d indet →
                  d ⟨ (τ1 ==> τ2) ⇒ (τ3 ==> τ4) ⟩ indet
      ICastSum  : ∀{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' : ihexp) (τ' : htyp) → 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 : ihexp) → Set where
      FBoxedVal : ∀{d} → d boxedval → d final
      FIndet    : ∀{d} → d indet → d final

  -- contextual dynamics

  -- evaluation contexts
  data ectx : Set where
    ⊙ : ectx
    _·+₁_  : ectx → ihexp → ectx
    _·+₂_  : ihexp → ectx → ectx
    _∘₁_   : ectx → ihexp → ectx
    _∘₂_   : ihexp → ectx → ectx
    inl    : htyp → ectx → ectx
    inr    : htyp → ectx → ectx
    case   : ectx → Nat → ihexp → Nat → ihexp → ectx
    ⟨_,_⟩₁ : ectx → ihexp → ectx
    ⟨_,_⟩₂ : ihexp → ectx → ectx
    fst    : ectx → ectx
    snd    : ectx → ectx
    ⦇⌜_⌟⦈⟨_⟩   : ectx → (Nat × env ) → ectx
    _⟨_⇒_⟩ : ectx → htyp → htyp → ectx
    _⟨_⇒⦇-⦈⇏_⟩ : ectx → htyp → htyp → 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 it's either trival to prove or
  -- provides no additional information

   --ε is an evaluation context
  data _evalctx : (ε : ectx) → Set where
    ECDot   : ⊙ evalctx
    ECPlus1  : ∀{d ε} →
               ε evalctx →
               (ε ·+₁ d) evalctx
    ECPlus2  : ∀{d ε} →
               -- d final → -- red brackets
               ε evalctx →
               (d ·+₂ ε) evalctx
    ECAp1    : ∀{d ε} →
               ε evalctx →
               (ε ∘₁ d) evalctx
    ECAp2    : ∀{d ε} →
               -- d final → -- red brackets
               ε evalctx →
               (d ∘₂ ε) evalctx
    ECInl    : ∀{τ ε} →
               ε evalctx →
               (inl τ ε) evalctx
    ECInr    : ∀{τ ε} →
               ε evalctx →
               (inr τ ε) evalctx
    ECCase   : ∀{ε x d1 y d2} →
               ε evalctx →
               (case ε x d1 y d2) evalctx
    ECPair1  : ∀{d ε} →
               ε evalctx →
               ⟨ ε , d ⟩₁ evalctx
    ECPair2  : ∀{d ε} →
               -- d final → -- red brackets
               ε evalctx →
               ⟨ d , ε ⟩₂ evalctx
    ECFst    : ∀{ε} →
               (fst ε) evalctx
    ECSnd    : ∀{ε} →
               (snd ε) evalctx
    ECNEHole : ∀{ε u σ} →
               ε evalctx →
               ⦇⌜ ε ⌟⦈⟨ u , σ ⟩ 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 : ihexp) (ε : ectx) (d' : ihexp) → Set where
    FHOuter  : ∀{d} → d == ⊙ ⟦ d ⟧
    FHPlus1  : ∀{d1 d1' d2 ε} →
               d1 == ε ⟦ d1' ⟧ →
               (d1 ·+ d2) == (ε ·+₁ d2) ⟦ d1' ⟧
    FHPlus2  : ∀{d1 d2 d2' ε} →
               -- d1 final → -- red brackets
               d2 == ε ⟦ d2' ⟧ →
               (d1 ·+ d2) == (d1 ·+₂ ε) ⟦ d2' ⟧
    FHAp1    : ∀{d1 d1' d2 ε} →
               d1 == ε ⟦ d1' ⟧ →
               (d1 ∘ d2) == (ε ∘₁ d2) ⟦ d1' ⟧
    FHAp2    : ∀{d1 d2 d2' ε} →
               -- d1 final → -- red brackets
               d2 == ε ⟦ d2' ⟧ →
               (d1 ∘ d2) == (d1 ∘₂ ε) ⟦ d2' ⟧
    FHInl    : ∀{d d' ε τ} →
               d == ε ⟦ d' ⟧ →
               (inl τ d) == (inl τ ε) ⟦ d' ⟧
    FHInr    : ∀{d d' ε τ} →
               d == ε ⟦ d' ⟧ →
               (inr τ d) == (inr τ ε) ⟦ d' ⟧
    FHCase   : ∀{d d' x d1 y d2 ε} →
               d == ε ⟦ d' ⟧ →
               (case d x d1 y d2) == (case ε x d1 y d2) ⟦ d' ⟧
    FHPair1  : ∀{d1 d1' d2 ε} →
               d1 == ε ⟦ d1' ⟧ →
               ⟨ d1 , d2 ⟩ == ⟨ ε , d2 ⟩₁ ⟦ d1' ⟧
    FHPair2  : ∀{d1 d2 d2' ε} →
               d2 == ε ⟦ d2' ⟧ →
               ⟨ d1 , d2 ⟩ == ⟨ d1 , ε ⟩₂ ⟦ d2' ⟧
    FHFst    : ∀{d d' ε} →
               d == ε ⟦ d' ⟧ →
               fst d == (fst ε) ⟦ d' ⟧
    FHSnd    : ∀{d d' ε} →
               d == ε ⟦ d' ⟧ →
               snd d == (snd ε) ⟦ d' ⟧
    FHNEHole : ∀{d d' ε u σ} →
               d == ε ⟦ d' ⟧ →
               ⦇⌜ d ⌟⦈⟨ (u , σ ) ⟩ ==  ⦇⌜ ε ⌟⦈⟨ (u , σ ) ⟩ ⟦ d' ⟧
    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_ : htyp → htyp → Set where
    MGArr  : ∀{τ1 τ2} →
             (τ1 ==> τ2) ≠ (⦇-⦈ ==> ⦇-⦈) →
             (τ1 ==> τ2) ▸gnd (⦇-⦈ ==> ⦇-⦈)
    MGSum  : ∀{τ1 τ2} →
             (τ1 ⊕ τ2) ≠ (⦇-⦈ ⊕ ⦇-⦈) →
             (τ1 ⊕ τ2) ▸gnd (⦇-⦈ ⊕ ⦇-⦈)
    MGProd : ∀{τ1 τ2} →
             (τ1 ⊠ τ2) ≠ (⦇-⦈ ⊠ ⦇-⦈) →
             (τ1 ⊠ τ2) ▸gnd (⦇-⦈ ⊠ ⦇-⦈)

  -- instruction transition judgement
  data _→>_ : (d d' : ihexp) → Set where
    ITPlus     : ∀{n1 n2 n3} →
                 (n1 nat+ n2) == n3 →
                 ((N n1) ·+ (N n2)) →> (N n3)
    ITLam      : ∀{x τ d1 d2} →
                 -- d2 final → -- red brackets
                 ((·λ x ·[ τ ] d1) ∘ d2) →> ([ d2 / x ] d1)
    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' ⟩)
    ITCaseInl  : ∀{d τ x d1 y d2} →
                 -- d final → -- red brackets,
                 (case (inl τ d) x d1 y d2) →> ([ d / x ] d1)
    ITCaseInr  : ∀{d τ x d1 y d2} →
                 -- d final → -- red brackets,
                 (case (inr τ d) x d1 y d2) →> ([ d / y ] d2)
    ITCaseCast : ∀{d τ1 τ2 τ1' τ2' x d1 y d2} →
                 -- d final → -- red brackets
                 (case (d ⟨ τ1 ⊕ τ2 ⇒ τ1' ⊕ τ2' ⟩) x d1 y d2) →>
                   (case d x ([ (X x) ⟨ τ1 ⇒ τ1' ⟩ / x ] d1) y ([ (X y) ⟨ τ2 ⇒ τ2' ⟩ / y ] d2))
    ITFstPair  : ∀{d1 d2} →
                 -- d1 final → -- red brackets
                 -- d2 final → -- red brackets
                 fst ⟨ d1 , d2 ⟩ →> d1
    ITFstCast  : ∀{d τ1 τ2 τ1' τ2' } →
                 -- d final → -- red brackets
                 fst (d ⟨ τ1 ⊠ τ2 ⇒ τ1' ⊠ τ2' ⟩) →> ((fst d) ⟨ τ1 ⇒ τ1' ⟩)
    ITSndPair  : ∀{d1 d2} →
                 -- d1 final → -- red brackets
                 -- d2 final → -- red brackets
                 snd ⟨ d1 , d2 ⟩ →> d2
    ITSndCast  : ∀{d τ1 τ2 τ1' τ2' } →
                 -- d final → -- red brackets
                 snd (d ⟨ τ1 ⊠ τ2 ⇒ τ1' ⊠ τ2' ⟩) →> ((snd d) ⟨ τ2 ⇒ τ2' ⟩)
    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 ⟩)
    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' : ihexp) → 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' : ihexp) → Set where
    MSRefl : ∀{d} → d ↦* d
    MSStep : ∀{d d' d''} →
             d ↦ d' →
             d' ↦* d'' →
             d  ↦* d''

  -- those internal expressions where every cast is the identity cast and
  -- there are no failed casts
  data cast-id : ihexp → Set where
    CINum    : ∀{n} →
               cast-id (N n)
    CIPlus   : ∀{d1 d2} →
               cast-id d1 →
               cast-id d2 →
               cast-id (d1 ·+ d2)
    CIVar    : ∀{x} →
               cast-id (X x)
    CILam    : ∀{x τ d} →
               cast-id d →
               cast-id (·λ x ·[ τ ] d)
    CIAp     : ∀{d1 d2} →
               cast-id d1 →
               cast-id d2 →
               cast-id (d1 ∘ d2)
    CIInl    : ∀{τ d} →
               cast-id d →
               cast-id (inl τ d)
    CIInr    : ∀{τ d} →
               cast-id d →
               cast-id (inr τ d)
    CICase   : ∀{d x d1 y d2} →
               cast-id d →
               cast-id d1 →
               cast-id d2 →
               cast-id (case d x d1 y d2)
    CIPair   : ∀{d1 d2} →
               cast-id d1 →
               cast-id d2 →
               cast-id ⟨ d1 , d2 ⟩
    CIFst    : ∀{d} →
               cast-id d →
               cast-id (fst d)
    CISnd    : ∀{d} →
               cast-id d →
               cast-id (snd d)
    CIHole   : ∀{u} →
               cast-id (⦇-⦈⟨ u ⟩)
    CINEHole : ∀{d u} →
               cast-id d →
               cast-id (⦇⌜ d ⌟⦈⟨ u ⟩)
    CICast   : ∀{d τ} →
               cast-id d →
               cast-id (d ⟨ τ ⇒ τ ⟩)

  -- freshness
  mutual
    -- ... with respect to a hole context
    data envfresh : Nat → 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 internal expressions
    data fresh : Nat → ihexp → Set where
      FNum    : ∀{x n} →
                fresh x (N n)
      FPlus   : ∀{x d1 d2} →
                fresh x d1 →
                fresh x d2 →
                fresh x (d1 ·+ d2)
      FVar    : ∀{x y} →
                x ≠ y →
                fresh x (X y)
      FLam    : ∀{x y τ d} →
                x ≠ y →
                fresh x d →
                fresh x (·λ y ·[ τ ] d)
      FAp     : ∀{x d1 d2} →
                fresh x d1 →
                fresh x d2 →
                fresh x (d1 ∘ d2)
      FInl    : ∀{x d τ} →
                fresh x d →
                fresh x (inl τ d)
      FInr    : ∀{x d τ} →
                fresh x d →
                fresh x (inr τ d)
      FCase   : ∀{x d y d1 z d2} →
                fresh x d →
                x ≠ y →
                fresh x d1 →
                x ≠ z →
                fresh x d2 →
                fresh x (case d y d1 z d2)
      FPair   : ∀{x d1 d2} →
                fresh x d1 →
                fresh x d2 →
                fresh x ⟨ d1 , d2 ⟩
      FFst    : ∀{x d} →
                fresh x d →
                fresh x (fst d)
      FSnd    : ∀{x d} →
                fresh x d →
                fresh x (snd d)
      FHole   : ∀{x u σ} →
                envfresh x σ →
                fresh x (⦇-⦈⟨ u , σ ⟩)
      FNEHole : ∀{x d u σ} →
                envfresh x σ →
                fresh x d →
                fresh x (⦇⌜ d ⌟⦈⟨ u , σ ⟩)
      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 ⟩)

  -- x is not used in a binding site in d
  mutual
    data unbound-in-σ : Nat → 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 : Nat) (d : ihexp) → Set where
      UBNum    : ∀{x n} → unbound-in x (N n)
      UBPlus   : ∀{x d1 d2} →
                 unbound-in x d1 →
                 unbound-in x d2 →
                 unbound-in x (d1 ·+ d2)
      UBVar    : ∀{x y} → unbound-in x (X y)
      UBLam2   : ∀{x d y τ} →
                 x ≠ y →
                 unbound-in x d →
                 unbound-in x (·λ y ·[ τ ] d)
      UBAp     : ∀{x d1 d2} →
                 unbound-in x d1 →
                 unbound-in x d2 →
                 unbound-in x (d1 ∘ d2)
      UBInl    : ∀{x d τ} →
                 unbound-in x d →
                 unbound-in x (inl τ d)
      UBInr    : ∀{x d τ} →
                 unbound-in x d →
                 unbound-in x (inr τ d)
      UBCase   : ∀{x d y d1 z d2} →
                 unbound-in x d →
                 x ≠ y →
                 unbound-in x d1 →
                 x ≠ z →
                 unbound-in x d2 →
                 unbound-in x (case d y d1 z d2)
      UBPair   : ∀{x d1 d2} →
                 unbound-in x d1 →
                 unbound-in x d2 →
                 unbound-in x ⟨ d1 , d2 ⟩
      UBFst    : ∀{x d} →
                 unbound-in x d →
                 unbound-in x (fst d)
      UBSnd    : ∀{x d} →
                 unbound-in x d →
                 unbound-in x (snd 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 , σ ⟩)
      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 ⟩)
  mutual
    data binders-disjoint-σ : env → ihexp → Set where
      BDσId    : ∀{Γ d} → binders-disjoint-σ (Id Γ) d
      BDσSubst : ∀{d1 d2 y σ} →
                 binders-disjoint d2 d1 →
                 binders-disjoint-σ σ d2 →
                 unbound-in y d2 →
                 binders-disjoint-σ (Subst d1 y σ) d2

    -- two terms that do not share any binders
    data binders-disjoint : ihexp → ihexp → Set where
      BDNum    : ∀{d n} → binders-disjoint (N n) d
      BDPlus   : ∀{d1 d2 d3} →
                 binders-disjoint d1 d3 →
                 binders-disjoint d2 d3 →
                 binders-disjoint (d1 ·+ d2) d3
      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
      BDAp     : ∀{d1 d2 d3} →
                 binders-disjoint d1 d3 →
                 binders-disjoint d2 d3 →
                 binders-disjoint (d1 ∘ d2) d3
      BDInl    : ∀{d1 d2 τ} →
                 binders-disjoint d1 d2 →
                 binders-disjoint (inl τ d1) d2
      BDInr    : ∀{d1 d2 τ} →
                 binders-disjoint d1 d2 →
                 binders-disjoint (inr τ d1) d2
      BDCase   : ∀{d x d1 y d2 d3} →
                 binders-disjoint d d3 →
                 unbound-in x d3 →
                 binders-disjoint d1 d3 →
                 unbound-in y d3 →
                 binders-disjoint d2 d3 →
                 binders-disjoint (case d x d1 y d2) d3
      BDPair   : ∀{d1 d2 d3} →
                 binders-disjoint d1 d3 →
                 binders-disjoint d2 d3 →
                 binders-disjoint ⟨ d1 , d2 ⟩ d3
      BDFst    : ∀{d1 d2} →
                 binders-disjoint d1 d2 →
                 binders-disjoint (fst d1) d2
      BDSnd    : ∀{d1 d2} →
                 binders-disjoint d1 d2 →
                 binders-disjoint (snd 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
      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

  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 : ihexp → Set where
      BUNum    : ∀{n} →
                 binders-unique (N n)
      BUPlus   : ∀{d1 d2} →
                 binders-unique d1 →
                 binders-unique d2 →
                 binders-disjoint d1 d2 →
                 binders-unique (d1 ·+ d2)
      BUVar    : ∀{x} →
                 binders-unique (X x)
      BULam    : {x : Nat} {τ : htyp} {d : ihexp} →
                 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)
      BUInl    : ∀{d τ} →
                 binders-unique d →
                 binders-unique (inl τ d)
      BUInr    : ∀{d τ} →
                 binders-unique d →
                 binders-unique (inr τ d)
      BUCase   : ∀{d x d1 y d2} →
                 binders-unique d →
                 binders-unique d1 →
                 binders-unique d2 →
                 binders-disjoint d d1 →
                 binders-disjoint d d2 →
                 binders-disjoint d1 d2 →
                 unbound-in x d →
                 unbound-in x d1 →
                 unbound-in x d2 →
                 unbound-in y d →
                 unbound-in y d1 →
                 unbound-in y d2 →
                 binders-unique (case d x d1 y d2)
      BUPair   : ∀{d1 d2} →
                 binders-unique d1 →
                 binders-unique d2 →
                 binders-disjoint d1 d2 →
                 binders-unique ⟨ d1 , d2 ⟩
      BUFst    : ∀{d} →
                 binders-unique d →
                 binders-unique (fst d)
      BUSnd    : ∀{d} →
                 binders-unique d →
                 binders-unique (snd d)
      BUCast   : ∀{d τ1 τ2} →
                 binders-unique d →
                 binders-unique (d ⟨ τ1 ⇒ τ2 ⟩)
      BUFailedCast : ∀{d τ1 τ2} →
                     binders-unique d →
                     binders-unique (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --cubical --safe #-}

module Cubical.Data.Group.Base where

import Cubical.Core.Glue as G

open import Cubical.Foundations.Prelude hiding ( comp )

import Cubical.Foundations.Isomorphism as I
import Cubical.Foundations.Equiv as E
import Cubical.Foundations.HAEquiv as HAE

record isGroup {ℓ} (A : Type ℓ) : Type ℓ where
  constructor group-struct
  field
    id  : A
    inv  : A → A
    comp  : A → A → A
    lUnit : ∀ a → comp id a ≡ a
    rUnit : ∀ a → comp a id ≡ a
    assoc  : ∀ a b c → comp (comp a b) c ≡ comp a (comp b c)
    lCancel  : ∀ a → comp (inv a) a ≡ id
    rCalcel : ∀ a → comp a (inv a) ≡ id

record Group {ℓ} : Type (ℓ-suc ℓ) where
  constructor group
  field
    type : Type ℓ
    setStruc : isSet type
    groupStruc : isGroup type

isMorph : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) → (f : (Group.type G → Group.type H)) → Type (ℓ-max ℓ ℓ')
isMorph (group G Gset (group-struct _ _ _⊙_ _ _ _ _ _))
        (group H Hset (group-struct _ _ _∘_ _ _ _ _ _)) f
        = (g0 g1 : G) → f (g0 ⊙ g1) ≡ (f g0) ∘ (f g1)

morph : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) → Type (ℓ-max ℓ ℓ')
morph G H = Σ (Group.type G →  Group.type H) (isMorph G H)

record Iso {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor iso
  field
    fun : morph G H
    inv : morph H G
    rightInv : I.section (fun .fst) (inv .fst)
    leftInv : I.retract (fun .fst) (inv .fst)

record Iso' {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor iso'
  field
    isoSet : I.Iso (Group.type G) (Group.type H)
    isoSetMorph : isMorph G H (I.Iso.fun isoSet)

_≃_ : ∀ {ℓ ℓ'} (A : Group {ℓ}) (B : Group {ℓ'}) → Type (ℓ-max ℓ ℓ')
A ≃ B = Σ (morph A B) \ f → (G.isEquiv (f .fst))

Iso'→Iso : ∀ {ℓ ℓ'} {G : Group {ℓ}} {H : Group {ℓ'}} → Iso' G  H → Iso G H
Iso'→Iso {G = group G Gset Ggroup} {H = group H Hset Hgroup} i = iso (fun , funMorph) (inv , invMorph) rightInv leftInv
  where
    G_ : Group
    G_ = (group G Gset Ggroup)

    H_ : Group
    H_ = (group H Hset Hgroup)

    open Iso'

    fun : G → H
    fun = I.Iso.fun (isoSet i)

    inv : H → G
    inv = I.Iso.inv (isoSet i)

    rightInv : I.section fun inv
    rightInv = I.Iso.rightInv (isoSet i)

    leftInv : I.retract fun inv
    leftInv = I.Iso.leftInv (isoSet i)

    e' : G G.≃ H
    e' = E.isoToEquiv (I.iso fun inv rightInv leftInv)

    funMorph : isMorph G_ H_ fun
    funMorph = isoSetMorph i

    _∘_ : H → H → H
    _∘_ = isGroup.comp Hgroup

    _⊙_ : G → G → G
    _⊙_ = isGroup.comp Ggroup

    invMorph : isMorph H_ G_ inv
    invMorph h0 h1 = E.invEq (HAE.congEquiv e')
          (fun (inv (h0 ∘ h1)) ≡⟨ rightInv (h0 ∘ h1) ⟩
           h0 ∘ h1 ≡⟨ cong (λ x → x ∘ h1) (sym (rightInv h0)) ⟩
           (fun (inv h0)) ∘ h1 ≡⟨ cong (λ x → fun (inv h0) ∘ x) (sym (rightInv h1)) ⟩
           (fun (inv h0)) ∘ (fun (inv h1)) ≡⟨ sym (funMorph (inv h0) (inv h1)) ⟩
           fun ((inv h0) ⊙ (inv h1)) ∎ )

Equiv→Iso' : ∀ {ℓ ℓ'} {G : Group {ℓ}} {H : Group {ℓ'}} → G ≃ H → Iso' G H
Equiv→Iso' {G = group G Gset Ggroup}
           {H = group H Hset Hgroup}
           e = iso' i' (e .fst .snd)
  where
    e' : G G.≃ H
    e' = (e .fst .fst) , (e .snd)

    i' : I.Iso G H
    i' = E.equivToIso e'

compMorph : ∀ {ℓ} {F G H : Group {ℓ}} (I : morph F G) (J : morph G H) → morph F H
compMorph {ℓ} {group F Fset (group-struct _ _ _⊙_ _ _ _ _ _)}
              {group G Gset (group-struct _ _ _∙_ _ _ _ _ _)}
              {group H Hset (group-struct _ _ _∘_ _ _ _ _ _)}
              (i , ic) (j , jc) = k , kc
  where
    k : F → H
    k f = j (i f)

    kc : (g0 g1 : F) → k (g0 ⊙ g1) ≡ (k g0) ∘ (k g1)
    kc g0 g1 = j (i (g0 ⊙ g1)) ≡⟨ cong j (ic _ _) ⟩
                j (i g0 ∙ i g1) ≡⟨ jc _ _ ⟩
                j (i g0) ∘ j (i g1) ∎

compIso : ∀ {ℓ} {F G H : Group {ℓ}} (I : Iso F G) (J : Iso G H) → Iso F H
compIso {ℓ} {F} {G} {H}
        (iso F→G G→F fg gf) (iso G→H H→G gh hg ) = iso F→H H→F sec ret
  where
    F→H : morph F H
    F→H = compMorph {ℓ} {F} {G} {H} F→G G→H

    H→F : morph H F
    H→F = compMorph {ℓ} {H} {G} {F} H→G G→F

    open Group

    f→h : F .type → H .type
    f→h = F→H .fst

    f→g : F .type → G .type
    f→g = F→G .fst

    g→h : G .type → H .type
    g→h = G→H .fst

    h→f : H .type → F .type
    h→f = H→F .fst

    h→g : H .type → G .type
    h→g = H→G .fst

    g→f : G .type → F .type
    g→f = G→F .fst

    sec : I.section f→h h→f
    sec h = f→h (h→f h) ≡⟨ cong g→h (fg (h→g h)) ⟩
             g→h (h→g h) ≡⟨ gh _ ⟩
             h ∎

    ret : I.retract f→h h→f
    ret f = h→f (f→h f) ≡⟨ cong g→f (hg (f→g f)) ⟩
             g→f (f→g f) ≡⟨ gf _ ⟩
             f ∎

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


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

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Relation.Nullary using (Dec; yes; no)

import Data.Bool as Bool
import Data.Empty as Empty
import Data.Unit as Unit
import Data.Sum as Sum
import Data.Product as Product
import Data.Nat as ℕ
import Data.Nat.Properties as ℕₚ

open Empty using (⊥)
open Unit using (⊤; tt)
open Sum using (inj₁; inj₂)
open Product using (∃-syntax; _×_; _,_)
open ℕ using (ℕ)

open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.Algebras.Linear where

open Bool using (Bool; true; false) public
pattern zero = false
pattern one = true

data _≔_∙_ : Bool → Bool → Bool → Set where
  skip  : zero ≔ zero ∙ zero
  right : one  ≔ zero ∙ one
  left  : one  ≔ one  ∙ zero

∙-computeʳ : ∀ x y → Dec (∃[ z ] (x ≔ y ∙ z))
∙-computeʳ zero zero = yes (zero , skip)
∙-computeʳ zero one = no λ ()
∙-computeʳ one zero = yes (one , right)
∙-computeʳ one one = yes (zero , left)

∙-unique : ∀ {x' x y z} → x' ≔ y ∙ z → x ≔ y ∙ z → x' ≡ x
∙-unique skip skip = refl
∙-unique right right = refl
∙-unique left left = refl

∙-uniqueˡ : ∀ {x y' y z} → x ≔ y' ∙ z → x ≔ y ∙ z → y' ≡ y
∙-uniqueˡ skip skip = refl
∙-uniqueˡ right right = refl
∙-uniqueˡ left left = refl

∙-idˡ : ∀ {x} → x ≔ zero ∙ x
∙-idˡ {zero} = skip
∙-idˡ {one} = right

∙-comm : ∀ {x y z} → x ≔ y ∙ z → x ≔ z ∙ y
∙-comm skip = skip
∙-comm right = left
∙-comm left = right

∙-assoc : ∀ {x y z u v} → x ≔ y ∙ z → y ≔ u ∙ v → ∃-syntax (λ w → (x ≔ u ∙ w) × (w ≔ v ∙ z))
∙-assoc skip skip = zero , skip , skip
∙-assoc right skip = one , right , right
∙-assoc left right = one , right , left
∙-assoc left left = zero , left , skip

Linear : Algebra Bool
Algebra.1∙ Linear = true
Algebra.0∙ Linear = false
Algebra._≔_∙_ Linear = _≔_∙_
Algebra.∙-computeʳ Linear = ∙-computeʳ
Algebra.∙-unique Linear = ∙-unique
Algebra.∙-uniqueˡ Linear = ∙-uniqueˡ
Algebra.0∙-minˡ Linear skip = refl
Algebra.∙-idˡ Linear = ∙-idˡ
Algebra.∙-comm Linear = ∙-comm
Algebra.∙-assoc Linear = ∙-assoc

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Nat.Order.Recursive where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport

open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as Sum
open import Cubical.Data.Unit

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties

open import Cubical.Induction.WellFounded

open import Cubical.Relation.Nullary

infix 4 _≤_ _<_

_≤_ : ℕ → ℕ → Type₀
zero ≤ _ = Unit
suc m ≤ zero = ⊥
suc m ≤ suc n = m ≤ n

_<_ : ℕ → ℕ → Type₀
m < n = suc m ≤ n

_≤?_ : (m n : ℕ) → Dec (m ≤ n)
zero  ≤? _     = yes tt
suc m ≤? zero  = no λ ()
suc m ≤? suc n = m ≤? n

data Trichotomy (m n : ℕ) : Type₀ where
  lt : m < n → Trichotomy m n
  eq : m ≡ n → Trichotomy m n
  gt : n < m → Trichotomy m n

private
  variable
    ℓ : Level
    R : Type ℓ
    P : ℕ → Type ℓ
    k l m n : ℕ

isProp≤ : isProp (m ≤ n)
isProp≤ {zero} = isPropUnit
isProp≤ {suc m} {zero}  = isProp⊥
isProp≤ {suc m} {suc n} = isProp≤ {m} {n}

≤-k+ : m ≤ n → k + m ≤ k + n
≤-k+ {k = zero}  m≤n = m≤n
≤-k+ {k = suc k} m≤n = ≤-k+ {k = k} m≤n

≤-+k : m ≤ n → m + k ≤ n + k
≤-+k {m} {n} {k} m≤n
  = transport (λ i → +-comm k m i ≤ +-comm k n i) (≤-k+ {m} {n} {k} m≤n)

≤-refl : ∀ m → m ≤ m
≤-refl zero = _
≤-refl (suc m) = ≤-refl m

≤-trans : k ≤ m → m ≤ n → k ≤ n
≤-trans {zero} _ _ = _
≤-trans {suc k} {suc m} {suc n} = ≤-trans {k} {m} {n}

≤-antisym : m ≤ n → n ≤ m → m ≡ n
≤-antisym {zero} {zero} _ _ = refl
≤-antisym {suc m} {suc n} m≤n n≤m = cong suc (≤-antisym m≤n n≤m)

≤-k+-cancel : k + m ≤ k + n → m ≤ n
≤-k+-cancel {k =  zero} m≤n = m≤n
≤-k+-cancel {k = suc k} m≤n = ≤-k+-cancel {k} m≤n

≤-+k-cancel : m + k ≤ n + k → m ≤ n
≤-+k-cancel {m} {k} {n}
  = ≤-k+-cancel {k} {m} {n} ∘ transport λ i → +-comm m k i ≤ +-comm n k i

¬m<m : ¬ m < m
¬m<m {suc m} = ¬m<m {m}

≤0→≡0 : n ≤ 0 → n ≡ 0
≤0→≡0 {zero} _ = refl

¬m+n<m : ¬ m + n < m
¬m+n<m {suc m} = ¬m+n<m {m}

<-weaken : m < n → m ≤ n
<-weaken {zero} _ = _
<-weaken {suc m} {suc n} = <-weaken {m}

<-trans : k < m → m < n → k < n
<-trans {k} {m} {n} k<m m<n
  = ≤-trans {suc k} {m} {n} k<m (<-weaken {m} m<n)

<-asym : m < n → ¬ n < m
<-asym {m} m<n n<m = ¬m<m {m} (<-trans {m} {_} {m} m<n n<m)

<→≢ : n < m → ¬ n ≡ m
<→≢ {n} {m} p q = ¬m<m {m = m} (subst {x = n} (_< m) q p)

Trichotomy-suc : Trichotomy m n → Trichotomy (suc m) (suc n)
Trichotomy-suc (lt m<n) = lt m<n
Trichotomy-suc (eq m≡n) = eq (cong suc m≡n)
Trichotomy-suc (gt n<m) = gt n<m

_≟_ : ∀ m n → Trichotomy m n
zero  ≟ zero = eq refl
zero  ≟ suc n = lt _
suc m ≟ zero = gt _
suc m ≟ suc n = Trichotomy-suc (m ≟ n)

k≤k+n : ∀ k → k ≤ k + n
k≤k+n zero    = _
k≤k+n (suc k) = k≤k+n k

n≤k+n : ∀ n → n ≤ k + n
n≤k+n {k} n = transport (λ i → n ≤ +-comm n k i) (k≤k+n n)

≤-split : m ≤ n → (m < n) ⊎ (m ≡ n)
≤-split {zero} {zero} m≤n = inr refl
≤-split {zero} {suc n} m≤n = inl _
≤-split {suc m} {suc n} m≤n
  = Sum.map (idfun _) (cong suc) (≤-split {m} {n} m≤n)

module WellFounded where
  wf-< : WellFounded _<_
  wf-rec-< : ∀ n → WFRec _<_ (Acc _<_) n

  wf-< n = acc (wf-rec-< n)

  wf-rec-< (suc n) m m≤n with ≤-split {m} {n} m≤n
  ... | inl m<n = wf-rec-< n m m<n
  ... | inr m≡n = subst⁻ (Acc _<_) m≡n (wf-< n)

wf-elim : (∀ n → (∀ m → m < n → P m) → P n) → ∀ n → P n
wf-elim = WFI.induction WellFounded.wf-<

wf-rec : (∀ n → (∀ m → m < n → R) → R) → ℕ → R
wf-rec {R = R} = wf-elim {P = λ _ → R}

module Minimal where
  Least : ∀{ℓ} → (ℕ → Type ℓ) → (ℕ → Type ℓ)
  Least P m = P m × (∀ n → n < m → ¬ P n)

  isPropLeast : (∀ m → isProp (P m)) → ∀ m → isProp (Least P m)
  isPropLeast pP m
    = isPropΣ (pP m) (λ _ → isPropΠ3 λ _ _ _ → isProp⊥)

  Least→ : Σ _ (Least P) → Σ _ P
  Least→ = map-snd fst

  search
    : (∀ m → Dec (P m))
    → ∀ n → (Σ[ m ∈ ℕ ] Least P m) ⊎ (∀ m → m < n → ¬ P m)
  search dec zero = inr (λ _ b _ → b)
  search {P = P} dec (suc n) with search dec n
  ... | inl tup = inl tup
  ... | inr ¬P<n with dec n
  ... | yes Pn = inl (n , Pn , ¬P<n)
  ... | no ¬Pn = inr λ m m≤n
      → case ≤-split m≤n of λ where
          (inl m<n) → ¬P<n m m<n
          (inr m≡n) → subst⁻ (¬_ ∘ P) m≡n ¬Pn

  →Least : (∀ m → Dec (P m)) → Σ _ P → Σ _ (Least P)
  →Least dec (n , Pn) with search dec n
  ... | inl least = least
  ... | inr ¬P<n  = n , Pn , ¬P<n

  Least-unique : ∀ m n → Least P m → Least P n → m ≡ n
  Least-unique m n (Pm , ¬P<m) (Pn , ¬P<n) with m ≟ n
  ... | lt m<n = Empty.rec (¬P<n m m<n Pm)
  ... | eq m≡n = m≡n
  ... | gt n<m = Empty.rec (¬P<m n n<m Pn)

  isPropΣLeast : (∀ m → isProp (P m)) → isProp (Σ _ (Least P))
  isPropΣLeast pP (m , LPm) (n , LPn)
    = ΣPathP λ where
        .fst → Least-unique m n LPm LPn
        .snd → isOfHLevel→isOfHLevelDep 1 (isPropLeast pP)
                LPm LPn (Least-unique m n LPm LPn)

  Decidable→Collapsible
    : (∀ m → isProp (P m)) → (∀ m → Dec (P m)) → Collapsible (Σ ℕ P)
  Decidable→Collapsible pP dP = λ where
    .fst → Least→ ∘ →Least dP
    .snd x y → cong Least→ (isPropΣLeast pP (→Least dP x) (→Least dP y))

open Minimal using (Decidable→Collapsible) public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, May-July 2016, implementing postfix projections

{-# OPTIONS --postfix-projections #-}

open import Common.Product
open import Common.Bool

pair : ∀{A : Set}(a : A) → A × A
pair a = {!!} -- C-c C-c here outputs postfix projections

record BoolFun : Set where
  field out : Bool → Bool
open BoolFun

neg : BoolFun
neg .out x = {!x!} -- splitting here should preserve postfix proj

neg2 : BoolFun
out neg2 x = {!x!} -- splitting here should preserve prefix proj

module ExtendedLambda where

  neg3 : BoolFun
  neg3 = λ{ .out → {!!} }

  pair2 : ∀{A : Set}(a : A) → A × A
  pair2 = λ{ a → {!!} }

  neg4 : BoolFun
  neg4 = λ{ .out b → {!b!} }

-- DOES NOT WORK DUE TO ISSUE #2020

-- module LambdaWhere where

--   neg3 : BoolFun
--   neg3 = λ where
--     .out → {!!} -- splitting on result here crashes

--   pair2 : ∀{A : Set}(a : A) → A × A
--   pair2 = λ where
--     a → {!!}

--   extlam-where : Bool → Bool
--   extlam-where = λ where
--     b → {!b!}

-- -- extlam : Bool → Bool
-- -- extlam = λ
-- --   { b → {!b!}
-- --   }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

open import Issue1278.A Set
open import Agda.Builtin.Equality

test : (c : D) -> (c ≡ c)
test d = {!!} -- goal ".#A-60005532.d ≡ .#A-60005532.d"