text:
module Tactic.Deriving where

open import Prelude hiding (abs)
open import Tactic.Reflection

private
  makeArgs : Nat → List (Arg Nat) → List (Arg Term)
  makeArgs n xs = reverse $ map (fmap (λ i → var (n - i - 1) [])) xs

  computeInstanceType : Name → Nat → List (Arg Nat) → Type → Maybe Term
  computeInstanceType class n xs (agda-sort _) =
    just (def class (vArg (var n (makeArgs n xs)) ∷ []))
  computeInstanceType class n xs (pi a (abs s b)) =
    pi (hArg (unArg a)) ∘ abs s <$> computeInstanceType class (suc n) ((n <$ a) ∷ xs) b
  computeInstanceType _ _ _ _ = nothing

  computeTel : Name → Nat → List (Arg Nat) → Telescope → Telescope → Telescope × List (Arg Term)
  computeTel d n xs is [] = reverse is , makeArgs (n + length is) xs
  computeTel d n xs is (a ∷ tel) =
    first (hArg (unArg a) ∷_) $
    case computeInstanceType d 0 [] (weaken 1 $ unArg a) of λ
    { (just i) → computeTel d (1 + n) ((n <$ a) ∷ xs)
                              (iArg (weaken (length is) i) ∷ weaken 1 is) tel
    ; nothing  → computeTel d (1 + n) ((n <$ a) ∷ xs) (weaken 1 is) tel }

-- Computes the telescope of instances for a given datatype and class. For instance,
-- instanceTelescope (quote Vec) (quote Eq) computes to
-- {a : Level} {A : Set a} {{_ : Eq A}} {n : Nat} , 3 ∷ 2 ∷ 0 ∷ []
instanceTelescope : Name → Name → TC (Telescope × List (Arg Term))
instanceTelescope d class = computeTel class 0 [] [] <$> (fst ∘ telView <$> getType d)

-- Compute the type of an instance declaration for an arbitrary datatype and class.
instanceType : Name → Name → TC Type
instanceType d class =
  caseM instanceTelescope d class of λ
  { (tel , vs) → pure $ telPi tel $ def₁ class (def d vs)
  }

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# OPTIONS --no-termination-check #-}

module oldPi where

open import Data.Nat hiding (_⊔_; suc; _+_; _*_)
open import Data.Vec
open import Data.Empty
open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Product hiding (map)
open import Function
open import Level
open import Relation.Binary.PropositionalEquality hiding (sym)
open import Relation.Binary.Core
open import Algebra
import Algebra.FunctionProperties as FunctionProperties
open import Algebra.FunctionProperties.Core
open import Algebra.Structures

infixr 30 _⟷_
infixr 30 _⟺_
infixr 20 _⊙_
infixr 20 _◎_

------------------------------------------------------------------------------
-- First we define a universe of our value types

data B : Set where
  ZERO  : B
  ONE   : B
  PLUS  : B → B → B
  NEG   : B → B
  TIMES : B → B → B
  RECIP : B → B

⟦_⟧ : B → Set
⟦ ZERO ⟧         = ⊥
⟦ ONE ⟧          = ⊤
⟦ PLUS b1 b2 ⟧   = ⟦ b1 ⟧ ⊎ ⟦ b2 ⟧
⟦ NEG b ⟧        = {!!}
⟦ TIMES b1 b2 ⟧  = ⟦ b1 ⟧ × ⟦ b2 ⟧
⟦ RECIP b ⟧      = {!!}

------------------------------------------------------------------------------
-- Now we define another universe for our equivalences. First the codes for
-- equivalences.

data _⟷_ : B → B → Set where
  unite₊  : { b : B } → PLUS ZERO b ⟷ b
  uniti₊  : { b : B } → b ⟷ PLUS ZERO b
  swap₊   : { b₁ b₂ : B } → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  η₊      : { b : B } → ZERO ⟷ PLUS (NEG b) b
  ε₊      : { b : B } → PLUS b (NEG b) ⟷ ZERO
  refe⋆   : { b : B } → RECIP (RECIP b) ⟷ b
  refi⋆   : { b : B } → b ⟷ RECIP (RECIP b)
  rile⋆   : { b : B } → TIMES b (TIMES b (RECIP b)) ⟷ b
  rili⋆   : { b : B } → b ⟷ TIMES b (TIMES b (RECIP b))
  id⟷   : { b : B } → b ⟷ b
  sym    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)

--

dist' : {b₁ b₂ b₃ : B} → TIMES b₁ (PLUS b₂ b₃) ⟷ PLUS (TIMES b₁ b₂) (TIMES b₁ b₃)
dist' = swap⋆ ◎ dist ◎ (swap⋆ ⊕ swap⋆)

midtofront : {a b c : B} → TIMES a (TIMES b c) ⟷ TIMES b (TIMES a c)
midtofront = assocl⋆ ◎ (swap⋆ ⊗ id⟷) ◎ assocr⋆

------------------------------------------------------------------------------
-- Establish that syntactically we have a commutative semiring

⟷IsEquivalence : IsEquivalence _⟷_
⟷IsEquivalence = record {
    refl = id⟷ ;
    sym = sym  ;
    trans = _◎_
  }

+IsSemigroup : IsSemigroup _⟷_ PLUS
+IsSemigroup = record {
    isEquivalence = ⟷IsEquivalence ;
    assoc = λ x y z → assocr₊ {x} {y} {z} ;
    ∙-cong = _⊕_
  }

+0IsMonoid : IsMonoid _⟷_ PLUS ZERO
+0IsMonoid = record {
    isSemigroup = +IsSemigroup ;
    identity = ((λ x → unite₊ {x}) ,
                (λ x → swap₊ ◎ unite₊ {x}))
  }

+0IsCommutativeMonoid : IsCommutativeMonoid _⟷_ PLUS ZERO
+0IsCommutativeMonoid = record {
    isSemigroup = +IsSemigroup ;
    identityˡ = λ x → unite₊ {x} ;
    comm = λ x y → swap₊ {x} {y}
  }

+0CommutativeMonoid : CommutativeMonoid _ _
+0CommutativeMonoid = record {
  Carrier = B ;
  _≈_ = _⟷_ ;
  _∙_ = PLUS ;
  ε = ZERO ;
  isCommutativeMonoid = +0IsCommutativeMonoid
  }

--

⋆IsSemigroup : IsSemigroup _⟷_ TIMES
⋆IsSemigroup = record {
    isEquivalence = ⟷IsEquivalence ;
    assoc = λ x y z → assocr⋆ {x} {y} {z} ;
    ∙-cong = _⊗_
  }

⋆1IsMonoid : IsMonoid _⟷_ TIMES ONE
⋆1IsMonoid = record {
    isSemigroup = ⋆IsSemigroup ;
    identity = ((λ x → unite⋆ {x}) ,
                (λ x → swap⋆ ◎ unite⋆ {x}))
  }

⋆1IsCommutativeMonoid : IsCommutativeMonoid _⟷_ TIMES ONE
⋆1IsCommutativeMonoid = record {
    isSemigroup = ⋆IsSemigroup ;
    identityˡ = λ x → unite⋆ {x} ;
    comm = λ x y → swap⋆ {x} {y}
  }

⋆1CommutativeMonoid : CommutativeMonoid _ _
⋆1CommutativeMonoid = record {
  Carrier = B ;
  _≈_ = _⟷_ ;
  _∙_ = TIMES ;
  ε = ONE ;
  isCommutativeMonoid = ⋆1IsCommutativeMonoid
  }

record IsCommutativeSemiringWithoutAnnihilatingZero
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (+ * : Op₂ A) (0# 1# : A)
       : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
    *-isCommutativeMonoid : IsCommutativeMonoid ≈ * 1#
    distrib               : * DistributesOver +

record CommutativeSemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    _+_ : Op₂ Carrier
    _*_ : Op₂ Carrier
    0# : Carrier
    1# : Carrier
    isCommutativeSemiringWithoutAnnihilatingZero :
      IsCommutativeSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#

B-isCommutativeSemiringWithoutAnnihilatingZero
    : IsCommutativeSemiringWithoutAnnihilatingZero _⟷_ PLUS TIMES ZERO ONE
B-isCommutativeSemiringWithoutAnnihilatingZero = record {
    +-isCommutativeMonoid = +0IsCommutativeMonoid ;
    *-isCommutativeMonoid = ⋆1IsCommutativeMonoid ;
    distrib = ( (λ x y z → dist' {x} {y} {z}) ,
                (λ x y z → dist {y} {z} {x} ))
    }

------------------------------------------------------------------------------
-- Now we want to add negatives and fractionals...

-- Define module over a ring (the types bot, top, disjoint union, and product
-- do form a ring as shown in the type-iso library)

module MR (C : CommutativeSemiringWithoutAnnihilatingZero Level.zero Level.zero) where

  open Data.Nat using (ℕ; zero; suc; _*_)
  open Data.Vec using ([]; _∷_; map; _++_)
  open CommutativeSemiringWithoutAnnihilatingZero using (Carrier; _+_)

  R-module : Set → ℕ → Set
  R-module c dim = Vec c dim

{--
  zeroV : ∀ {b : Set} → R-module b 0
  zeroV = []

  tensorV : {b₁ b₂ : Set } {m₁ m₂ : ℕ} →
            R-module b₁ m₁ → R-module b₂ m₂ →
            R-module (b₁ × b₂) (m₁ * m₂)
  tensorV [] _ = []
  tensorV (x ∷ xs) ys = (map (λ y → (x , y)) ys) ++ (tensorV xs ys)
--}

  addV : {n : ℕ} → R-module (Carrier C) n → R-module (Carrier C) n
                 → R-module (Carrier C) n
  addV x y = Data.Vec.zipWith (_+_ C) x y
open MR

--

neg : {b₁ b₂ : B} → (b₁ ⟷ b₂) → (NEG b₁ ⟷ NEG b₂)
neg {b₁} {b₂} c =              -- -b1
  uniti₊ ◎                     -- 0 + (-b1)
  (η₊ {b₂} ⊕ id⟷) ◎           -- (-b2 + b2) + (-b1)
  ((id⟷ ⊕ sym c) ⊕ id⟷) ◎    -- (-b2 + b1) + (-b1)
  assocr₊ ◎                    -- (-b2) + (b1 + (-b1))
  (id⟷ ⊕ ε₊) ◎                -- (-b2) + 0
  swap₊ ◎                      -- 0 + (-b2)
  unite₊                       -- -b2

--

mul0 : {b : B} → TIMES ZERO b ⟷ ZERO
mul0 =                    -- 0*b
  uniti₊ ◎                  --  0 + 0*b
  (η₊ ⊕ id⟷) ◎        -- (-(0*b) + 0*b) + 0*b
  assocr₊ ◎              -- -(0*b) + (0*b + 0*b)
  (id⟷ ⊕ factor) ◎  -- -(0*b) + (0+0)*b
  (id⟷ ⊕ (unite₊ ⊗ id⟷)) ◎  -- -(0*b) + 0*b
  swap₊ ◎  ε₊ -- 0

inv0 : TIMES ZERO (RECIP ZERO) ⟷ ZERO
inv0 = mul0

--

recip : {b₁ b₂ : B} → (b₁ ⟷ b₂) → (RECIP b₁ ⟷ RECIP b₂)
recip {b₁} {b₂} c =          -- 1/a
  rili⋆ {RECIP b₁} ◎         -- 1/a * (1/a * 1/1/a)
  (id⟷ ⊗ (id⟷ ⊗ refe⋆)) ◎   -- 1/a * (1/a * a)
  assocl⋆ ◎                  -- (1/a * 1/a) * a
  (id⟷ ⊗ reciplem c) ◎     -- (1/a * 1/a) * (a * ((a * 1/b) * (b * 1/b)))
  assocl⋆ ◎                  -- (((1/a * 1/a) * a) * ((a * 1/b) * (b * 1/b)))
  ((id⟷ ⊗ refi⋆ ) ⊗ id⟷) ◎   -- (((1/a *1/a) * 1/(1/a)) * ((a * 1/b) * (b * 1/b))
  ((assocr⋆ ◎ rile⋆ ) ⊗ (id⟷ ⊗ ((sym c) ⊗ id⟷))) ◎ -- 1/a * ((a * 1/b) * (a * 1/b))
  (id⟷ ⊗ (assocr⋆ ◎ (id⟷ ⊗ midtofront))) ◎ -- 1/a * (a * (a * (1/b * 1/b)))
  (assocl⋆ ◎ assocl⋆) ◎                      -- ((1/a * a) * a) * (1/b * 1/b)
  (((swap⋆ ⊗ id⟷) ◎ swap⋆) ⊗ id⟷) ◎         -- ((a * (a * 1/a)) * (1/b * 1/b))
  (rile⋆ ⊗ id⟷ ) ◎                           -- a * (1/b * 1/b)
  ((c ◎ refi⋆ ) ⊗ id⟷) ◎ swap⋆ ◎             -- (1/b * 1/b) * 1/(1/b)
  assocr⋆ ◎ rile⋆                             -- 1/b
  where
    reciplem : {b₁ b₂ : B} → (b₁ ⟷ b₂) → (b₁ ⟷ (TIMES b₁ (TIMES (TIMES b₁ (RECIP b₂)) (TIMES b₂ (RECIP b₂)))))
    reciplem {b₁} {b₂} c =  c ◎                       -- b
      rili⋆ ◎                                -- b * (b * 1/b)
      (rili⋆ ⊗ id⟷) ◎                        -- (b * (b * 1/b)) * (b * 1/b)
      (((sym c) ⊗ ((sym c) ⊗ id⟷)) ⊗ id⟷) ◎ -- ((a * (a * 1/b)) * (b * 1/b))
      assocr⋆                                -- a * ((a * 1/b) * (b * 1/b))

--

adjoint : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
adjoint unite₊    = uniti₊
adjoint uniti₊    = unite₊
adjoint swap₊     = swap₊
adjoint assocl₊   = assocr₊
adjoint assocr₊   = assocl₊
adjoint unite⋆    = uniti⋆
adjoint uniti⋆    = unite⋆
adjoint swap⋆     = swap⋆
adjoint assocl⋆   = assocr⋆
adjoint assocr⋆   = assocl⋆
adjoint dist      = factor
adjoint factor    = dist
adjoint η₊        = swap₊ ◎ ε₊
adjoint ε₊        = η₊ ◎ swap₊
adjoint refe⋆     = refi⋆
adjoint refi⋆     = refe⋆
adjoint rile⋆     = rili⋆
adjoint rili⋆     = rile⋆
adjoint id⟷      = id⟷
adjoint (sym c)   = c
adjoint (c₁ ◎ c₂) = adjoint c₂ ◎ adjoint c₁
adjoint (c₁ ⊕ c₂) = adjoint c₁ ⊕ adjoint c₂
adjoint (c₁ ⊗ c₂) = adjoint c₁ ⊗ adjoint c₂

eval  :{ b₁ b₂ : B } → (b₁ ⟷ b₂) → ⟦ b₁ ⟧ → ⟦ b₂ ⟧
eval unite₊ (inj₁ ())
eval unite₊ (inj₂ v) = v
eval uniti₊ v = inj₂ v
eval swap₊ (inj₁ v) = inj₂ v
eval swap₊ (inj₂ v) = inj₁ v
eval assocl₊ (inj₁ v) = inj₁ (inj₁ v)
eval assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
eval assocl₊ (inj₂ (inj₂ v)) = inj₂ v
eval assocr₊ (inj₁ (inj₁ v)) = inj₁ v
eval assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
eval assocr₊ (inj₂ v) = inj₂ (inj₂ v)
eval unite⋆ (tt , v) = v
eval uniti⋆ v = (tt , v)
eval swap⋆ (v₁ , v₂) = (v₂ , v₁)
eval assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
eval assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
eval dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
eval dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
eval factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
eval factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
eval η₊ ()
eval ε₊ (inj₁ x) = {!!}
eval ε₊ (inj₂ y) = {!!}
eval refe⋆ v = {!!}
eval refi⋆ v = {!!}
eval rile⋆ v = {!!}
eval rili⋆ v = {!!}
eval id⟷ v = v
eval (sym c) v = eval (adjoint c) v
eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₁ v) = inj₁ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₂ v) = inj₂ (eval c₂ v)
eval (c₁ ⊗ c₂) (v₁ , v₂) = (eval c₁ v₁ , eval c₂ v₂)

------------------------------------------------------------------------------
-- Define the alternative semantics based on small-step semantics

--

+0-IsGroup : IsGroup _⟷_ PLUS ZERO NEG
+0-IsGroup = record {
  isMonoid = +0IsMonoid ;
  inverse = ( (λ x → swap₊ ◎ ε₊ {x}) ,
              (λ x → ε₊ {x}) );
  ⁻¹-cong = neg
  }

+0-IsAbelianGroup : IsAbelianGroup _⟷_ PLUS ZERO NEG
+0-IsAbelianGroup = record {
    isGroup = +0-IsGroup ;
    comm = λ x y → swap₊ {x} {y}
  }

B-IsRing : IsRing _⟷_ PLUS TIMES NEG ZERO ONE
B-IsRing = record {
    +-isAbelianGroup = +0-IsAbelianGroup ;
    *-isMonoid = ⋆1IsMonoid ;
    distrib = ( (λ x y z → dist' {x} {y} {z}) ,
                (λ x y z → dist {y} {z} {x} ))
  }

B-IsCommutativeRing : IsCommutativeRing _⟷_ PLUS TIMES NEG ZERO ONE
B-IsCommutativeRing = record {
    isRing = B-IsRing ;
    *-comm = λ x y → swap⋆ {x} {y}
  }

--

B-CommutativeRing : CommutativeRing _ _
B-CommutativeRing = record {
    Carrier = B ;
    _≈_ = _⟷_ ;
    _+_ = PLUS ;
    _*_ = TIMES ;
    -_ = NEG ;
    0# = ZERO ;
    1# = ONE ;
    isCommutativeRing = B-IsCommutativeRing
  }

--

record IsMeadow
         {a ℓ} {A : Set a} (≈ : Rel A ℓ)
         (+ * : Op₂ A) (- r : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  open FunctionProperties ≈
  field
    +*-isCommutativeRing : IsCommutativeRing ≈ + * - 0# 1#
    *-refl-l : ∀ x → ≈ (r (r x)) x
    *-refl-r : ∀ x → ≈ x (r (r x))
    *-ril-l : ∀ x → ≈ (* x (* x (r x))) x
    *-ril-r : ∀ x → ≈ x (* x (* x (r x)))
    r-cong : ∀ x y → ≈ x y → ≈ (r x) (r y)

record Meadow c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    _+_ : Op₂ Carrier
    _*_ : Op₂ Carrier
    -_ : Op₁ Carrier
    r  : Op₁ Carrier
    0# : Carrier
    1# : Carrier
    isMeadow : IsMeadow _≈_ _+_ _*_ -_ r 0# 1#

B-/IsMeadow : IsMeadow _⟷_ PLUS TIMES NEG RECIP ZERO ONE
B-/IsMeadow = record {
    +*-isCommutativeRing = B-IsCommutativeRing ;
    *-refl-l = λ x → refe⋆ {x} ;
    *-refl-r = λ x → sym (refe⋆ {x}) ;
    *-ril-l = λ x → sym (rili⋆ {x}) ;
    *-ril-r = λ x → rili⋆ {x} ;
    r-cong = λ x y → recip {x} {y}
  }

B-/Meadow : Meadow _ _
B-/Meadow = record {
    Carrier = B ;
    _≈_ = _⟷_ ;
    _+_ = PLUS ;
    _*_ = TIMES ;
    -_ = NEG ;
    r  = RECIP ;
    0# = ZERO ;
    1# = ONE ;
    isMeadow = B-/IsMeadow
  }

------------------------------------------------------------------------------
-- NOW WE DEFINE THE SEMANTIC NOTION OF EQUIVALENCE

record _⟺_ (b₁ b₂ : B) : Set where
  constructor equiv
  field
    f₁₂ : ⟦ b₁ ⟧ → ⟦ b₂ ⟧
    f₂₁ : ⟦ b₂ ⟧ → ⟦ b₁ ⟧
    p₁  : ∀ { x : ⟦ b₁ ⟧ } → f₂₁ (f₁₂ x) ≡ x
    p₂  : ∀ { x : ⟦ b₂ ⟧ } → f₁₂ (f₂₁ x) ≡ x

open _⟺_ public

lem-⟺-inv : ∀{A B C : Set }(g₁₂ : A → B )(g₂₁ : B → A)
  (g₂₃ : B → C)(g₃₂ : C → B) →
     (∀ {x : B } → g₁₂ (g₂₁ x) ≡ x) → ({y : C } → g₂₃ (g₃₂ y) ≡ y ) →
     (∀ {z} → g₂₃ (g₁₂ (g₂₁ (g₃₂ z))) ≡ z)
lem-⟺-inv g₁₂ g₂₁ g₂₃ g₃₂ p₁ p₂ {z = z} = trans p p₂
  where w = g₁₂ (g₂₁ (g₃₂ z))
        p = cong g₂₃ {w} p₁

_⊙_ : {b₁ b₂ b₃ : B} → b₁ ⟺ b₂ → b₂ ⟺ b₃ → b₁ ⟺ b₃
r ⊙ s = equiv (λ x → f₁₂ s ( f₁₂ r x)) (λ x → f₂₁ r ( f₂₁ s x))
              (lem-⟺-inv (f₂₁ s) (f₁₂ s) (f₂₁ r) (f₁₂ r) (p₁ s) (p₁ r))
              (lem-⟺-inv (f₁₂ r) (f₂₁ r) (f₁₂ s) (f₂₁ s) (p₂ r) (p₂ s))

-- THESE ARE NEEDED MULTIPLE TIMES, FACTOR OUT

zeroe : {A : Set} → ⊥ ⊎ A → A
zeroe (inj₁ ())
zeroe (inj₂ V) = V

zeroi : {A : Set} → A → ⊥ ⊎ A
zeroi v = inj₂ v

zeroeip : { A : Set } { x : ⊥ ⊎ A } → zeroi (zeroe x) ≡ x
zeroeip { x = inj₁ () }
zeroeip { x = inj₂ v } = refl

sw : {A₁ A₂ : Set} → A₁ ⊎ A₂ → A₂ ⊎ A₁
sw (inj₁ v) = inj₂ v
sw (inj₂ v) = inj₁ v

swp : { A₁ A₂ : Set } → { x : A₁ ⊎ A₂ } → sw (sw x) ≡ x
swp { x = inj₁ v } = refl
swp { x = inj₂ v } = refl

-- And finally we map each code to an actual equivalence

iso : { b₁ b₂ : B } → b₁ ⟷ b₂ → b₁ ⟺ b₂
iso id⟷ = equiv id id refl refl
iso (f ◎ g) = (iso f) ⊙ (iso g)
iso unite₊ = equiv zeroe zeroi zeroeip refl
iso swap₊ = equiv sw sw swp swp
iso _ = {!!}

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

BOOL : B
BOOL = PLUS ONE ONE

BOOL² : B
BOOL² = TIMES BOOL BOOL

BOOL³ : B
BOOL³ = TIMES BOOL BOOL²

unitπ : ⟦ ONE ⟧
unitπ = tt

trueπ : ⟦ BOOL ⟧
trueπ = inj₁ tt

falseπ : ⟦ BOOL ⟧
falseπ = inj₂ tt

e0 : ⟦ BOOL² ⟧
e0 = (falseπ , falseπ)

e1 : ⟦ BOOL² ⟧
e1 = (falseπ , trueπ)

e2 : ⟦ BOOL² ⟧
e2 = (trueπ , falseπ)

e3 : ⟦ BOOL² ⟧
e3 = (trueπ , trueπ)

notπ : BOOL ⟷ BOOL
notπ = swap₊

ifc : { b : B } → (b ⟷ b) → (TIMES BOOL b ⟷ TIMES BOOL b)
ifc c = dist ◎ ((id⟷ ⊗ c) ⊕ id⟷) ◎ factor

cnot : BOOL² ⟷ BOOL²
cnot = ifc notπ

toffoli : BOOL³ ⟷ BOOL³
toffoli = ifc cnot

test1 : ⟦ BOOL³ ⟧
test1 = eval toffoli (trueπ , (trueπ , trueπ))

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

ext: agda

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
postulate
  A : Set
  a : A

record B : Set where
  constructor i
  field b : A
open B

data D : (X : Set) → X → Set where
  c : D B (record { b = a })

accepted : (X : Set) (x : X) → D X x → Set
accepted .B (i a) c = A

rejected : (X : Set) (x : X) → D X x → Set
rejected .B (record { b = a }) c = A

-- WAS:
-- I'm not sure if there should be a case for the constructor c,
-- because I get stuck when trying to solve the following unification
-- problems (inferred index ≟ expected index):
--   B ≟ X
--   record { b = a } ≟ x
-- when checking that the pattern c has type D X x

-- SHOULD: succeed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module SystemF.Syntax.Type where

open import Prelude
open import Data.Fin hiding (lift)
open import Data.Fin.Substitution
open import Extensions.Substitution
open import Data.Star using (Star; ε; _◅_)

infixl 10 _→'_
data Type (ν : ℕ) : Set where
  tc   : ℕ → Type ν
  tvar : (n : Fin ν) → Type ν
  _→'_ : Type ν → Type ν → Type ν
  _⟶_ : Type ν → Type ν → Type ν
  ∀'   : Type (suc ν) → Type ν

data Base {ν} : (Type ν) → Set where
  tc   : ∀ n → Base (tc n)
  tvar : ∀ n → Base (tvar n)
  _⟶_ : ∀ a b → Base (a ⟶ b)

module Functions where

  -- proposition that states that the given polytype
  -- is a (possibly polymorphic) function
  data IsFunction {ν : ℕ} : Type ν → Set where
    lambda : (a b : Type ν) → IsFunction (a →' b)
    ∀'-lambda : ∀ {f} → IsFunction f → IsFunction (∀' f)

  -- decision procedure for IsFunction
  is-function : ∀ {ν} → (a : Type ν) → Dec (IsFunction a)
  is-function (tc c) = no (λ ())
  is-function (tvar n) = no (λ ())
  is-function (a →' b) = yes (lambda a b)
  is-function (a ⟶ b) = no (λ ())
  is-function (∀' a) with is-function a
  is-function (∀' a) | yes a-is-f = yes $ ∀'-lambda a-is-f
  is-function (∀' a) | no a-not-f = no (λ{ (∀'-lambda a-is-f) → a-not-f a-is-f })

  domain : ∀ {ν} {f : Type ν} → IsFunction f → Type ν
  domain (lambda a b) = a
  domain (∀'-lambda f) = ∀' (domain f)

  codomain : ∀ {ν} {f : Type ν} → IsFunction f → Type ν
  codomain (lambda a b) = b
  codomain (∀'-lambda f) = ∀' (codomain f)

open Functions public


text:
module NoQualifiedInstances.Import.A where

record I : Set where

instance
  postulate i : I

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Categories
open import Monads

module Monads.EM.Adjunction {a b}{C : Cat {a}{b}}(M : Monad C) where

open import Library

open import Functors
open import Adjunctions
open import Monads.EM M
open import Monads.EM.Functors M

open Cat C
open Fun
open Monad M
open Adj
open Alg
open AlgMorph

EMAdj : Adj C EM
EMAdj  = record {
  L = EML;
  R = EMR;
  left = λ f → comp (amor f) η;
  right = λ {X}{Y} f →
    record{amor = astr Y X f;
           ahom = λ {Z}{g} →
             proof
             comp (astr Y X f) (astr (OMap EML X) Z g)
             ≅⟨ sym (alaw2 Y) ⟩
             astr Y Z (comp (astr Y X f) g)
             ∎};
  lawa = λ {X}{Y}(f : AlgMorph (OMap EML X) Y) → AlgMorphEq (
    proof
    astr Y X (comp (amor f) η)
    ≅⟨ sym (ahom f) ⟩
    comp (amor f) (astr (OMap EML X) X η)
    ≡⟨⟩
    comp (amor f) (bind η)
    ≅⟨ cong (comp (amor f)) law1 ⟩
    comp (amor f) iden
    ≅⟨ idr ⟩
    amor f
    ∎);
  lawb = λ {X}{Y} f →
    proof
    comp (astr Y X f) η
    ≅⟨ sym (alaw1 Y) ⟩
    f
    ∎;
  natleft = λ{X}{X'}{Y}{Y'} f g h →
    proof
    comp (amor g) (comp (comp (amor h) η) f)
    ≅⟨ cong (comp (amor g)) ass ⟩
    comp (amor g) (comp (amor h) (comp η f))
    ≅⟨ cong (comp (amor g) ∘ comp (amor h)) (sym law2) ⟩
    comp (amor g) (comp (amor h) (comp (bind (comp η f)) η))
    ≅⟨ cong (comp (amor g)) (sym ass) ⟩
    comp (amor g) (comp (comp (amor h) (bind (comp η f))) η)
    ≅⟨ sym ass ⟩
    comp (comp (amor g) (comp (amor h) (bind (comp η f)))) η
    ∎;
  natright = λ{X}{X'}{Y}{Y'} f g h → AlgMorphEq (
    proof
    astr Y' X' (comp (amor g) (comp h f))
    ≅⟨ sym (ahom g) ⟩
    comp (amor g) (astr Y X' (comp h f))
    ≅⟨ cong (λ h → comp (amor g) (astr Y X' (comp h f))) (alaw1 Y) ⟩
    comp (amor g) (astr Y X' (comp (comp (astr Y X h) η) f))
    ≅⟨ cong (comp (amor g) ∘ astr Y X') ass ⟩
    comp (amor g) (astr Y X' (comp (astr Y X h) (comp η f)))
    ≅⟨ cong (comp (amor g)) (alaw2 Y) ⟩
    comp (amor g) (comp (astr Y X h) (bind (comp η f)))
    ∎)}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


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

{-
  Extremal Mono and Epimorphisms.

  https://ncatlab.org/nlab/show/extremal+epimorphism
-}

open import Categories.Category.Core

module Categories.Morphism.Extremal {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Categories.Morphism 𝒞

open Category 𝒞

IsExtremalEpi : ∀ {A B} {f : A ⇒ B} → Epi f → Set (o ⊔ ℓ ⊔ e)
IsExtremalEpi {A = A} {B = B} {f = f} epi =
  ∀ {X} {i : X ⇒ B} {g : A ⇒ X} → Mono i → f ≈ i ∘ g → IsIso i

IsExtremalMono : ∀ {A B} {f : A ⇒ B} → Mono f → Set (o ⊔ ℓ ⊔ e)
IsExtremalMono {A = A} {B = B} {f = f} mono =
  ∀ {X} {g : X ⇒ B} {i : A ⇒ X} → Epi i → f ≈ g ∘ i → IsIso i

record ExtremalEpi {A B} (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    epi : Epi f
    extremal : IsExtremalEpi epi

record ExtremalMono {A B} (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    mono : Mono f
    extremal : IsExtremalMono mono

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Homotopy.Loopspace where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.Truncation hiding (elim2)

{- loop space of a pointed type -}
Ω : {ℓ : Level} → Pointed ℓ → Pointed ℓ
Ω (_ , a) = ((a ≡ a) , refl)

{- n-fold loop space of a pointed type -}
Ω^_ : ∀ {ℓ} → ℕ → Pointed ℓ → Pointed ℓ
(Ω^ 0) p = p
(Ω^ (suc n)) p = Ω ((Ω^ n) p)

{- homotopy Group -}
π : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → Type ℓ
π n A = ∥ typ ((Ω^ n) A) ∥ 2

{- loop space map -}
Ω→ : ∀ {ℓA ℓB} {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → (Ω A →∙ Ω B)
Ω→ (f , f∙) = (λ p → (sym f∙ ∙ cong f p) ∙ f∙) , cong (λ q → q ∙ f∙) (sym (rUnit (sym f∙))) ∙ lCancel f∙

Eckmann-Hilton : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (α β : typ ((Ω^ (2 + n)) A))
              → α ∙ β ≡ β ∙ α
Eckmann-Hilton {A = A} n α β i =
  comp (λ k → rUnit (snd ((Ω^ (1 + n)) A)) (~ k) ≡ rUnit (snd ((Ω^ (1 + n)) A)) (~ k)) -- note : rUnit refl := lUnit refl
       (λ k → λ { (i = i0) → (cong (λ x → rUnit x (~ k)) α) ∙ cong (λ x → lUnit x (~ k)) β
               ;  (i = i1) → (cong (λ x → lUnit x (~ k)) β) ∙ cong (λ x → rUnit x (~ k)) α})
       ((λ j → α (j ∧ ~ i) ∙ β (j ∧ i)) ∙ λ j → α (~ i ∨ j) ∙ β (i ∨ j))

{- Homotopy group version -}
π-comp : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → ∥ typ ((Ω^ (suc n)) A) ∥₂
      → ∥ typ ((Ω^ (suc n)) A) ∥₂ → ∥ typ ((Ω^ (suc n)) A) ∥₂
π-comp n = elim2 (λ _ _ → setTruncIsSet) λ p q → ∣ p ∙ q ∣₂

Eckmann-Hilton-π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p q : ∥ typ ((Ω^ (2 + n)) A) ∥₂)
               → π-comp (1 + n) p q ≡ π-comp (1 + n) q p
Eckmann-Hilton-π  n = elim2 (λ x y → isOfHLevelPath 2 setTruncIsSet _ _)
                             λ p q → cong ∣_∣₂ (Eckmann-Hilton n p q)

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
open import Mockingbird.Forest using (Forest)

-- A Gallery of Sage Birds
module Mockingbird.Problems.Chapter13 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Function using (_$_)
open import Data.Product using (proj₂)

open import Mockingbird.Forest.Birds forest
import Mockingbird.Problems.Chapter09 forest as Chapter₉
import Mockingbird.Problems.Chapter10 forest as Chapter₁₀
import Mockingbird.Problems.Chapter11 forest as Chapter₁₁
import Mockingbird.Problems.Chapter12 forest as Chapter₁₂

open Forest forest

problem₁ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasRobin ⦄ → HasSageBird
problem₁ = record
  { Θ = B ∙ M ∙ (R ∙ M ∙ B)
  ; isSageBird = λ x → begin
      x ∙ (B ∙ M ∙ (R ∙ M ∙ B) ∙ x)  ≈⟨ congˡ lemma ⟩
      x ∙ (M ∙ (B ∙ x ∙ M))          ≈⟨ isFond ⟩
      M ∙ (B ∙ x ∙ M)                ≈˘⟨ lemma ⟩
      B ∙ M ∙ (R ∙ M ∙ B) ∙ x        ∎
  } where
  isFond = λ {x} → proj₂ (Chapter₁₁.problem₂ x)

  lemma : ∀ {x} → B ∙ M ∙ (R ∙ M ∙ B) ∙ x ≈ M ∙ (B ∙ x ∙ M)
  lemma {x} = begin
    B ∙ M ∙ (R ∙ M ∙ B) ∙ x  ≈⟨ isBluebird M (R ∙ M ∙ B) x ⟩
    M ∙ (R ∙ M ∙ B ∙ x)      ≈⟨ congˡ $ isRobin M B x ⟩
    M ∙ (B ∙ x ∙ M)          ∎

problem₂ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasCardinal ⦄ → HasSageBird
problem₂ = record
  { Θ = B ∙ M ∙ (C ∙ B ∙ M)
  ; isSageBird = λ x → begin
      x ∙ (B ∙ M ∙ (C ∙ B ∙ M) ∙ x)  ≈⟨ congˡ lemma ⟩
      x ∙ (M ∙ (B ∙ x ∙ M))          ≈⟨ isFond ⟩
      M ∙ (B ∙ x ∙ M)                ≈˘⟨ lemma ⟩
      B ∙ M ∙ (C ∙ B ∙ M) ∙ x        ∎
  } where
  isFond = λ {x} → proj₂ (Chapter₁₁.problem₂ x)

  lemma : ∀ {x} → B ∙ M ∙ (C ∙ B ∙ M) ∙ x ≈ M ∙ (B ∙ x ∙ M)
  lemma {x} = begin
    B ∙ M ∙ (C ∙ B ∙ M) ∙ x  ≈⟨ isBluebird M (C ∙ B ∙ M) x ⟩
    M ∙ (C ∙ B ∙ M ∙ x)      ≈⟨ congˡ $ isCardinal B M x ⟩
    M ∙ (B ∙ x ∙ M)          ∎

problem₃ : ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasLark ⦄ → HasSageBird
problem₃ = record
  { Θ = B ∙ M ∙ L
  ; isSageBird = isSageBird ⦃ Chapter₁₀.hasSageBird ⦄
  } where instance hasComposition = Chapter₁₁.problem₁

problem₄ : ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasWarbler ⦄ → HasSageBird
problem₄ = record
  { Θ = B ∙ M ∙ (B ∙ W ∙ B)
  ; isSageBird = isSageBird ⦃ problem₃ ⦄
  } where instance hasLark = Chapter₁₂.problem₃

problem₆ : ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasLark ⦄ ⦃ _ : HasWarbler ⦄ → HasSageBird
problem₆ = record
  { Θ = W ∙ (Q ∙ L ∙ (Q ∙ L))
  ; isSageBird = λ x → begin
      x ∙ (W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x)  ≈⟨ congˡ lemma ⟩
      x ∙ (L ∙ x ∙ (L ∙ x))            ≈⟨ isFond ⟩
      L ∙ x ∙ (L ∙ x)                  ≈˘⟨ lemma ⟩
      W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x        ∎
  } where
  isFond = λ {x} → proj₂ (Chapter₉.problem₂₅ x)

  lemma : ∀ {x} → W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x ≈ L ∙ x ∙ (L ∙ x)
  lemma {x} = begin
      W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x  ≈⟨ isWarbler (Q ∙ L ∙ (Q ∙ L)) x ⟩
      Q ∙ L ∙ (Q ∙ L) ∙ x ∙ x    ≈⟨ congʳ $ isQueerBird L (Q ∙ L) x ⟩
      Q ∙ L ∙ (L ∙ x) ∙ x        ≈⟨ isQueerBird L (L ∙ x) x ⟩
      L ∙ x ∙ (L ∙ x)            ∎

problem₅ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasWarbler ⦄ → HasSageBird
problem₅ = problem₆
  where
    instance
      hasQueerBird = Chapter₁₁.problem₃₇′
      hasLark = Chapter₁₂.problem₃

problem₇ = problem₅

problem₈ : ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasQueerBird ⦄ → HasSageBird
problem₈ = record
  { Θ = Q ∙ (Q ∙ M) ∙ M
  ; isSageBird = λ x → sym $ begin
      Q ∙ (Q ∙ M) ∙ M ∙ x        ≈⟨ isQueerBird (Q ∙ M) M x ⟩
      M ∙ (Q ∙ M ∙ x)            ≈⟨ isMockingbird (Q ∙ M ∙ x) ⟩
      Q ∙ M ∙ x ∙ (Q ∙ M ∙ x)    ≈⟨ isQueerBird M x (Q ∙ M ∙ x) ⟩
      x ∙ (M ∙ (Q ∙ M ∙ x))      ≈˘⟨ congˡ $ isQueerBird (Q ∙ M) M x ⟩
      x ∙ (Q ∙ (Q ∙ M) ∙ M ∙ x)  ∎
  }

-- TODO: formalise regularity.

problem₉ : ⦃ _ : HasStarling ⦄ ⦃ _ : HasLark ⦄ → HasSageBird
problem₉ = record
  { Θ = S ∙ L ∙ L
  ; isSageBird = λ x → begin
      x ∙ (S ∙ L ∙ L ∙ x)    ≈⟨ congˡ $ isStarling L L x ⟩
      x ∙ (L ∙ x ∙ (L ∙ x))  ≈⟨ isFond ⟩
      L ∙ x ∙ (L ∙ x)        ≈˘⟨ isStarling L L x ⟩
      S ∙ L ∙ L ∙ x          ∎
  } where
  isFond = λ {x} → proj₂ (Chapter₉.problem₂₅ x)

problem₁₀ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasWarbler ⦄ ⦃ _ : HasStarling ⦄ → HasSageBird
problem₁₀ = record
  { Θ = W ∙ S ∙ (B ∙ W ∙ B)
  ; isSageBird = λ x → begin
      x ∙ (W ∙ S ∙ (B ∙ W ∙ B) ∙ x) ≈⟨⟩
      x ∙ (W ∙ S ∙ L ∙ x)      ≈⟨ congˡ $ congʳ $ isWarbler S L ⟩
      x ∙ (S ∙ L ∙ L ∙ x)      ≈⟨ isSageBird ⦃ problem₉ ⦄ x ⟩
      S ∙ L ∙ L ∙ x            ≈˘⟨ congʳ $ isWarbler S L ⟩
      W ∙ S ∙ L ∙ x            ≈⟨⟩
      W ∙ S ∙ (B ∙ W ∙ B) ∙ x  ∎
  } where instance hasLark = Chapter₁₂.problem₃

problem₁₁ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasThrush ⦄ → HasTuringBird
problem₁₁ = record
  { U = B ∙ (B ∙ W ∙ (C ∙ B)) ∙ M
  ; isTuringBird = λ x y → begin
      B ∙ (B ∙ W ∙ (C ∙ B)) ∙ M ∙ x ∙ y  ≈⟨ congʳ $ isBluebird (B ∙ W ∙ (C ∙ B)) M x ⟩
      B ∙ W ∙ (C ∙ B) ∙ (M ∙ x) ∙ y      ≈⟨ congʳ $ isBluebird W (C ∙ B) (M ∙ x) ⟩
      W ∙ (C ∙ B ∙ (M ∙ x)) ∙ y          ≈⟨ isWarbler (C ∙ B ∙ (M ∙ x)) y ⟩
      C ∙ B ∙ (M ∙ x) ∙ y ∙ y            ≈⟨ congʳ $ isCardinal B (M ∙ x) y ⟩
      B ∙ y ∙ (M ∙ x) ∙ y                ≈⟨ isBluebird y (M ∙ x) y ⟩
      y ∙ (M ∙ x ∙ y)                    ≈⟨ congˡ $ congʳ $ isMockingbird x ⟩
      y ∙ (x ∙ x ∙ y)                    ∎
  } where
  instance
    hasCardinal = Chapter₁₁.problem₂₁′
    hasLark = Chapter₁₂.problem₇

problem₁₂ : ⦃ _ : HasTuringBird ⦄ → HasSageBird
problem₁₂ = record
  { Θ = U ∙ U
  ; isSageBird = λ x → sym $ isTuringBird U x
  }

problem₁₃ : ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasWarbler ⦄ → HasOwl
problem₁₃ = record
  { O = Q ∙ Q ∙ W
  ; isOwl = λ x y → begin
      Q ∙ Q ∙ W ∙ x ∙ y  ≈⟨ congʳ $ isQueerBird Q W x ⟩
      W ∙ (Q ∙ x) ∙ y    ≈⟨ isWarbler (Q ∙ x) y ⟩
      Q ∙ x ∙ y ∙ y      ≈⟨ isQueerBird x y y ⟩
      y ∙ (x ∙ y)        ∎
  }

problem₁₄ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasLark ⦄ → HasTuringBird
problem₁₄ = record
  { U = L ∙ O
  ; isTuringBird = λ x y → begin
      L ∙ O ∙ x ∙ y    ≈⟨ congʳ $ isLark O x ⟩
      O ∙ (x ∙ x) ∙ y  ≈⟨ isOwl (x ∙ x) y ⟩
      y ∙ (x ∙ x ∙ y)  ∎
  }

problem₁₅ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasIdentity ⦄ → HasMockingbird
problem₁₅ = record
  { M = O ∙ I
  ; isMockingbird = λ x → begin
      O ∙ I ∙ x    ≈⟨ isOwl I x ⟩
      x ∙ (I ∙ x)  ≈⟨ congˡ $ isIdentity x ⟩
      x ∙ x        ∎
  }

problem₁₆ : ⦃ _ : HasStarling ⦄ ⦃ _ : HasIdentity ⦄ → HasOwl
problem₁₆ = record
  { O = S ∙ I
  ; isOwl = λ x y → begin
      S ∙ I ∙ x ∙ y    ≈⟨ isStarling I x y ⟩
      I ∙ y ∙ (x ∙ y)  ≈⟨ congʳ $ isIdentity y ⟩
      y ∙ (x ∙ y)      ∎
  }

problem₁₇ : ∀ x y → x IsFondOf y → x IsFondOf x ∙ y
problem₁₇ x y xy≈y = begin
  x ∙ (x ∙ y)  ≈⟨ congˡ xy≈y ⟩
  x ∙ y        ∎

problem₁₈ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → IsSageBird (O ∙ Θ)
problem₁₈ x = begin
  x ∙ (O ∙ Θ ∙ x)    ≈⟨ congˡ $ isOwl Θ x ⟩
  x ∙ (x ∙ (Θ ∙ x))  ≈⟨ isFond ⟩
  x ∙ (Θ ∙ x)        ≈˘⟨ isOwl Θ x ⟩
  O ∙ Θ ∙ x          ∎
  where
    isFond : x IsFondOf (x ∙ (Θ ∙ x))
    isFond = problem₁₇ x (Θ ∙ x) (isSageBird x)

problem₁₉ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → IsSageBird (Θ ∙ O)
problem₁₉ x = sym $ begin
  Θ ∙ O ∙ x        ≈˘⟨ congʳ $ isSageBird O ⟩
  O ∙ (Θ ∙ O) ∙ x  ≈⟨ isOwl (Θ ∙ O) x ⟩
  x ∙ (Θ ∙ O ∙ x)  ∎

problem₂₀ : ⦃ _ : HasOwl ⦄ → ∀ A → O IsFondOf A → IsSageBird A
problem₂₀ A OA≈A x = begin
  x ∙ (A ∙ x)  ≈˘⟨ isOwl A x ⟩
  O ∙ A ∙ x    ≈⟨ congʳ OA≈A ⟩
  A ∙ x        ∎

problem₂₁ : ⦃ _ : HasSageBird ⦄ → ∀ A → IsChoosy A → IsSageBird (Θ ∙ A)
problem₂₁ A isChoosy = isChoosy (Θ ∙ A) $ isSageBird A

open import Mockingbird.Forest.Extensionality forest

problem₂₂ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → O ∙ Θ ≋ Θ
problem₂₂ x = begin
  O ∙ Θ ∙ x    ≈⟨ isOwl Θ x ⟩
  x ∙ (Θ ∙ x)  ≈⟨ isSageBird x ⟩
  Θ ∙ x        ∎

problem₂₃ : ⦃ _ : Extensional ⦄ ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → O IsFondOf Θ
problem₂₃ = ext problem₂₂

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


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

module unions where
  -- values mapped in Γ2 replace those mapped in Γ1
  _∪_ : {A : Set} → A ctx → A ctx → A ctx
  Γ1 ∪ Γ2 = union (λ a b → b) Γ1 Γ2

  -- duplicate mappings are combined by append (_++_)
  _⊎_ : {A : Set} → (List A) ctx → (List A) ctx → (List A) ctx
  Γ1 ⊎ Γ2 = union (λ a b → a ++ b) Γ1 Γ2

  infixl 50 _∪_
  infixl 50 _⊎_

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
open import Data.Word.Primitive public using ( Word8 ; Word16 ; Word32 ; Word64 )

module Data.Word where

data WordSize : Set where
  #8 #16 #32 #64 : WordSize

Word : WordSize → Set
Word #8  = Word8
Word #16 = Word16
Word #32 = Word32
Word #64 = Word64

Byte : Set
Byte = Word8

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
open import Data.Empty using ( ⊥ )
open import FRP.LTL.RSet.Core using ( RSet )

module FRP.LTL.RSet.Empty where

F : RSet
F t = ⊥

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module Issue1760c where

-- Skipping an old-style mutual block: Before the `mutual` keyword.
{-# NO_POSITIVITY_CHECK #-}
mutual
  data D : Set where
    lam : (D → D) → D

  record U : Set where
    field ap : U → U


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Symmetry {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties.Conversion

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  -- Helper function for symmetry of type equality using shape views.
  symEqT : ∀ {Γ A B l l′} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
         → ShapeView Γ l l′ A B [A] [B]
         → Γ ⊩⟨ l  ⟩ A ≡ B / [A]
         → Γ ⊩⟨ l′ ⟩ B ≡ A / [B]
  symEqT (ℕᵥ D D′) A≡B = ιx (ℕ₌ (red D))
  symEqT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ιx (ne₌ M D′ neM K≡M))
         rewrite whrDet* (red D′ , ne neM) (red D₁ , ne neK₁) =
    ιx (ne₌ _ D neK
        (~-sym K≡M))
  symEqT {Γ = Γ} (Πᵥ (Πᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                     (Πᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
         (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , G₁≡G′ = Π-PE-injectivity ΠF₁G₁≡ΠF′G′
        [F₁≡F] : ∀ {Δ} {ρ} [ρ] ⊢Δ → _
        [F₁≡F] {Δ} {ρ} [ρ] ⊢Δ =
          let ρF′≡ρF₁ ρ = PE.cong (wk ρ) (PE.sym F₁≡F′)
              [ρF′] {ρ} [ρ] ⊢Δ = PE.subst (λ x → Δ ⊩⟨ _ ⟩ wk ρ x) F₁≡F′ ([F]₁ [ρ] ⊢Δ)
          in  irrelevanceEq′ {Δ} (ρF′≡ρF₁ ρ)
                             ([ρF′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ)
                             (symEq ([F] [ρ] ⊢Δ) ([ρF′] [ρ] ⊢Δ)
                                    ([F≡F′] [ρ] ⊢Δ))
    in  Π₌ _ _ (red D) (≅-sym (PE.subst (λ x → Γ ⊢ Π F ▹ G ≅ x) (PE.sym ΠF₁G₁≡ΠF′G′) A≡B))
          [F₁≡F]
          (λ {ρ} [ρ] ⊢Δ [a] →
               let ρG′a≡ρG₁′a = PE.cong (λ x → wk (lift ρ) x [ _ ]) (PE.sym G₁≡G′)
                   [ρG′a] = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk (lift ρ) x [ _ ]) G₁≡G′
                                     ([G]₁ [ρ] ⊢Δ [a])
                   [a]₁ = convTerm₁ ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) ([F₁≡F] [ρ] ⊢Δ) [a]
               in  irrelevanceEq′ ρG′a≡ρG₁′a
                                  [ρG′a]
                                  ([G]₁ [ρ] ⊢Δ [a])
                                  (symEq ([G] [ρ] ⊢Δ [a]₁) [ρG′a]
                                         ([G≡G′] [ρ] ⊢Δ [a]₁)))
  symEqT (Uᵥ _ _ _ _ _ _) A≡B = U₌ PE.refl
  symEqT (emb⁰¹ PE.refl x) (ιx A≡B) = symEqT x A≡B
  symEqT (emb¹⁰ PE.refl x) A≡B = ιx (symEqT x A≡B)

  -- Symmetry of type equality.
  symEq : ∀ {Γ A B l l′} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
        → Γ ⊩⟨ l ⟩ A ≡ B / [A]
        → Γ ⊩⟨ l′ ⟩ B ≡ A / [B]
  symEq [A] [B] A≡B = symEqT (goodCases [A] [B] A≡B) A≡B

symNeutralTerm : ∀ {t u A Γ}
               → Γ ⊩neNf t ≡ u ∷ A
               → Γ ⊩neNf u ≡ t ∷ A
symNeutralTerm (neNfₜ₌ neK neM k≡m) = neNfₜ₌ neM neK (~-sym k≡m)

symNatural-prop : ∀ {Γ k k′}
                → [Natural]-prop Γ k k′
                → [Natural]-prop Γ k′ k
symNatural-prop (sucᵣ (ℕₜ₌ k k′ d d′ t≡u prop)) =
  sucᵣ (ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop))
symNatural-prop zeroᵣ = zeroᵣ
symNatural-prop (ne prop) = ne (symNeutralTerm prop)

-- Symmetry of term equality.
symEqTerm : ∀ {l Γ A t u} ([A] : Γ ⊩⟨ l ⟩ A)
          → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
          → Γ ⊩⟨ l ⟩ u ≡ t ∷ A / [A]
symEqTerm (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ₌ A B d d′ typeA typeB A≡B [A] [B] [A≡B]) =
  Uₜ₌ B A d′ d typeB typeA (≅ₜ-sym A≡B) [B] [A] (symEq [A] [B] [A≡B])
symEqTerm (ℕᵣ D) (ιx (ℕₜ₌ k k′ d d′ t≡u prop)) =
  ιx (ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop))
symEqTerm (ne′ K D neK K≡K) (ιx (neₜ₌ k m d d′ nf)) =
  ιx (neₜ₌ m k d′ d (symNeutralTerm nf))
symEqTerm (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  Πₜ₌ g f d′ d funcG funcF (≅ₜ-sym f≡g) [g] [f]
      (λ ρ ⊢Δ [a] → symEqTerm ([G] ρ ⊢Δ [a]) ([f≡g] ρ ⊢Δ [a]))
symEqTerm (emb′ 0<1 x) (ιx t≡u) = ιx (symEqTerm x t≡u)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
{-# OPTIONS --universe-polymorphism #-}
module Prelude.Stream where
-- open import Coinduction
  -- Infinite streams.
open import Prelude.IO
open import Prelude.Nat
open import Prelude.Unit

data Level : Set where
  zero : Level
  suc  : (i : Level) → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

infixl 6 _⊔_

_⊔_ : Level → Level → Level
zero  ⊔ j     = j
suc i ⊔ zero  = suc i
suc i ⊔ suc j = suc (i ⊔ j)

{-# BUILTIN LEVELMAX _⊔_ #-}
infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

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

-- A stream processor SP A B consumes elements of A and produces
-- elements of B. It can only consume a finite number of A’s before
-- producing a B.

data SP (A B : Set) : Set where
  get : (f : A → SP A B) → SP A B
  put : (b : B) (sp : ∞ (SP A B)) → SP A B

-- The function eat is defined by an outer corecursion into Stream B
-- and an inner recursion on SP A B.

eat : ∀ {A B} → SP A B → Stream A → Stream B
eat (get f)    (a ∷ as) = eat (f a) (♭ as)
eat (put b sp) as       = b ∷ ♯ eat (♭ sp) as

-- Composition of stream processors.

_∘_ : ∀ {A B C} → SP B C → SP A B → SP A C
get f₁    ∘ put x sp₂ = f₁ x ∘ ♭ sp₂
put x sp₁ ∘ sp₂       = put x (♯ (♭ sp₁ ∘ sp₂))
sp₁       ∘ get f₂    = get (λ x → sp₁ ∘ f₂ x)

ones : Stream Nat
ones = 1 ∷ (♯ ones)

twos : Stream Nat
twos = 2 ∷ (♯ twos)

printStream : Nat -> Stream Nat -> IO Unit
printStream Z _ = return unit
printStream (S steps) (n ∷ ns) =
    printNat n ,,
    printStream steps (♭ ns)

main : IO Unit
main = printStream 100 twos


text:
-- Andreas, 2011-05-10
module MetaAppUnderLambda where

data _≡_ {A : Set} (a : A) : A -> Set where
  refl : a ≡ a

data D (A : Set) : Set where
  cons : A -> (A -> A) -> D A

f : {A : Set} -> D A -> A
f (cons a h) = a

test : (A : Set) ->
       let X : A
           X = _
           Y : A -> A
           Y = λ v -> _ v
       in  f (cons X Y) ≡ X
test A = refl
-- should return "Unsolved Metas"
-- executes the defauls A.App case in the type checker (which is not covered by appView)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2015-08-26
{-# OPTIONS --rewriting #-} -- Should give error

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

{-# BUILTIN REWRITE _≡_ #-}

lengthMap : {A B : Set} (f : A → B) (xs : List A) →
            length (map f xs) ≡ length xs
lengthMap f [] = refl
lengthMap f (x ∷ xs) rewrite lengthMap f xs = refl

{-# REWRITE lengthMap #-}


text:
open import Oscar.Prelude

module Oscar.Class.Apply where

module _
  (𝔉 : ∀ {𝔣} → Ø 𝔣 → Ø 𝔣)
  𝔬₁ 𝔬₂
  where
  𝓪pply = ∀ {𝔒₁ : Ø 𝔬₁} {𝔒₂ : Ø 𝔬₂} → 𝔉 (𝔒₁ → 𝔒₂) → 𝔉 𝔒₁ → 𝔉 𝔒₂
  record 𝓐pply : Ø ↑̂ (𝔬₁ ∙̂ 𝔬₂) where
    infixl 4 apply
    field apply : 𝓪pply
    syntax apply f x = f <*> x
open 𝓐pply ⦃ … ⦄ public

_<*>_ = apply


text:
open import Coinduction using ( ∞ ; ♯_ ; ♭ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done ; _⟫_ ; ⟦_⟧ ; _≃_ ; equiv )
open import System.IO.Transducers.Session using ( Session ; I ; Σ ; _∼_ ; ∼-refl ; ∼-trans )
open import System.IO.Transducers.Trace using ( Trace ; [] ; _∷_ )
open import System.IO.Transducers.Properties.Lemmas using ( ⟦⟧-resp-∼ ; ≃-refl ; ≃-sym ; IsEquiv ; isEquiv ; ≃-equiv ; ∷-refl-≡₁ ; ∷-refl-≡₂ )

module System.IO.Transducers.Properties.Category where

open Relation.Binary.PropositionalEquality.≡-Reasoning

infixr 6 _⟦⟫⟧_

-- Coinductive equivalence of programs, note that in the
-- case where done has type I ⇒ I, this is syntactic
-- identity.

data _⇒_⊨_≣_ : ∀ S T (P Q : S ⇒ T) → Set₁ where
  inp : ∀ {A V F T P Q} → ∞ (∀ a → ♭ F a ⇒ T ⊨ ♭ P a ≣ ♭ Q a) →
    (Σ {A} V F ⇒ T ⊨ inp P ≣ inp Q)
  out : ∀ {B W G S} b {P Q} → (S ⇒ ♭ G b ⊨ P ≣ Q) →
    (S ⇒ Σ {B} W G ⊨ out b P ≣ out b Q)
  done : ∀ {S} →
    (S ⇒ S ⊨ done ≣ done)
  inp-done : ∀ {A V F P} → ∞ (∀ a → ♭ F a ⇒ Σ V F ⊨ ♭ P a ≣ out a done) →
    (Σ {A} V F ⇒ Σ V F ⊨ inp P ≣ done)
  done-inp : ∀ {A V F P} → ∞ (∀ a → ♭ F a ⇒ Σ V F ⊨ out a done ≣ ♭ P a) →
    (Σ {A} V F ⇒ Σ V F ⊨ done ≣ inp P)

_≣_ : ∀ {S T} (P Q : S ⇒ T) → Set₁
P ≣ Q = _ ⇒ _ ⊨ P ≣ Q

-- Coinductive equivalence implies semantic equivalence

⟦⟧-resp-≣ : ∀ {S T} {P Q : S ⇒ T} → (P ≣ Q) → (⟦ P ⟧ ≃ ⟦ Q ⟧)
⟦⟧-resp-≣ (inp P≣Q) []                   = refl
⟦⟧-resp-≣ (inp P≣Q) (a ∷ as)             = ⟦⟧-resp-≣ (♭ P≣Q a) as
⟦⟧-resp-≣ (out b P≣Q) as                 = cong (_∷_ b) (⟦⟧-resp-≣ P≣Q as)
⟦⟧-resp-≣ done as                        = refl
⟦⟧-resp-≣ (inp-done P≣outadone) []       = refl
⟦⟧-resp-≣ (inp-done P≣outadone) (a ∷ as) = ⟦⟧-resp-≣ (♭ P≣outadone a) as
⟦⟧-resp-≣ (done-inp outadone≣P) []       = refl
⟦⟧-resp-≣ (done-inp outadone≣P) (a ∷ as) = ⟦⟧-resp-≣ (♭ outadone≣P a) as

-- Semantic equivalence implies coinductive equivalence

⟦⟧-refl-≣ : ∀ {S T} (P Q : S ⇒ T) → (⟦ P ⟧ ≃ ⟦ Q ⟧) → (P ≣ Q)
⟦⟧-refl-≣ (inp P)   (inp Q)    P≃Q        = inp (♯ λ a → ⟦⟧-refl-≣ (♭ P a) (♭ Q a) (λ as → P≃Q (a ∷ as)))
⟦⟧-refl-≣ (inp P)   done       P≃Q        = inp-done (♯ λ a → ⟦⟧-refl-≣ (♭ P a) (out a done) (λ as → P≃Q (a ∷ as)))
⟦⟧-refl-≣ (out b P) (out c Q)  P≃Q with ∷-refl-≡₁ refl refl (P≃Q [])
⟦⟧-refl-≣ (out b P) (out .b Q) P≃Q | refl = out b (⟦⟧-refl-≣ P Q (λ as → ∷-refl-≡₂ refl refl (P≃Q as)))
⟦⟧-refl-≣ done      (inp Q)    P≃Q        = done-inp (♯ λ a → ⟦⟧-refl-≣ (out a done) (♭ Q a) (λ as → P≃Q (a ∷ as)))
⟦⟧-refl-≣ done      done       P≃Q        = done
⟦⟧-refl-≣ (inp P)   (out b Q)  P≃Q with P≃Q []
⟦⟧-refl-≣ (inp P)   (out b Q)  P≃Q | ()
⟦⟧-refl-≣ (out b P) (inp Q)    P≃Q with P≃Q []
⟦⟧-refl-≣ (out b P) (inp Q)    P≃Q | ()
⟦⟧-refl-≣ (out b P) done       P≃Q with P≃Q []
⟦⟧-refl-≣ (out b P) done       P≃Q | ()
⟦⟧-refl-≣ done      (out b Q)  P≃Q with P≃Q []
⟦⟧-refl-≣ done      (out b Q)  P≃Q | ()

-- Trace semantics of identity

⟦done⟧ : ∀ {S} → (Trace S)  → (Trace S)
⟦done⟧ as = as

done-semantics : ∀ {S} → ⟦ done {S} ⟧ ≃ ⟦done⟧
done-semantics as = refl

-- Trace semantics of composition

_⟦⟫⟧_ : ∀ {S T U} →
  (f : Trace S → Trace T) → (g : Trace T → Trace U) →
    (Trace S) → (Trace U)
(f ⟦⟫⟧ g) as = g (f as)

⟫-semantics : ∀ {S T U} (P : S ⇒ T) (Q : T ⇒ U) →
    (⟦ P ⟫ Q ⟧ ≃ ⟦ P ⟧ ⟦⟫⟧ ⟦ Q ⟧)
⟫-semantics (inp P)   (inp Q)   []       = refl
⟫-semantics (inp P)   (inp Q)   (a ∷ as) = ⟫-semantics (♭ P a) (inp Q) as
⟫-semantics (inp P)   (out c Q) as       = cong (_∷_ c) (⟫-semantics (inp P) Q as)
⟫-semantics (inp P)   done      as       = refl
⟫-semantics (out b P) (inp Q)   as       = ⟫-semantics P (♭ Q b) as
⟫-semantics (out b P) (out c Q) as       = cong (_∷_ c) (⟫-semantics (out b P) Q as)
⟫-semantics (out b P) done      as       = refl
⟫-semantics done      Q         as       = refl

⟫-≃-⟦⟫⟧ : ∀ {S T U}
  {P : S ⇒ T} {f : Trace S → Trace T} {Q : T ⇒ U} {g : Trace T → Trace U} →
    (⟦ P ⟧ ≃ f) → (⟦ Q ⟧ ≃ g) → (⟦ P ⟫ Q ⟧ ≃ f ⟦⟫⟧ g)
⟫-≃-⟦⟫⟧ {S} {T} {U} {P} {f} {Q} {g} P≃f Q≃g as =
  begin
    ⟦ P ⟫ Q ⟧ as
  ≡⟨ ⟫-semantics P Q as ⟩
    ⟦ Q ⟧ (⟦ P ⟧ as)
  ≡⟨ cong ⟦ Q ⟧ (P≃f as) ⟩
    ⟦ Q ⟧ (f as)
  ≡⟨ Q≃g (f as) ⟩
    g (f as)
  ∎

-- Composition respects ≃

⟫-resp-≃ : ∀ {S T U} {P₁ P₂ : S ⇒ T} {Q₁ Q₂ : T ⇒ U} →
  (⟦ P₁ ⟧ ≃ ⟦ P₂ ⟧) → (⟦ Q₁ ⟧ ≃ ⟦ Q₂ ⟧) →
    (⟦ P₁ ⟫ Q₁ ⟧ ≃ ⟦ P₂ ⟫ Q₂ ⟧)
⟫-resp-≃ {S} {T} {U} {P₁} {P₂} {Q₁} {Q₂} P₁≃P₂ Q₁≃Q₂ as =
  begin
    ⟦ P₁ ⟫ Q₁ ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ P₁≃P₂ Q₁≃Q₂ as ⟩
    (⟦ P₂ ⟧ ⟦⟫⟧ ⟦ Q₂ ⟧) as
  ≡⟨ sym (⟫-semantics P₂ Q₂ as) ⟩
    ⟦ P₂ ⟫ Q₂ ⟧ as
  ∎

-- Left identity of composition

⟫-identity₁ : ∀ {S T} (P : S ⇒ T) → ⟦ done ⟫ P ⟧ ≃ ⟦ P ⟧
⟫-identity₁ P = ⟫-semantics done P

-- Right identity of composition

⟫-identity₂ : ∀ {S T} (P : S ⇒ T) → ⟦ P ⟫ done ⟧ ≃ ⟦ P ⟧
⟫-identity₂ P = ⟫-semantics P done

-- Associativity of composition

⟫-assoc : ∀ {S T U V} (P : S ⇒ T) (Q : T ⇒ U) (R : U ⇒ V) →
    ⟦ (P ⟫ Q) ⟫ R ⟧ ≃ ⟦ P ⟫ (Q ⟫ R) ⟧
⟫-assoc P Q R as =
  begin
    ⟦ (P ⟫ Q) ⟫ R ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ (⟫-semantics P Q) ≃-refl as ⟩
    (⟦ P ⟧ ⟦⟫⟧ ⟦ Q ⟧ ⟦⟫⟧ ⟦ R ⟧) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ ≃-refl (⟫-semantics Q R) as) ⟩
    ⟦ P ⟫ (Q ⟫ R) ⟧ as
  ∎

-- Identity is an equivalence

equiv-resp-done : ∀ {S} → ⟦ done ⟧ ≃ ⟦ equiv (∼-refl {S}) ⟧
equiv-resp-done {I}     as = refl
equiv-resp-done {Σ V F} [] = refl
equiv-resp-done {Σ V F} (a ∷ as) = cong (_∷_ a) (equiv-resp-done as)

done-isEquiv : ∀ {S} → IsEquiv (done {S})
done-isEquiv = isEquiv {P = done} ∼-refl equiv-resp-done

-- Composition respects being an equivalence

equiv-resp-⟦⟫⟧ : ∀ {S T U} (S∼T : S ∼ T) (T∼U : T ∼ U) →
  ⟦ equiv S∼T ⟧ ⟦⟫⟧ ⟦ equiv T∼U ⟧ ≃ ⟦ equiv (∼-trans S∼T T∼U) ⟧
equiv-resp-⟦⟫⟧ I       I        as       = refl
equiv-resp-⟦⟫⟧ (Σ W F) (Σ .W G) []       = refl
equiv-resp-⟦⟫⟧ (Σ W F) (Σ .W G) (a ∷ as) = cong (_∷_ a) (equiv-resp-⟦⟫⟧ (♭ F a) (♭ G a) as)

equiv-resp-⟫ : ∀ {S T U} (S∼T : S ∼ T) (T∼U : T ∼ U) →
  ⟦ equiv S∼T ⟫ equiv T∼U ⟧ ≃ ⟦ equiv (∼-trans S∼T T∼U) ⟧
equiv-resp-⟫ S∼T T∼U as =
  begin
    ⟦ equiv S∼T ⟫ equiv T∼U ⟧ as
  ≡⟨ ⟫-semantics (equiv S∼T) (equiv T∼U) as ⟩
    (⟦ equiv S∼T ⟧ ⟦⟫⟧ ⟦ equiv T∼U ⟧) as
  ≡⟨ equiv-resp-⟦⟫⟧ S∼T T∼U as ⟩
    ⟦ equiv (∼-trans S∼T T∼U) ⟧ as
  ∎

⟫-isEquiv : ∀ {S T U} {P : S ⇒ T} {Q : T ⇒ U} →
  (IsEquiv P) → (IsEquiv Q) → (IsEquiv (P ⟫ Q))
⟫-isEquiv {S} {T} {U} {P} {Q} (isEquiv S∼T P≃S∼T) (isEquiv (T∼U) (Q≃T∼U)) =
  isEquiv (∼-trans S∼T T∼U) λ as →
    begin
      ⟦ P ⟫ Q ⟧ as
    ≡⟨ ⟫-resp-≃ P≃S∼T Q≃T∼U as ⟩
      ⟦ equiv S∼T ⟫ equiv T∼U ⟧ as
    ≡⟨ equiv-resp-⟫ S∼T T∼U as ⟩
      ⟦ equiv (∼-trans S∼T T∼U) ⟧ as
    ∎

-- Equivalences form isos

equiv-is-iso : ∀ {S T} {P : S ⇒ T} {Q : T ⇒ S} →
  (IsEquiv P) → (IsEquiv Q) → ⟦ P ⟫ Q ⟧ ≃ ⟦ done ⟧
equiv-is-iso PisEq QisEq =
  ≃-equiv (⟫-isEquiv PisEq QisEq) done-isEquiv


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

-- Categorical equivalences preserve various structures

module Categories.Category.Equivalence.Preserves where

open import Level

open import Categories.Adjoint.Equivalence using (⊣Equivalence)
open import Categories.Category.Core
open import Categories.Category.Equivalence using (WeakInverse; StrongEquivalence)
open import Categories.Category.Equivalence.Properties using (C≅D)
open import Categories.Diagram.Duality
open import Categories.Functor.Core
open import Categories.Morphism
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
open import Categories.Object.Initial
open import Categories.Object.Terminal
open import Categories.Object.Duality

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C : Category o ℓ e
    D : Category o′ ℓ′ e′

module _ (S : StrongEquivalence C D) where
  open StrongEquivalence S
  open IsInitial
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
    X : ⊣Equivalence C D
    X = C≅D S

  -- see below the proof for the abbreviations that make the proof readable
  pres-IsInitial : {c : C.Obj} (i : IsInitial C c) → IsInitial D (F.₀ c)
  pres-IsInitial {c} i = record
    { ! = λ {A} →  F∘G≈id.⇒.η A D.∘ F.₁ (! i)
    ; !-unique = λ {A} f → begin  {- f : F.₀ c D.⇒ A -}
      FG⇒ A D.∘ F.₁ (! i)                                            ≈⟨ (refl⟩∘⟨ F.F-resp-≈ (!-unique i _)) ⟩
      FG⇒ A D.∘ F.₁ ((G.₁ f C.∘ GF⇒) C.∘ G.₁ FG⇐′ C.∘ GF⇐)          ≈⟨ (refl⟩∘⟨ F.homomorphism) ⟩
      FG⇒ A D.∘ F.₁ (G.₁ f C.∘ GF⇒) D.∘ F.₁ (G.₁ FG⇐′ C.∘ GF⇐)      ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (F.homomorphism ○ (D.Equiv.sym (F≃id-comm₂ F∘G≈id) ⟩∘⟨refl))) ⟩
      FG⇒ A D.∘ F.₁ (G.₁ f C.∘ GF⇒) D.∘ FG⇐ D.∘ F.F₁ GF⇐            ≈⟨ (refl⟩∘⟨ F.homomorphism ⟩∘⟨refl) ⟩
      FG⇒ A D.∘ (F.₁ (G.₁ f) D.∘ F.₁ GF⇒) D.∘ (FG⇐ D.∘ F.F₁ GF⇐)    ≈⟨ (D.sym-assoc ○ (D.sym-assoc ⟩∘⟨refl) ○ D.assoc) ⟩
      (FG⇒ A D.∘ F.₁ (G.₁ f)) D.∘ F.F₁ GF⇒ D.∘ FG⇐ D.∘ F.F₁ GF⇐     ≈⟨ (F∘G≈id.⇒.commute f ⟩∘⟨ D.sym-assoc) ⟩
      (f D.∘ FG⇒ (F.₀ c)) D.∘ (F.F₁ GF⇒ D.∘ FG⇐) D.∘ F.F₁ GF⇐       ≈⟨ (D.assoc ○ (refl⟩∘⟨ D.sym-assoc)) ⟩
      f D.∘ (FG⇒ (F.₀ c) D.∘ F.F₁ GF⇒ D.∘ FG⇐) D.∘ F.F₁ GF⇐         ≈⟨ elimʳ (⊣Equivalence.zig X) ⟩
      f ∎
    }
    where
    open D.HomReasoning
    open MR D
    FG⇒ : (A : D.Obj) → F.₀ (G.₀ A) D.⇒ A
    FG⇒ A = F∘G≈id.⇒.η A
    FG⇐ = F∘G≈id.⇐.η (F.F₀ (G.F₀ (F.F₀ c)))
    FG⇐′ = F∘G≈id.⇐.η (F.₀ c)
    GF⇐ : c C.⇒ G.₀ (F.₀ c)
    GF⇐ = G∘F≈id.⇐.η c
    GF⇒ = G∘F≈id.⇒.η (G.F₀ (F.F₀ c))

  pres-Initial : Initial C → Initial D
  pres-Initial i = record { ⊥ = F.₀ ⊥ ; ⊥-is-initial = pres-IsInitial ⊥-is-initial }
    where open Initial i

-- We can do the other proof by duality
pres-terminal : {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (S : StrongEquivalence C D) {c : Category.Obj C} → (t : IsTerminal C c) → IsTerminal D (Functor.F₀ (StrongEquivalence.F S) c)
pres-terminal {C = C} {D} S {c} t = IsInitial⇒coIsTerminal (Category.op D) (pres-IsInitial Sop (coIsTerminal⇒IsInitial (Category.op C) t))
  where
  Sop : StrongEquivalence (Category.op C) (Category.op D)
  Sop = StrongEquivalence.op S

pres-Terminal : {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (S : StrongEquivalence C D) (t : Terminal C) → Terminal D
pres-Terminal S t = record { ⊤ = Functor.F₀ F ⊤; ⊤-is-terminal = pres-terminal S ⊤-is-terminal}
  where
  open Terminal t
  open StrongEquivalence S

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- An ATP local hint cannot be equal to the conjecture in which it is
-- used.

-- This error is detected by Syntax.Translation.ConcreteToAbstract.

module ATPBadLocalHint1 where

postulate
  D : Set
  p : D

{-# ATP prove p p #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
------------------------------------------------------------------------
-- Reduced canonical kinding for the undecidability proof
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Canonical.Reduced where

open import Data.Context.WellFormed
open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.List using ([]; _∷_; _++_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (∃; _,_; _×_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec as Vec using ([]; _∷_)
open import Data.Vec.Properties as VecProps using (map-∘; map-cong)
open import Function using (_∘_)
open import Level using () renaming (zero to lzero)
open import Relation.Binary.PropositionalEquality

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.HereditarySubstitution using (Kind/⟨★⟩-/)
import FOmegaInt.Kinding.Canonical as CanonicalKinding

module C where
  open CanonicalKinding public
  open Kinding          public

------------------------------------------------------------------------
-- Reduced canonical kinding derivations.

module Kinding where
  open ElimCtx
  open Syntax
  open Substitution using (_Kind′[_])

  infix 4 _⊢_wf _ctx _⊢_kd
  infix 4 _⊢Nf_⇉_ _⊢Ne_⇉_ _⊢Var_⇉_ _⊢_⇉∙_⇉_ _⊢Nf_⇇_
  infix 4 _⊢_<∷_ _⊢_∼_
  infix 4 _⊢_⇉∙_∼_⇉_

  mutual

    -- Formation of kinds, bindings, and contexts.
    --
    -- NOTE. The rule kd-Π only supports first-order operators.

    data _⊢_kd {n} (Γ : Ctx n) : Kind Elim n → Set where
      kd-⋯ : ∀ {a b}   → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢Nf b ⇉ b ⋯ b → Γ ⊢ a ⋯ b kd
      kd-Π : ∀ {a b k} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢Nf b ⇉ b ⋯ b →
             kd (a ⋯ b) ∷ Γ ⊢ k kd → Γ ⊢ Π (a ⋯ b) k kd

    data _⊢_wf {n} (Γ : Ctx n) : ElimAsc n → Set where
      wf-kd : ∀ {a} → Γ ⊢ a kd        → Γ ⊢ kd a wf
      wf-tp : ∀ {a} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢ tp a wf

    _ctx : ∀ {n} → Ctx n → Set
    Γ ctx = ContextFormation._wf _⊢_wf Γ

    -- Kind synthesis for variables, neutrals and βη-normal types.

    data _⊢Var_⇉_ {n} (Γ : Ctx n) : Fin n → Kind Elim n → Set where
      ⇉-var : ∀ {k} x → Γ ctx → lookup Γ x ≡ kd k → Γ ⊢Var x ⇉ k

    data _⊢Ne_⇉_ {n} (Γ : Ctx n) : Elim n → Kind Elim n → Set where
      ⇉-∙ : ∀ {x j k} {as : Spine n} → Γ ⊢Var x ⇉ j →
            Γ ⊢ j ⇉∙ as ⇉ k → Γ ⊢Ne var x ∙ as ⇉ k

    data _⊢Nf_⇉_ {n} (Γ : Ctx n) : Elim n → Kind Elim n → Set where
      ⇉-⊥-f : Γ ctx → Γ ⊢Nf ⊥∙ ⇉ ⊥∙ ⋯ ⊥∙
      ⇉-⊤-f : Γ ctx → Γ ⊢Nf ⊤∙ ⇉ ⊤∙ ⋯ ⊤∙
      ⇉-s-i : ∀ {a b c} → Γ ⊢Ne a ⇉ b ⋯ c → Γ ⊢Nf a ⇉ a ⋯ a

    -- Kind checking for η-long β-normal types.

    data _⊢Nf_⇇_ {n} (Γ : Ctx n) : Elim n → Kind Elim n → Set where
      ⇇-⇑  : ∀ {a j k} → Γ ⊢Nf a ⇉ j → Γ ⊢ j <∷ k → Γ ⊢Nf a ⇇ k

    -- Kind synthesis for spines.
    --
    -- Note the use of ordinary (instead of hereditary) substitution.

    data _⊢_⇉∙_⇉_ {n} (Γ : Ctx n)
      : Kind Elim n → Spine n → Kind Elim n → Set where
      ⇉-[] : ∀ {k} → Γ ⊢ k ⇉∙ [] ⇉ k
      ⇉-∷  : ∀ {a as b c j k} → Γ ⊢Nf a ⇇ b ⋯ c →
             Γ ⊢ j Kind′[ ⌞ a ⌟ ] ⇉∙ as ⇉ k → Γ ⊢ Π (b ⋯ c) j ⇉∙ a ∷ as ⇉ k

    -- Reduced canonical subkinding derivations.
    --
    -- NOTE. The rule <∷-Π only supports first-order operators.

    data _⊢_<∷_ {n} (Γ : Ctx n) : Kind Elim n → Kind Elim n → Set where
      <∷-⋯ : ∀ {a₁ a₂ b₁ b₂} →
             Γ ⊢ a₂ ∼ a₁ → Γ ⊢ b₁ ∼ b₂ → Γ ⊢ a₁ ⋯ b₁ <∷ a₂ ⋯ b₂
      <∷-Π : ∀ {a₁ a₂ b₁ b₂ k₁ k₂} → Γ ⊢ a₁ ∼ a₂ → Γ ⊢ b₂ ∼ b₁ →
             kd (a₂ ⋯ b₂) ∷ Γ ⊢ k₁ <∷ k₂ →
             Γ ⊢ Π (a₁ ⋯ b₁) k₁ <∷ Π (a₂ ⋯ b₂) k₂

    -- Canonical relatedness of proper types and spines.

    data _⊢_∼_ {n} (Γ : Ctx n) : Elim n → Elim n → Set where
      ∼-trans : ∀ {a b c} → Γ ⊢ a ∼ b → Γ ⊢ b ∼ c → Γ ⊢ a ∼ c
      ∼-⊥     : ∀ {a} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢ ⊥∙ ∼ a
      ∼-⊤     : ∀ {a} → Γ ⊢Nf a ⇉ a ⋯ a → Γ ⊢ a ∼ ⊤∙
      ∼-∙     : ∀ {x as₁ as₂ k b c} →
                Γ ⊢Var x ⇉ k → Γ ⊢ k ⇉∙ as₁ ∼ as₂ ⇉ b ⋯ c →
                Γ ⊢ var x ∙ as₁ ∼ var x ∙ as₂
      ∼-⟨|    : ∀ {a b c} → Γ ⊢Ne a ⇉ b ⋯ c → Γ ⊢ b ∼ a
      ∼-|⟩    : ∀ {a b c} → Γ ⊢Ne a ⇉ b ⋯ c → Γ ⊢ a ∼ c

    data _⊢_⇉∙_∼_⇉_ {n} (Γ : Ctx n)
      : Kind Elim n → Spine n → Spine n → Kind Elim n → Set where
      ∼-[] : ∀ {k} → Γ ⊢ k ⇉∙ [] ∼ [] ⇉ k
      ∼-∷  : ∀ {a as b bs c d j k} → Γ ⊢ c ∼ a → Γ ⊢ a ∼ d →
             Γ ⊢ a ∼ b → Γ ⊢ j Kind′[ ⌞ a ⌟ ] ⇉∙ as ∼ bs ⇉ k →
             Γ ⊢ Π (c ⋯ d) j ⇉∙ a ∷ as ∼ b ∷ bs ⇉ k

  -- Well-formed context extensions.
  open ContextFormation _⊢_wf public hiding (_wf; _⊢_wfExt)

  -- A wrapper for the kind checking judgment that also supports
  -- arbitrary variable bindings.

  infix 4 _⊢NfOrVar_∈_

  data _⊢NfOrVar_∈_ {n} (Γ : Ctx n) : Term n → ElimAsc n → Set where
    ∈-nf  : ∀ {a b c d e} → Γ ⊢Nf a ⇇ c ⋯ d → ⌞ a ⌟ ≡ b → kd (c ⋯ d) ≡ e →
            Γ ⊢NfOrVar b ∈ e
    ∈-var : ∀ x {a b} → Γ ctx → var x ≡ a → lookup Γ x ≡ b →
            Γ ⊢NfOrVar a ∈ b

------------------------------------------------------------------------
-- Simple properties of canonical kindings

open Syntax
open ElimCtx hiding (_++_)
open Kinding

-- An inversion lemma for interval subkinding.

<∷-⋯-inv : ∀ {n} {Γ : Ctx n} {k a₂ b₂} → Γ ⊢ k <∷ a₂ ⋯ b₂ →
           ∃ λ a₁ → ∃ λ b₁ → Γ ⊢ a₂ ∼ a₁ × Γ ⊢ b₁ ∼ b₂ × k ≡ a₁ ⋯ b₁
<∷-⋯-inv (<∷-⋯ a₂∼a₁ b₁∼b₂) = _ , _ , a₂∼a₁ , b₁∼b₂ , refl

-- An inversion lemma for _⊢_wf.

wf-kd-inv : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ kd k wf → Γ ⊢ k kd
wf-kd-inv (wf-kd k-kd) = k-kd

-- The synthesized kind of a normal proper type is exactly the singleton
-- containing that type.

Nf⇉-≡ : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇉ k → k ≡ a ⋯ a
Nf⇉-≡ (⇉-⊥-f Γ-ctx)       = refl
Nf⇉-≡ (⇉-⊤-f Γ-ctx)       = refl
Nf⇉-≡ (⇉-s-i a∈b⋯c)       = refl

-- Derived singleton introduction rules where the premises are
-- well-kinded normal forms rather than neutrals.

Nf⇉-s-i : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇉ k → Γ ⊢Nf a ⇉ a ⋯ a
Nf⇉-s-i a⇉b⋯c with Nf⇉-≡ a⇉b⋯c
Nf⇉-s-i a⇉a⋯a | refl = a⇉a⋯a

Nf⇇-s-i : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢Nf a ⇉ a ⋯ a
Nf⇇-s-i (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂∼b₁ c₁∼c₂)) = Nf⇉-s-i a⇉b₁⋯c₁

-- The synthesized kinds of neutrals kind-check.

Nf⇇-ne : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Ne a ⇉ b ⋯ c → Γ ⊢Nf a ⇇ b ⋯ c
Nf⇇-ne (⇉-∙ x∈k k⇉as⇉b⋯c) =
  ⇇-⇑ (⇉-s-i (⇉-∙ x∈k k⇉as⇉b⋯c))
      (<∷-⋯ (∼-⟨| (⇉-∙ x∈k k⇉as⇉b⋯c)) (∼-|⟩ (⇉-∙ x∈k k⇉as⇉b⋯c)))

-- The contexts of (most of) the above judgments are well-formed.
--
-- NOTE. The exceptions are again the spine judgments.  See the
-- comment on context validity in FOmegaInt.Kinding.Canonical for why
-- this doesn't matter.

Var⇉-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Var a ⇉ k → Γ ctx
Var⇉-ctx (⇉-var x Γ-ctx _) = Γ-ctx

Ne⇉-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Ne a ⇉ k → Γ ctx
Ne⇉-ctx (⇉-∙ x∈j j⇉as⇉k) = Var⇉-ctx x∈j

Nf⇉-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇉ k → Γ ctx
Nf⇉-ctx (⇉-⊥-f Γ-ctx) = Γ-ctx
Nf⇉-ctx (⇉-⊤-f Γ-ctx) = Γ-ctx
Nf⇉-ctx (⇉-s-i a∈b⋯c) = Ne⇉-ctx a∈b⋯c

Nf⇇-ctx : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇇ k → Γ ctx
Nf⇇-ctx (⇇-⇑ a⇉j j<∷k) = Nf⇉-ctx a⇉j

kd-ctx : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ctx
kd-ctx (kd-⋯ a⇉a⋯a b⇉b⋯b)      = Nf⇉-ctx a⇉a⋯a
kd-ctx (kd-Π a⇉a⋯a b⇉b⋯b k-kd) = Nf⇉-ctx a⇉a⋯a

∼-ctx : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ∼ b → Γ ctx
∼-ctx (∼-trans a∼b b∼c)   = ∼-ctx a∼b
∼-ctx (∼-⊥ a⇉a⋯a)           = Nf⇉-ctx a⇉a⋯a
∼-ctx (∼-⊤ a⇉a⋯a)           = Nf⇉-ctx a⇉a⋯a
∼-ctx (∼-∙ x∈j as∼bs)       = Var⇉-ctx x∈j
∼-ctx (∼-⟨| a∈b⋯c)          = Ne⇉-ctx a∈b⋯c
∼-ctx (∼-|⟩ a∈b⋯c)          = Ne⇉-ctx a∈b⋯c

<∷-ctx : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → Γ ctx
<∷-ctx (<∷-⋯ a₂∼a₁ b₁∼b₂)        = ∼-ctx a₂∼a₁
<∷-ctx (<∷-Π a₁∼a₂ b₂∼b₁ k₁<∷k₂) = ∼-ctx a₁∼a₂

wf-ctx : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢ a wf → Γ ctx
wf-ctx (wf-kd k-kd)  = kd-ctx k-kd
wf-ctx (wf-tp a⇉a⋯a) = Nf⇉-ctx a⇉a⋯a

NfOrVar∈-ctx : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢NfOrVar a ∈ b → Γ ctx
NfOrVar∈-ctx (∈-nf a⇇c⋯d _ _)    = Nf⇇-ctx a⇇c⋯d
NfOrVar∈-ctx (∈-var x Γ-ctx _ _) = Γ-ctx

-- Reflexivity of the various relations.

mutual

  <∷-refl : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ ⊢ k <∷ k
  <∷-refl (kd-⋯ a⇉a⋯a b⇉b⋯b)      = <∷-⋯ (∼-refl a⇉a⋯a) (∼-refl b⇉b⋯b)
  <∷-refl (kd-Π a⇉a⋯a b⇉b⋯b k-kd) =
    <∷-Π (∼-refl a⇉a⋯a) (∼-refl b⇉b⋯b) (<∷-refl k-kd)

  ∼-refl : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢ a ∼ a
  ∼-refl (⇉-⊥-f Γ-ctx)            = ∼-⊥ (⇉-⊥-f Γ-ctx)
  ∼-refl (⇉-⊤-f Γ-ctx)            = ∼-⊤ (⇉-⊤-f Γ-ctx)
  ∼-refl (⇉-s-i (⇉-∙ x∈j j⇉as⇉k)) = ∼-∙ x∈j (∼Sp-refl j⇉as⇉k)

  ∼Sp-refl : ∀ {n} {Γ : Ctx n} {as j k} →
             Γ ⊢ j ⇉∙ as ⇉ k → Γ ⊢ j ⇉∙ as ∼ as ⇉ k
  ∼Sp-refl ⇉-[]                       = ∼-[]
  ∼Sp-refl (⇉-∷ (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂∼b₁ c₁∼c₂)) k[a]⇉as⇉l)
    with Nf⇉-≡ a⇉b₁⋯c₁
  ∼Sp-refl (⇉-∷ (⇇-⇑ a⇉a⋯a (<∷-⋯ b∼a a∼c)) k[a]⇉as⇉l) | refl =
    ∼-∷ b∼a a∼c (∼-refl a⇉a⋯a) (∼Sp-refl k[a]⇉as⇉l)

-- Admissible projection rules for canonically kinded proper types.

∼-⟨|-Nf⇉ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢ b ∼ a
∼-⟨|-Nf⇉ a⇉b⋯c with Nf⇉-≡ a⇉b⋯c
∼-⟨|-Nf⇉ a⇉a⋯a | refl = ∼-refl a⇉a⋯a

∼-⟨|-Nf⇇ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢ b ∼ a
∼-⟨|-Nf⇇ (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂∼b₁ c₁∼c₂)) =
  ∼-trans b₂∼b₁ (∼-⟨|-Nf⇉ a⇉b₁⋯c₁)

∼-|⟩-Nf⇉ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇉ b ⋯ c → Γ ⊢ a ∼ c
∼-|⟩-Nf⇉ a⇉b⋯c with Nf⇉-≡ a⇉b⋯c
∼-|⟩-Nf⇉ a⇉a⋯a | refl = ∼-refl a⇉a⋯a

∼-|⟩-Nf⇇ : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢ a ∼ c
∼-|⟩-Nf⇇ (⇇-⇑ a⇉b₁⋯c₁ (<∷-⋯ b₂∼b₁ c₁∼c₂)) =
  ∼-trans (∼-|⟩-Nf⇉ a⇉b₁⋯c₁) c₁∼c₂

-- Spines with interval-kinded heads are empty, and therefore have
-- interval-kinded tails.

Sp⇉-⋯ : ∀ {n} {Γ : Ctx n} {as b c k} →
        Γ ⊢ b ⋯ c ⇉∙ as ⇉ k → as ≡ [] × k ≡ b ⋯ c
Sp⇉-⋯ ⇉-[] = refl , refl

Sp∼-⋯ : ∀ {n} {Γ : Ctx n} {as bs c d k} →
        Γ ⊢ c ⋯ d ⇉∙ as ∼ bs ⇉ k → as ≡ [] × bs ≡ [] × k ≡ c ⋯ d
Sp∼-⋯ ∼-[] = refl , refl , refl

----------------------------------------------------------------------
-- Well-kinded/typed substitutions (i.e. substitution lemmas)

-- A shorthand for kindings and typings of Ts by kind or type
-- ascriptions.
ElimAscTyping : (ℕ → Set) → Set₁
ElimAscTyping T = Typing ElimAsc T ElimAsc Level.zero

-- Liftings from well-typed Ts to well-typed/kinded normal forms or
-- variables.
LiftTo-NfOrVar∈ : ∀ {T} → ElimAscTyping T → Set₁
LiftTo-NfOrVar∈ _⊢T_∈_ =
  LiftTyped Substitution.elimAscTermSubst _⊢_wf _⊢T_∈_ _⊢NfOrVar_∈_

-- A helper lemma about untyped T-substitutions in raw kinds.

record TypedSubstAppHelpers {T} (rawLift : Lift T Term) : Set where
  open Substitution using (_Kind′[_])
  module A = SubstApp rawLift
  module L = Lift     rawLift

  -- Substitutions in kinds and types commute.

  field Kind/-sub-↑ : ∀ {m n} k a (σ : Sub T m n) →
                      k Kind′[ ⌞ a ⌟ ] A.Kind′/ σ ≡
                        (k A.Kind′/ σ L.↑) Kind′[ ⌞ a A.Elim/ σ ⌟ ]

-- Application of generic well-typed T-substitutions to all the judgments.

module TypedSubstApp {T : ℕ → Set} (_⊢T_∈_ : ElimAscTyping T)
                     (liftTyped : LiftTo-NfOrVar∈ _⊢T_∈_)
                     (helpers : TypedSubstAppHelpers
                                  (LiftTyped.rawLift liftTyped))
                     where

  open LiftTyped liftTyped renaming (lookup to /∈-lookup) hiding (∈-var)
  open TypedSubstAppHelpers helpers

  -- Well-typed/kinded substitutions preserve all the judgments.

  mutual

    wf-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a σ} →
              Γ ⊢ a wf → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A.ElimAsc/ σ wf
    wf-/ (wf-kd k-kd)  σ∈Γ = wf-kd (kd-/ k-kd σ∈Γ)
    wf-/ (wf-tp a⇉a⋯a) σ∈Γ = wf-tp (Nf⇉-/ a⇉a⋯a σ∈Γ)

    kd-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {k σ} →
              Γ ⊢ k kd → Δ ⊢/ σ ∈ Γ → Δ ⊢ k A.Kind′/ σ kd
    kd-/ (kd-⋯ a⇉a⋯a b⇉b⋯b) σ∈Γ =
      kd-⋯ (Nf⇉-/ a⇉a⋯a σ∈Γ) (Nf⇉-/ b⇉b⋯b σ∈Γ)
    kd-/ (kd-Π a⇉a⋯a b⇉b⋯b  k-kd) σ∈Γ =
      let a/σ⇉a/σ⋯a/σ = Nf⇉-/ a⇉a⋯a σ∈Γ
          b/σ⇉b/σ⋯b/σ = Nf⇉-/ b⇉b⋯b σ∈Γ
      in kd-Π a/σ⇉a/σ⋯a/σ b/σ⇉b/σ⋯b/σ
              (kd-/ k-kd (∈-↑ (wf-kd (kd-⋯ a/σ⇉a/σ⋯a/σ b/σ⇉b/σ⋯b/σ)) σ∈Γ))

    Ne⇉-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k σ} →
               Γ ⊢Ne a ⇉ k → Δ ⊢/ σ ∈ Γ →
               Δ ⊢Nf a A.Elim/ σ ⇇ k A.Kind′/ σ ⊎
               Δ ⊢Ne a A.Elim/ σ ⇉ k A.Kind′/ σ
    Ne⇉-/ (⇉-∙ (⇉-var x Γ-ctx Γ[x]≡j) j⇉as⇉k) σ∈Γ with ∈-lift (/∈-lookup σ∈Γ x)
    ... | ∈-nf {a} a⇇c⋯d ⌞a⌟≡σ[x] c⋯d≡Γ[x]/σ =
      let c⋯d≡j/σ = kd-inj (trans c⋯d≡Γ[x]/σ (cong (A._ElimAsc/ _) Γ[x]≡j))
          c⋯d⇉as/σ⇉k/σ = subst (_ ⊢_⇉∙ _ ⇉ _) (sym c⋯d≡j/σ) (Sp⇉-/ j⇉as⇉k σ∈Γ)
          as≡[] , k/σ≡c⋯d = Sp⇉-⋯ c⋯d⇉as/σ⇉k/σ
          a≡⌜σ[x]⌝ = trans (sym (⌜⌝∘⌞⌟-id a)) (cong ⌜_⌝ ⌞a⌟≡σ[x])
          ⌜σ[x]⌝∙∙as≡a = trans (cong₂ _∙∙_ (sym a≡⌜σ[x]⌝) as≡[]) (∙∙-[] _)
      in inj₁ (subst₂ (_ ⊢Nf_⇇_) (sym ⌜σ[x]⌝∙∙as≡a) (sym k/σ≡c⋯d) a⇇c⋯d)
    ... | ∈-var y Δ-ctx y≡σ[x] Δ[y]≡Γ[x]/σ =
      let Δ[y]≡j/σ = trans Δ[y]≡Γ[x]/σ (cong (A._ElimAsc/ _) Γ[x]≡j)
      in inj₂ (subst (_ ⊢Ne_⇉ _) (cong (_∙∙ _) (cong ⌜_⌝ y≡σ[x]))
                     (⇉-∙ (⇉-var y Δ-ctx Δ[y]≡j/σ) (Sp⇉-/ j⇉as⇉k σ∈Γ)))

    Nf⇉-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k σ} →
            Γ ⊢Nf a ⇉ k → Δ ⊢/ σ ∈ Γ → Δ ⊢Nf a A.Elim/ σ ⇉ k A.Kind′/ σ
    Nf⇉-/ (⇉-⊥-f Γ-ctx) σ∈Γ = ⇉-⊥-f (/∈-wf σ∈Γ)
    Nf⇉-/ (⇉-⊤-f Γ-ctx) σ∈Γ = ⇉-⊤-f (/∈-wf σ∈Γ)
    Nf⇉-/ (⇉-s-i a∈b⋯c) σ∈Γ with Ne⇉-/ a∈b⋯c σ∈Γ
    ... | inj₁ a/σ⇇b/σ⋯c/σ = Nf⇇-s-i a/σ⇇b/σ⋯c/σ
    ... | inj₂ a/σ⇉b/σ⋯c/σ = ⇉-s-i a/σ⇉b/σ⋯c/σ

    Nf⇇-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a k σ} →
               Γ ⊢Nf a ⇇ k → Δ ⊢/ σ ∈ Γ → Δ ⊢Nf a A.Elim/ σ ⇇ k A.Kind′/ σ
    Nf⇇-/ (⇇-⇑ a⇉j j<∷k) σ∈Γ = ⇇-⇑ (Nf⇉-/ a⇉j σ∈Γ) (<∷-/ j<∷k σ∈Γ)

    Sp⇉-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {as j k σ} →
               Γ ⊢ j ⇉∙ as ⇉ k → Δ ⊢/ σ ∈ Γ →
               Δ ⊢ j A.Kind′/ σ ⇉∙ as A.// σ ⇉ k A.Kind′/ σ
    Sp⇉-/ ⇉-[]                                σ∈Γ = ⇉-[]
    Sp⇉-/ (⇉-∷ {a} {j = j} a⇇b⋯c j[a]⇉as⇉k) σ∈Γ =
      ⇉-∷ (Nf⇇-/ a⇇b⋯c σ∈Γ)
          (subst (_ ⊢_⇉∙ _ ⇉ _) (Kind/-sub-↑ j a _)
                 (Sp⇉-/ j[a]⇉as⇉k σ∈Γ))

    <∷-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k σ} →
              Γ ⊢ j <∷ k → Δ ⊢/ σ ∈ Γ → Δ ⊢ j A.Kind′/ σ <∷ k A.Kind′/ σ
    <∷-/ (<∷-⋯ a₂∼a₁ b₁∼b₂) σ∈Γ =
      <∷-⋯ (∼-/ a₂∼a₁ σ∈Γ) (∼-/ b₁∼b₂ σ∈Γ)
    <∷-/ (<∷-Π a₁∼a₂ b₂∼b₁ k₁<∷k₂) σ∈Γ =
      <∷-Π (∼-/ a₁∼a₂ σ∈Γ) (∼-/ b₂∼b₁ σ∈Γ)
           (<∷-/ k₁<∷k₂ (∈-↑ (<∷-/-wf k₁<∷k₂ σ∈Γ) σ∈Γ))

    ∼-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
              Γ ⊢ a ∼ b → Δ ⊢/ σ ∈ Γ → Δ ⊢ a A.Elim/ σ ∼ b A.Elim/ σ
    ∼-/ (∼-trans a∼b b∼c) σ∈Γ =
      ∼-trans (∼-/ a∼b σ∈Γ) (∼-/ b∼c σ∈Γ)
    ∼-/ (∼-⊥ a⇉a⋯a) σ∈Γ = ∼-⊥ (Nf⇉-/ a⇉a⋯a σ∈Γ)
    ∼-/ (∼-⊤ a⇉a⋯a) σ∈Γ = ∼-⊤ (Nf⇉-/ a⇉a⋯a σ∈Γ)
    ∼-/ (∼-∙ (⇉-var x Γ-ctx Γ[x]≡j) j⇉as∼bs⇉k) σ∈Γ
      with ∈-lift (/∈-lookup σ∈Γ x)
    ... | ∈-nf {a} (⇇-⇑ a⇉c₁⋯d₁ (<∷-⋯ _ _)) ⌞a⌟≡σ[x] c⋯d≡Γ[x]/σ =
      let c⋯d≡j/σ = kd-inj (trans c⋯d≡Γ[x]/σ (cong (A._ElimAsc/ _) Γ[x]≡j))
          c⋯d⇉as/σ∼bs/σ⇉k/σ = subst (_ ⊢_⇉∙ _ ∼ _ ⇉ _) (sym c⋯d≡j/σ)
                                    (Sp∼-/ j⇉as∼bs⇉k σ∈Γ)
          as≡[] , bs≡[] , _ = Sp∼-⋯ c⋯d⇉as/σ∼bs/σ⇉k/σ
          a≡⌜σ[x]⌝ = trans (sym (⌜⌝∘⌞⌟-id a)) (cong ⌜_⌝ ⌞a⌟≡σ[x])
          ⌜σ[x]⌝∙∙as≡a = trans (cong₂ _∙∙_ (sym a≡⌜σ[x]⌝) as≡[]) (∙∙-[] _)
          ⌜σ[x]⌝∙∙bs≡a = trans (cong₂ _∙∙_ (sym a≡⌜σ[x]⌝) bs≡[]) (∙∙-[] _)
      in subst₂ (_ ⊢_∼_) (sym ⌜σ[x]⌝∙∙as≡a) (sym ⌜σ[x]⌝∙∙bs≡a)
                (∼-refl a⇉c₁⋯d₁)
    ... | ∈-var y Δ-ctx y≡σ[x] Δ[y]≡Γ[x]/σ =
      let Δ[y]≡j/σ = trans Δ[y]≡Γ[x]/σ (cong (A._ElimAsc/ _) Γ[x]≡j)
      in subst₂ (_ ⊢_∼_) (cong (_∙∙ _) (cong ⌜_⌝ y≡σ[x]))
                (cong (_∙∙ _) (cong ⌜_⌝ y≡σ[x]))
                (∼-∙ (⇉-var y Δ-ctx Δ[y]≡j/σ) (Sp∼-/ j⇉as∼bs⇉k σ∈Γ))
    ∼-/ (∼-⟨| a∈b⋯c) σ∈Γ with Ne⇉-/ a∈b⋯c σ∈Γ
    ... | inj₁ a⇇b⋯c = ∼-⟨|-Nf⇇ a⇇b⋯c
    ... | inj₂ a⇉b⋯c = ∼-⟨| a⇉b⋯c
    ∼-/ (∼-|⟩ a∈b⋯c) σ∈Γ with Ne⇉-/ a∈b⋯c σ∈Γ
    ... | inj₁ a⇇b⋯c = ∼-|⟩-Nf⇇ a⇇b⋯c
    ... | inj₂ a⇉b⋯c = ∼-|⟩ a⇉b⋯c

    Sp∼-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {as bs j k σ} →
                Γ ⊢ j ⇉∙ as ∼ bs ⇉ k → Δ ⊢/ σ ∈ Γ →
                Δ ⊢ j A.Kind′/ σ ⇉∙ as A.// σ ∼ bs A.// σ ⇉ k A.Kind′/ σ
    Sp∼-/ ∼-[] σ∈Γ = ∼-[]
    Sp∼-/ (∼-∷ {a} {j = j} c∼a a∼d a∼b as∼bs) σ∈Γ =
      ∼-∷ (∼-/ c∼a σ∈Γ) (∼-/ a∼d σ∈Γ) (∼-/ a∼b σ∈Γ)
          (subst (_ ⊢_⇉∙ _ ∼ _ ⇉ _) (Kind/-sub-↑ j a _)
                 (Sp∼-/ as∼bs σ∈Γ))

    -- Helpers (to satisfy the termination checker).
    --
    -- These are simply (manual) expansions of the form
    --
    --   XX-/-wf x σ∈Γ  =  wf-/ (wf-∷₁ (XX-ctx x)) σ∈Γ
    --
    -- to ensure the above definitions remain structurally recursive
    -- in the various derivations.

    Nf⇉-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k σ} →
                  kd j ∷ Γ ⊢Nf a ⇉ k → Δ ⊢/ σ ∈ Γ →
                  Δ ⊢ kd (j A.Kind′/ σ) wf
    Nf⇉-/-wf (⇉-⊥-f (j-wf ∷ _)) σ∈Γ = wf-/ j-wf σ∈Γ
    Nf⇉-/-wf (⇉-⊤-f (j-wf ∷ _)) σ∈Γ = wf-/ j-wf σ∈Γ
    Nf⇉-/-wf (⇉-s-i a∈b⋯c)      σ∈Γ = Ne⇉-/-wf a∈b⋯c σ∈Γ

    Ne⇉-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k σ} →
                  kd j ∷ Γ ⊢Ne a ⇉ k → Δ ⊢/ σ ∈ Γ →
                  Δ ⊢ kd (j A.Kind′/ σ) wf
    Ne⇉-/-wf (⇉-∙ x∈k _) σ∈Γ = Var⇉-/-wf x∈k σ∈Γ

    Var⇉-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a j k σ} →
                   kd j ∷ Γ ⊢Var a ⇉ k → Δ ⊢/ σ ∈ Γ →
                   Δ ⊢ kd (j A.Kind′/ σ) wf
    Var⇉-/-wf (⇉-var x (j-wf ∷ _) _) σ∈Γ = wf-/ j-wf σ∈Γ

    <∷-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {j k l σ} →
                 kd j ∷ Γ ⊢ k <∷ l → Δ ⊢/ σ ∈ Γ → Δ ⊢ kd (j A.Kind′/ σ) wf
    <∷-/-wf (<∷-⋯ a₂∼a₁ _)   σ∈Γ = ∼-/-wf a₂∼a₁ σ∈Γ
    <∷-/-wf (<∷-Π a₁∼a₂ _ _) σ∈Γ = ∼-/-wf a₁∼a₂ σ∈Γ

    ∼-/-wf : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b j σ} →
                 kd j ∷ Γ ⊢ a ∼ b → Δ ⊢/ σ ∈ Γ →
                 Δ ⊢ kd (j A.Kind′/ σ) wf
    ∼-/-wf (∼-trans a∼b _)  σ∈Γ = ∼-/-wf a∼b σ∈Γ
    ∼-/-wf (∼-⊥ a⇉a⋯a)      σ∈Γ = Nf⇉-/-wf a⇉a⋯a σ∈Γ
    ∼-/-wf (∼-⊤ a⇉a⋯a)      σ∈Γ = Nf⇉-/-wf a⇉a⋯a σ∈Γ
    ∼-/-wf (∼-∙ x∈j _)      σ∈Γ = Var⇉-/-wf x∈j σ∈Γ
    ∼-/-wf (∼-⟨| a∈b⋯c)     σ∈Γ = Ne⇉-/-wf a∈b⋯c σ∈Γ
    ∼-/-wf (∼-|⟩ a∈b⋯c)     σ∈Γ = Ne⇉-/-wf a∈b⋯c σ∈Γ

  -- Renamings preserve wrapped variable typing

  NfOrVar∈-/ : ∀ {m n} {Γ : Ctx m} {Δ : Ctx n} {a b σ} →
               Γ ⊢NfOrVar a ∈ b → Δ ⊢/ σ ∈ Γ →
               Δ ⊢NfOrVar a A./ σ ∈ b A.ElimAsc/ σ
  NfOrVar∈-/ (∈-nf {a} a⇇c⋯d refl refl) σ∈Γ =
    ∈-nf (Nf⇇-/ a⇇c⋯d σ∈Γ) (A.⌞⌟-/ a) refl
  NfOrVar∈-/ (∈-var x _ refl refl)  σ∈Γ = ∈-lift (/∈-lookup σ∈Γ x)

-- Well-kinded renamings and type substitutions.

module KindedSubstitution where
  open Substitution           using (simple; termSubst)
  open SimpleExt    simple    using (extension)
  open TermSubst    termSubst using (varLift; termLift)
  open ≡-Reasoning

  private
    module S  = Substitution
    module KL = TermLikeLemmas S.termLikeLemmasKind′

  -- Helper lemmas about untyped renamings and substitutions in terms
  -- and kinds.

  varHelpers : TypedSubstAppHelpers varLift
  varHelpers = record
    { Kind/-sub-↑ = λ k a ρ → begin
          (k Kind′[ ⌞ a ⌟ ]) Kind′/Var ρ
        ≡⟨ KL./-sub-↑ k ⌞ a ⌟ ρ ⟩
          (k Kind′/Var ρ VarSubst.↑) Kind′[ ⌞ a ⌟ /Var ρ ]
        ≡⟨ cong ((k Kind′/Var ρ VarSubst.↑) Kind′[_]) (sym (⌞⌟-/Var a)) ⟩
          (k Kind′/Var ρ VarSubst.↑) Kind′[ ⌞ a Elim/Var ρ ⌟ ]
        ∎
    }
    where open S

  termHelpers : TypedSubstAppHelpers termLift
  termHelpers = record
    { Kind/-sub-↑ = λ k a σ → begin
          (k Kind′[ ⌞ a ⌟ ]) Kind′/ σ
        ≡⟨ KL.sub-commutes k ⟩
          (k Kind′/ σ ↑) Kind′[ ⌞ a ⌟ / σ ]
        ≡⟨ cong ((k Kind′/ σ ↑) Kind′[_]) (sym (⌞⌟-/ a)) ⟩
          (k Kind′/ σ ↑) Kind′[ ⌞ a Elim/ σ ⌟ ]
        ∎
    }
    where open S

  -- Kinded type substitutions.

  typedTermSubst : TypedTermSubst ElimAsc Term Level.zero TypedSubstAppHelpers
  typedTermSubst = record
    { _⊢_wf = _⊢_wf
    ; _⊢_∈_ = _⊢NfOrVar_∈_
    ; termLikeLemmas = S.termLikeLemmasElimAsc
    ; varHelpers     = varHelpers
    ; termHelpers    = termHelpers
    ; wf-wf    = wf-ctx
    ; ∈-wf     = NfOrVar∈-ctx
    ; ∈-var    = λ x Γ-ctx → ∈-var x Γ-ctx refl refl
    ; typedApp = TypedSubstApp.NfOrVar∈-/
    }
  open TypedTermSubst typedTermSubst public
    hiding (_⊢_wf; _⊢_∈_; varHelpers; termHelpers; ∈-var; ∈-/Var; ∈-/)
    renaming (lookup to /∈-lookup)
  open TypedSubstApp _⊢Var_∈_ varLiftTyped varHelpers public using ()
    renaming (wf-/ to wf-/Var; ∼-/ to ∼-/Var)
  open Substitution using (weakenElim; weakenElimAsc)

  -- Weakening preserves the various judgments.

  wf-weaken : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a wf → Γ ⊢ b wf →
              (a ∷ Γ) ⊢ weakenElimAsc b wf
  wf-weaken a-wf b-wf = wf-/Var b-wf (Var∈-wk a-wf)

  ∼-weaken : ∀ {n} {Γ : Ctx n} {a b c} → Γ ⊢ a wf → Γ ⊢ b ∼ c →
             (a ∷ Γ) ⊢ weakenElim b ∼ weakenElim c
  ∼-weaken a-wf b∼c∈k = ∼-/Var b∼c∈k (Var∈-wk a-wf)

  open TypedSubstApp _⊢NfOrVar_∈_ termLiftTyped termHelpers public
  open Substitution using (_Kind′/_; id; sub; _Kind′[_])

  -- Substitution of a single variable or normal form preserves the
  -- kinding judgments.

  kd-[] : ∀ {n} {Γ : Ctx n} {a b c k} →
          kd (b ⋯ c) ∷ Γ ⊢ k kd → Γ ⊢Nf a ⇇ b ⋯ c → Γ ⊢ k Kind′[ ⌞ a ⌟ ] kd
  kd-[] k-kd a⇇b⋯c = kd-/ k-kd (∈-sub (∈-nf a⇇b⋯c refl refl))

  <∷-[] : ∀ {n} {Γ : Ctx n} {j k a b c} →
          kd (b ⋯ c) ∷ Γ ⊢ j <∷ k → Γ ⊢Nf a ⇇ b ⋯ c →
          Γ ⊢ j Kind′[ ⌞ a ⌟ ] <∷ k Kind′[ ⌞ a ⌟ ]
  <∷-[] j<∷k a⇇b⋯c = <∷-/ j<∷k (∈-sub (∈-nf a⇇b⋯c refl refl))

  -- A typed substitution that narrows the kind of the first type
  -- variable.

  ∈-<∷-sub : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂} →
             Γ ⊢ (a₁ ⋯ b₁) kd → Γ ⊢ a₂ ∼ a₁ → Γ ⊢ b₁ ∼ b₂ →
             kd (a₁ ⋯ b₁) ∷ Γ ⊢/ id ∈ kd (a₂ ⋯ b₂) ∷ Γ
  ∈-<∷-sub a₁⋯b₁-kd a₁∼a₂ b₂∼b₁ =
    ∈-tsub (∈-nf (⇇-⇑ (⇉-s-i x∈a₁⋯a₂) (<∷-⋯ x∼a₂ b₂∼x)) refl refl)
    where
      a₁⋯b₁-wf = wf-kd a₁⋯b₁-kd
      Γ-ctx    = kd-ctx a₁⋯b₁-kd
      x∈a₁⋯a₂  = ⇉-∙ (⇉-var zero (a₁⋯b₁-wf ∷ Γ-ctx) refl) ⇉-[]
      x∼a₂     = ∼-trans (∼-weaken a₁⋯b₁-wf a₁∼a₂) (∼-⟨| x∈a₁⋯a₂)
      b₂∼x     = ∼-trans (∼-|⟩ x∈a₁⋯a₂) (∼-weaken a₁⋯b₁-wf b₂∼b₁)

  -- Narrowing the kind of the first type variable preserves
  -- subkinding

  ⇓-<∷ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ k₁ k₂} →
         Γ ⊢ (a₁ ⋯ b₁) kd → Γ ⊢ a₂ ∼ a₁ → Γ ⊢ b₁ ∼ b₂ →
         kd (a₂ ⋯ b₂) ∷ Γ ⊢ k₁ <∷ k₂ → kd (a₁ ⋯ b₁) ∷ Γ ⊢ k₁ <∷ k₂
  ⇓-<∷ a₁⋯b₁-kd a₂∼a₁ b₁∼b₂ k₁<∷k₂ =
    subst₂ (_ ⊢_<∷_) (KL.id-vanishes _) (KL.id-vanishes _)
           (<∷-/ k₁<∷k₂ (∈-<∷-sub a₁⋯b₁-kd a₂∼a₁ b₁∼b₂))

-- Operations on well-formed contexts that require weakening of
-- well-formedness judgments.

module WfCtxOps where
  wfWeakenOps : WellFormedWeakenOps weakenOps
  wfWeakenOps = record { wf-weaken = KindedSubstitution.wf-weaken }

  open WellFormedWeakenOps wfWeakenOps public renaming (lookup to lookup-wf)

  -- Lookup the kind of a type variable in a well-formed context.

  lookup-kd : ∀ {m} {Γ : Ctx m} {k} x →
              Γ ctx → ElimCtx.lookup Γ x ≡ kd k → Γ ⊢ k kd
  lookup-kd x Γ-ctx Γ[x]≡kd-k =
    wf-kd-inv (subst (_ ⊢_wf) Γ[x]≡kd-k (lookup-wf Γ-ctx x))

open KindedSubstitution
open WfCtxOps

-- A corollary of context narrowing: transitivity of subkinding is
-- admissible.

<∷-trans : ∀ {n} {Γ : Ctx n} {j k l} → Γ ⊢ j <∷ k → Γ ⊢ k <∷ l → Γ ⊢ j <∷ l
<∷-trans (<∷-⋯ a₂∼a₁ b₁∼b₂) (<∷-⋯ a₃∼a₂ b₂∼b₃) =
  <∷-⋯ (∼-trans a₃∼a₂ a₂∼a₁) (∼-trans b₁∼b₂ b₂∼b₃)
<∷-trans (<∷-Π a₁∼a₂ b₂∼b₁ k₁<∷k₂) (<∷-Π a₂∼a₃ b₃∼b₂ k₂<∷k₃) =
  let a₃⋯b₃-kd = wf-kd-inv (wf-∷₁ (<∷-ctx k₂<∷k₃))
  in <∷-Π (∼-trans a₁∼a₂ a₂∼a₃) (∼-trans b₃∼b₂ b₂∼b₁)
          (<∷-trans (⇓-<∷ a₃⋯b₃-kd a₂∼a₃ b₃∼b₂ k₁<∷k₂) k₂<∷k₃)

-- Another corollary: subsumption is admissible in kind checking.

Nf⇇-⇑ : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢Nf a ⇇ j → Γ ⊢ j <∷ k → Γ ⊢Nf a ⇇ k
Nf⇇-⇑ (⇇-⇑ a⇇j₁ j₁<∷j₂) j₂<∷j₃ = ⇇-⇑ a⇇j₁ (<∷-trans j₁<∷j₂ j₂<∷j₃)

-- We can push kind formation proofs through spine kindings.

kd-Sp⇉ : ∀ {n} {Γ : Ctx n} {j as k} →
         Γ ⊢ j kd → Γ ⊢ j ⇉∙ as ⇉ k → Γ ⊢ k kd
kd-Sp⇉ j-kd ⇉-[] = j-kd
kd-Sp⇉ (kd-Π b⇉b⋯b c⇉c⋯c j-kd) (⇉-∷ a⇇b⋯c j[a]⇉as⇉k) =
  kd-Sp⇉ (kd-[] j-kd a⇇b⋯c) j[a]⇉as⇉k

-- Kind-validity of neutrals

Var⇉-valid : ∀ {n} {Γ : Ctx n} {x k} → Γ ⊢Var x ⇉ k → Γ ⊢ k kd
Var⇉-valid (⇉-var x Γ-ctx Γ[x]≡k) = lookup-kd x Γ-ctx Γ[x]≡k

Ne⇉-valid : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Ne a ⇉ k → Γ ⊢ k kd
Ne⇉-valid (⇉-∙ x⇉j j⇉as⇉k) = kd-Sp⇉ (Var⇉-valid x⇉j) j⇉as⇉k

-- Left-hand validity of related types and spines

mutual

  ∼-valid₁ : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a ∼ b → Γ ⊢Nf a ⇉ a ⋯ a
  ∼-valid₁ (∼-trans a∼b _) = ∼-valid₁ a∼b
  ∼-valid₁ (∼-⊥ b⇉b⋯b) = ⇉-⊥-f (Nf⇉-ctx b⇉b⋯b)
  ∼-valid₁ (∼-⊤ a⇉a⋯a) = a⇉a⋯a
  ∼-valid₁ (∼-∙ x⇉j j⇉as⇉k) = ⇉-s-i (⇉-∙ x⇉j (∼Sp-valid₁ j⇉as⇉k))
  ∼-valid₁ (∼-⟨| a⇉b⋯c) with Ne⇉-valid a⇉b⋯c
  ... | kd-⋯ b⇉b⋯b _ = b⇉b⋯b
  ∼-valid₁ (∼-|⟩ a⇉b⋯c) = ⇉-s-i a⇉b⋯c

  ∼Sp-valid₁ : ∀ {n} {Γ : Ctx n} {j as bs k} →
               Γ ⊢ j ⇉∙ as ∼ bs ⇉ k → Γ ⊢ j ⇉∙ as ⇉ k
  ∼Sp-valid₁ ∼-[] = ⇉-[]
  ∼Sp-valid₁ (∼-∷ c∼a a∼d a∼b j[x]⇉as⇉k) =
    ⇉-∷ (⇇-⇑ (∼-valid₁ a∼b) (<∷-⋯ c∼a a∼d)) (∼Sp-valid₁ j[x]⇉as⇉k)

-- We can push subkinding proofs through spine kindings/relations.

<∷-Sp⇉ : ∀ {n} {Γ : Ctx n} {j₁ j₂ as k₂} →
         Γ ⊢ j₁ <∷ j₂ → Γ ⊢ j₂ ⇉∙ as ⇉ k₂ → ∃ λ k₁ →
         Γ ⊢ j₁ ⇉∙ as ⇉ k₁ × Γ ⊢ k₁ <∷ k₂
<∷-Sp⇉ j₁<∷j₂ ⇉-[] = _ , ⇉-[] , j₁<∷j₂
<∷-Sp⇉ (<∷-Π b₁∼b₂ c₂∼c₁ j₁<∷j₂) (⇉-∷ a⇇b₂⋯c₂ j₂[a]⇉as⇉k₂) =
  let k₁ , j₁[a]⇉as⇉k₁ , k₁<∷k₂ = <∷-Sp⇉ (<∷-[] j₁<∷j₂ a⇇b₂⋯c₂) j₂[a]⇉as⇉k₂
  in  k₁ , ⇉-∷ (Nf⇇-⇑ a⇇b₂⋯c₂ (<∷-⋯ b₁∼b₂ c₂∼c₁)) j₁[a]⇉as⇉k₁ , k₁<∷k₂

<∷-Sp∼ : ∀ {n} {Γ : Ctx n} {j₁ j₂ as bs k₂} →
         Γ ⊢ j₁ <∷ j₂ → Γ ⊢ j₂ ⇉∙ as ∼ bs ⇉ k₂ → ∃ λ k₁ →
         Γ ⊢ j₁ ⇉∙ as ∼ bs ⇉ k₁ × Γ ⊢ k₁ <∷ k₂
<∷-Sp∼ j₁<∷j₂ ∼-[] = _ , ∼-[] , j₁<∷j₂
<∷-Sp∼ (<∷-Π c₁∼c₂ d₂∼d₁ j₁<∷j₂)
       (∼-∷ c₂∼a a∼d₂ a∼b j₂[a]⇉as∼bs⇉k₂) =
  let a⇇c₂⋯d₂ = ⇇-⇑ (∼-valid₁ a∼b) (<∷-⋯ c₂∼a a∼d₂)
      k₁ , j₁[a]⇉as∼bs⇉k₁ , k₁<∷k₂ = <∷-Sp∼ (<∷-[] j₁<∷j₂ a⇇c₂⋯d₂)
                                            j₂[a]⇉as∼bs⇉k₂
  in  k₁ , ∼-∷ (∼-trans c₁∼c₂ c₂∼a) (∼-trans a∼d₂ d₂∼d₁) a∼b j₁[a]⇉as∼bs⇉k₁ ,
      k₁<∷k₂

------------------------------------------------------------------------
-- Squashing of terms

mutual

  squashElim : ∀ {n} → Elim n → Elim n
  squashElim (a ∙ as) = squashHead a ∙ squashSpine as

  squashHead : ∀ {n} → Head n → Head n
  squashHead (var x) = var x
  squashHead ⊥       = ⊥
  squashHead ⊤       = ⊤
  {-# CATCHALL #-}
  squashHead a       = ⊤   -- all other types are squashed into ⊤

  squashSpine : ∀ {n} → Spine n → Spine n
  squashSpine []       = []
  squashSpine (a ∷ as) = squashElim a ∷ squashSpine as

  squashKind : ∀ {n} → Kind Elim n → Kind Elim n
  squashKind (a ⋯ b) = squashElim a ⋯ squashElim b
  squashKind (Π j k) = Π (squashKind j) (squashKind k)

squashAsc : ∀ {n} → ElimAsc n → ElimAsc n
squashAsc (kd k) = kd (squashKind k)
squashAsc (tp a) = tp (squashElim a)

squashCtx : ∀ {n} → Ctx n → Ctx n
squashCtx []      = []
squashCtx (a ∷ Γ) = (squashAsc a) ∷ (squashCtx Γ)

squashTerm : ∀ {n} → Term n → Term n
squashTerm a = ⌞ squashElim ⌜ a ⌝ ⌟

squash-++ : ∀ {n} (as : Spine n) {bs} →
            squashSpine as ++ squashSpine bs ≡ squashSpine (as ++ bs)
squash-++ []       = refl
squash-++ (a ∷ as) = cong (_ ∷_) (squash-++ as)

squash-∙∙ : ∀ {n} (a : Elim n) {bs} →
            squashElim a ∙∙ squashSpine bs ≡ squashElim (a ∙∙ bs)
squash-∙∙ (a ∙ as) = cong (_ ∙_) (squash-++ as)

-- Squashing commutes with generic substitutions.

module SquashSubstAppLemmas {T : ℕ → Set} (l : Lift T Term)
       (squashSub : ∀ {m n} → Sub T m n → Sub T m n)
       (squash-↑  : ∀ {m n} (σ : Sub T m n) →
          Lift._↑ l (squashSub σ) ≡ squashSub (Lift._↑ l σ))
       (squash-lift-lookup : ∀ {m n} (σ : Sub T m n) x →
          ⌜ Lift.lift l (Vec.lookup (squashSub σ) x) ⌝ ≡
          squashElim ⌜ Lift.lift l (Vec.lookup σ x) ⌝)
       where

  open SubstApp l

  -- Squashing commutes with application of generic substitutions.

  mutual

    squashElim-/ : ∀ {m n} {σ : Sub T m n} a →
                   squashElim a Elim/ squashSub σ ≡ squashElim (a Elim/ σ)
    squashElim-/ (a ∙ as) =
      trans (cong₂ _∙∙_ (squashHead-/ a) (squashSpine-/ as)) (squash-∙∙ _)

    squashHead-/ : ∀ {m n} {σ : Sub T m n} a →
                   squashHead a Head/ squashSub σ ≡ squashElim (a Head/ σ)
    squashHead-/ (var x) = squash-lift-lookup _ x
    squashHead-/ ⊥       = refl
    squashHead-/ ⊤       = refl
    squashHead-/ (Π k a) = refl
    squashHead-/ (a ⇒ b) = refl
    squashHead-/ (Λ k a) = refl
    squashHead-/ (ƛ a b) = refl
    squashHead-/ (a ⊡ b) = refl

    squashSpine-/ : ∀ {m n} {σ : Sub T m n} as →
                    squashSpine as // squashSub σ ≡ squashSpine (as // σ)
    squashSpine-/ []       = refl
    squashSpine-/ (a ∷ as) =
      cong₂ _∷_ (squashElim-/ a) (squashSpine-/ as)

    squashKind-/ : ∀ {m n} {σ : Sub T m n} k →
                   squashKind k Kind′/ squashSub σ ≡ squashKind (k Kind′/ σ)
    squashKind-/ (a ⋯ b) = cong₂ _⋯_ (squashElim-/ a) (squashElim-/ b)
    squashKind-/ (Π j k) =
      cong₂ Π (squashKind-/ j)
            (trans (cong (_ Kind′/_) (squash-↑ _)) (squashKind-/ k))

  squashAsc-/ : ∀ {m n} {σ : Sub T m n} a →
                squashAsc a ElimAsc/ squashSub σ ≡ squashAsc (a ElimAsc/ σ)
  squashAsc-/ (kd k) = cong kd (squashKind-/ k)
  squashAsc-/ (tp a) = cong tp (squashElim-/ a)

  squashTerm-/ : ∀ {m n} {σ : Sub T m n} a →
                 squashTerm a / squashSub σ ≡ squashTerm (a / σ)
  squashTerm-/ {σ = σ} a = begin
    ⌞ squashElim ⌜ a ⌝ ⌟ / squashSub σ      ≡˘⟨ ⌞⌟-/ (squashElim ⌜ a ⌝) ⟩
    ⌞ squashElim ⌜ a ⌝ Elim/ squashSub σ ⌟  ≡⟨ cong ⌞_⌟ (squashElim-/ ⌜ a ⌝) ⟩
    ⌞ squashElim (⌜ a ⌝ Elim/ σ) ⌟   ≡˘⟨ cong (⌞_⌟ ∘ squashElim) (⌜⌝-/ a) ⟩
    ⌞ squashElim ⌜ a / σ ⌝ ⌟         ∎
    where open ≡-Reasoning

-- Squashing commutes with renamings and term substitutions.

module SquashSubstLemmas where
  open Substitution
    using (termSubst; _↑; id; sub; weaken; _Kind′/_; _Kind′[_])
  open TermSubst termSubst using (varLift; termLift)
  open ≡-Reasoning

  open SquashSubstAppLemmas varLift (λ x → x) (λ _ → refl) (λ _ _ → refl)
    public using () renaming
    ( squashAsc-/  to squashAsc-/Var
    ; squashTerm-/ to squashTerm-/Var
    )

  -- Squashing applied point-wise to term substitutions.

  squashSub : ∀ {m n} → Sub Term m n → Sub Term m n
  squashSub = Vec.map squashTerm

  -- Helper lemmas about squashed substitutions.

  squash-↑ : ∀ {m n} (σ : Sub Term m n) → (squashSub σ) ↑ ≡ squashSub (σ ↑)
  squash-↑ σ = cong (_ ∷_) (begin
    Vec.map weaken (Vec.map squashTerm σ)  ≡˘⟨ map-∘ weaken squashTerm σ ⟩
    Vec.map (weaken ∘ squashTerm) σ        ≡⟨ map-cong squashTerm-/Var σ ⟩
    Vec.map (squashTerm ∘ weaken) σ        ≡⟨ map-∘ squashTerm weaken σ  ⟩
    Vec.map squashTerm (Vec.map weaken σ)  ∎)

  squash-lookup : ∀ {m n} (σ : Sub Term m n) x →
    ⌜ Vec.lookup (squashSub σ) x ⌝ ≡ squashElim ⌜ Vec.lookup σ x ⌝
  squash-lookup σ x = begin
      ⌜ Vec.lookup (squashSub σ) x ⌝
    ≡⟨ cong ⌜_⌝ (VecProps.lookup-map x squashTerm σ) ⟩
      ⌜ squashTerm (Vec.lookup σ x) ⌝
    ≡⟨ ⌜⌝∘⌞⌟-id (squashElim ⌜ Vec.lookup σ x ⌝) ⟩
      squashElim ⌜ Vec.lookup σ x ⌝
    ∎
  open SquashSubstAppLemmas termLift squashSub squash-↑ squash-lookup public

  squash-id : ∀ {n} → squashSub (id {n}) ≡ id
  squash-id {zero}  = refl
  squash-id {suc n} = cong (var zero ∷_) (begin
    Vec.map squashTerm (Vec.map weaken id)  ≡˘⟨ map-∘ squashTerm weaken id ⟩
    Vec.map (squashTerm ∘ weaken) id        ≡˘⟨ map-cong squashTerm-/Var id ⟩
    Vec.map (weaken ∘ squashTerm) id        ≡⟨ map-∘ weaken squashTerm id ⟩
    Vec.map weaken (Vec.map squashTerm id)  ≡⟨ cong (Vec.map weaken) squash-id ⟩
    Vec.map weaken id                       ∎)

  squash-sub : ∀ {n} (a : Term n) → squashSub (sub a) ≡ sub (squashTerm a)
  squash-sub a = cong (squashTerm a ∷_) squash-id

  -- Squashing commutes with single-variable substitutions in kinds.

  squashKind-[] : ∀ {n} k (a : Elim n) →
                  squashKind (k Kind′[ ⌞ a ⌟ ]) ≡
                    squashKind k Kind′[ ⌞ squashElim a ⌟ ]
  squashKind-[] k a = begin
      squashKind (k Kind′[ ⌞ a ⌟ ])
    ≡˘⟨ squashKind-/ k ⟩
      squashKind k Kind′/ squashSub (sub ⌞ a ⌟)
    ≡⟨ cong (squashKind k Kind′/_) (squash-sub ⌞ a ⌟) ⟩
      squashKind k Kind′[ squashTerm ⌞ a ⌟ ]
    ≡⟨ cong ((squashKind k Kind′[_]) ∘ ⌞_⌟ ∘ squashElim) (⌜⌝∘⌞⌟-id a) ⟩
      squashKind k Kind′[ ⌞ squashElim a ⌟ ]
    ∎

open Substitution using (weakenElimAsc)
open SquashSubstLemmas

-- Context lookup and conversion to vector representation commute with
-- squashing

toVec-squashCtx : ∀ {n} (Γ : Ctx n) →
                  toVec (squashCtx Γ) ≡ Vec.map squashAsc (toVec Γ)
toVec-squashCtx []      = refl
toVec-squashCtx (a ∷ Γ) = cong₂ _∷_ (squashAsc-/Var a) (begin
    Vec.map weakenElimAsc (toVec (squashCtx Γ))
  ≡⟨ cong (Vec.map weakenElimAsc) (toVec-squashCtx Γ) ⟩
    Vec.map weakenElimAsc (Vec.map squashAsc (toVec Γ))
  ≡˘⟨ map-∘ weakenElimAsc squashAsc (toVec Γ) ⟩
    Vec.map (weakenElimAsc ∘ squashAsc) (toVec Γ)
  ≡⟨ map-cong squashAsc-/Var (toVec Γ) ⟩
    Vec.map (squashAsc ∘ weakenElimAsc) (toVec Γ)
  ≡⟨ map-∘ squashAsc weakenElimAsc (toVec Γ) ⟩
    Vec.map squashAsc (Vec.map weakenElimAsc (toVec Γ))
  ∎)
  where open ≡-Reasoning

lookup-squashCtx : ∀ {n} (Γ : Ctx n) x →
                   lookup (squashCtx Γ) x ≡ squashAsc (lookup Γ x)
lookup-squashCtx {n} Γ x = begin
    Vec.lookup (toVec (squashCtx Γ)) x
  ≡⟨ cong (λ Δ → Vec.lookup Δ x) (toVec-squashCtx Γ) ⟩
    Vec.lookup (Vec.map squashAsc (toVec Γ)) x
  ≡⟨ VecProps.lookup-map x squashAsc (toVec Γ) ⟩
    squashAsc (Vec.lookup (toVec Γ) x)
  ∎
  where open ≡-Reasoning

------------------------------------------------------------------------
-- Predicates characterizing first-order kinds, bindings and contexts.

data FOKind {n} : Kind Elim n → Set where
  fo-⋯ : ∀ {a b}   → FOKind (a ⋯ b)
  fo-Π : ∀ {a b k} → FOKind k → FOKind (Π (a ⋯ b) k)

data FOAsc {n} : ElimAsc n → Set where
  fo-kd : ∀ {k} → FOKind k → FOAsc (kd k)

open ContextFormation (λ {n} Γ → FOAsc {n}) public using () renaming
  ( _wf to FOCtx; [] to fo-[]; _∷_ to fo-∷
  ; WellFormedWeakenOps to FOWeakenOps)

<∷-FOKind₂ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → FOKind k
<∷-FOKind₂ (<∷-⋯ _ _)      = fo-⋯
<∷-FOKind₂ (<∷-Π _ _ j<∷k) = fo-Π (<∷-FOKind₂ j<∷k)

module FOSubstAppLemmas {T : ℕ → Set} (l : Lift T Term) where
  open SubstApp l

  FOKind-/ : ∀ {m n k} {σ : Sub T m n} → FOKind k → FOKind (k Kind′/ σ)
  FOKind-/ fo-⋯        = fo-⋯
  FOKind-/ (fo-Π k-fo) = fo-Π (FOKind-/ k-fo)

  FOAsc-/ : ∀ {m n a} {σ : Sub T m n} → FOAsc a → FOAsc (a ElimAsc/ σ)
  FOAsc-/ (fo-kd k-fo) = fo-kd (FOKind-/ k-fo)

module FOSubstLemmas where
  open Substitution using (termSubst)
  open TermSubst termSubst using (varLift; termLift)

  open FOSubstAppLemmas varLift public using ()
    renaming (FOKind-/ to FOKind-/Var; FOAsc-/ to FOAsc-/Var)
  open FOSubstAppLemmas termLift public

  FOAsc-weaken : ∀ {n} {a : ElimAsc n} → FOAsc a → FOAsc (weakenElimAsc a)
  FOAsc-weaken a-fo = FOAsc-/Var a-fo

open FOSubstLemmas

foWeakenOps : FOWeakenOps weakenOps
foWeakenOps = record { wf-weaken = λ _ → FOAsc-weaken }
open FOWeakenOps foWeakenOps public using () renaming (lookup to lookup-FOAsc)

lookup-FOKind : ∀ {m} {Γ : Ctx m} {k} x →
                FOCtx Γ → ElimCtx.lookup Γ x ≡ kd k → FOKind k
lookup-FOKind x Γ-fo Γ[x]≡kd-a with subst FOAsc Γ[x]≡kd-a (lookup-FOAsc Γ-fo x)
... | fo-kd k-fo = k-fo

------------------------------------------------------------------------
-- Reduction of canonical judgments to their reduced forms

open Substitution hiding (subst)

mutual

  reduce-ctx : ∀ {n} {Γ : Ctx n} → FOCtx (squashCtx Γ) →
               Γ C.ctx → squashCtx Γ ctx
  reduce-ctx fo-[] C.[]                        = []
  reduce-ctx (fo-∷ a-fo Γ-fo) (a-wf C.∷ Γ-ctx) =
    reduce-wf Γ-fo a-fo a-wf ∷ reduce-ctx Γ-fo Γ-ctx

  reduce-wf : ∀ {n} {Γ : Ctx n} {a} →
              FOCtx (squashCtx Γ) → FOAsc (squashAsc a) →
              Γ C.⊢ a wf → squashCtx Γ ⊢ squashAsc a wf
  reduce-wf Γ-fo (fo-kd k-fo) (C.wf-kd k-kd)  =
    wf-kd (reduce-kd Γ-fo k-fo k-kd)
  reduce-wf Γ-fo _ (C.wf-tp a⇉a⋯a) = wf-tp (reduce-Nf⇉ Γ-fo a⇉a⋯a)

  reduce-kd : ∀ {n} {Γ : Ctx n} {k} →
              FOCtx (squashCtx Γ) → FOKind (squashKind k) →
              Γ C.⊢ k kd → squashCtx Γ ⊢ squashKind k kd
  reduce-kd Γ-fo _ (C.kd-⋯ a⇉a⋯a b⇉b⋯b) =
    kd-⋯ (reduce-Nf⇉ Γ-fo a⇉a⋯a) (reduce-Nf⇉ Γ-fo b⇉b⋯b)
  reduce-kd Γ-fo (fo-Π k-fo) (C.kd-Π (C.kd-⋯ a⇉a⋯a b⇉b⋯b) k-kd) =
    kd-Π (reduce-Nf⇉ Γ-fo a⇉a⋯a) (reduce-Nf⇉ Γ-fo b⇉b⋯b)
         (reduce-kd (fo-∷ (fo-kd fo-⋯) Γ-fo) k-fo k-kd)
  reduce-kd Γ-fo () (C.kd-Π (C.kd-Π _ _) k-kd)

  reduce-Var∈ : ∀ {n} {Γ : Ctx n} {x k} → FOCtx (squashCtx Γ) →
                Γ C.⊢Var x ∈ k → ∃ λ j →
                squashCtx Γ ⊢Var x ⇉ j × squashCtx Γ ⊢ j <∷ squashKind k
  reduce-Var∈ {_} {Γ} Γ-fo (C.⇉-var x Γ-ctx Γ[x]≡kd-j₁) =
    let Γ-ctx′      = reduce-ctx Γ-fo Γ-ctx
        Γ[x]≡kd-j₁′ = trans (lookup-squashCtx Γ x) (cong squashAsc Γ[x]≡kd-j₁)
    in _ , ⇉-var x Γ-ctx′ Γ[x]≡kd-j₁′ ,
       <∷-refl (lookup-kd x Γ-ctx′ Γ[x]≡kd-j₁′)
  reduce-Var∈ Γ-fo (C.⇇-⇑ x∈k₁ k₁<∷k₂ _) =
    let j , x∈j , j<∷k₁ = reduce-Var∈ Γ-fo x∈k₁
    in  j , x∈j , <∷-trans j<∷k₁ (reduce-<∷ Γ-fo (<∷-FOKind₂ j<∷k₁) k₁<∷k₂)

  reduce-Ne∈ : ∀ {n} {Γ : Ctx n} {a b c} → FOCtx (squashCtx Γ) →
               Γ C.⊢Ne a ∈ (b ⋯ c) →
               squashCtx Γ ⊢Nf squashElim a ⇇ squashKind (b ⋯ c)
  reduce-Ne∈ {_} {Γ} Γ-fo (C.∈-∙ {as = as} x∈j₂ j₂⇉as⇉b₂⋯c₂) =
    let j₁ , x⇉j₁ , j₁<∷j₂ = reduce-Var∈ Γ-fo x∈j₂
        j₂-fo              = <∷-FOKind₂ j₁<∷j₂
        j₂⇉as⇉b₂⋯c₂′       = reduce-Sp⇉ Γ-fo j₂-fo j₂⇉as⇉b₂⋯c₂
        k₁ , j₁⇉as⇉k₁ , k₁<∷b₂⋯c₂        = <∷-Sp⇉ j₁<∷j₂ j₂⇉as⇉b₂⋯c₂′
        _ , _ , b₂∼b₁ , c₁∼c₂ , k₁≡b₁⋯c₁ = <∷-⋯-inv k₁<∷b₂⋯c₂
        j₁⇉as⇉b₁⋯c₁ = subst (squashCtx Γ ⊢ j₁ ⇉∙ squashSpine as ⇉_)
                            k₁≡b₁⋯c₁ j₁⇉as⇉k₁
    in Nf⇇-⇑ (Nf⇇-ne (⇉-∙ x⇉j₁ j₁⇉as⇉b₁⋯c₁)) (<∷-⋯ b₂∼b₁ c₁∼c₂)

  reduce-Nf⇉ : ∀ {n} {Γ : Ctx n} {a b c} → FOCtx (squashCtx Γ) →
               Γ C.⊢Nf a ⇉ b ⋯ c →
               squashCtx Γ ⊢Nf squashElim a ⇉ squashElim b ⋯ squashElim c
  reduce-Nf⇉ Γ-fo (C.⇉-⊥-f Γ-ctx)   = ⇉-⊥-f (reduce-ctx Γ-fo Γ-ctx)
  reduce-Nf⇉ Γ-fo (C.⇉-⊤-f Γ-ctx)   = ⇉-⊤-f (reduce-ctx Γ-fo Γ-ctx)
  reduce-Nf⇉ Γ-fo (C.⇉-∀-f k-kd _)  =
    ⇉-⊤-f (reduce-kd-ctx Γ-fo k-kd)
  reduce-Nf⇉ Γ-fo (C.⇉-→-f a⇉a⋯a _) =
    ⇉-⊤-f (Nf⇉-ctx (reduce-Nf⇉ Γ-fo a⇉a⋯a))
  reduce-Nf⇉ Γ-fo (C.⇉-s-i (C.∈-∙ x∈j j⇉as⇉b⋯c))
    with reduce-Ne∈ Γ-fo (C.∈-∙ x∈j j⇉as⇉b⋯c)
  ... | ⇇-⇑ (⇉-s-i x∙as∈b′⋯c′) (<∷-⋯ _ _) = ⇉-s-i x∙as∈b′⋯c′

  reduce-Nf⇇ : ∀ {n} {Γ : Ctx n} {a b c} → FOCtx (squashCtx Γ) →
               Γ C.⊢Nf a ⇇ b ⋯ c →
               squashCtx Γ ⊢Nf squashElim a ⇇ squashElim b ⋯ squashElim c
  reduce-Nf⇇ Γ-fo (C.⇇-⇑ a⇉b₁⋯c₁ (C.<∷-⋯ b₂<:b₁ c₁<:c₂)) =
    ⇇-⇑ (reduce-Nf⇉ Γ-fo a⇉b₁⋯c₁)
        (<∷-⋯ (reduce-<: Γ-fo b₂<:b₁) (reduce-<: Γ-fo c₁<:c₂))

  reduce-Sp⇉ : ∀ {n} {Γ : Ctx n} {j as k} →
               FOCtx (squashCtx Γ) → FOKind (squashKind j) →
               Γ C.⊢ j ⇉∙ as ⇉ k →
               squashCtx Γ ⊢ squashKind j ⇉∙ squashSpine as ⇉ squashKind k
  reduce-Sp⇉ Γ-fo _ C.⇉-[]                  = ⇉-[]
  reduce-Sp⇉ Γ-fo (fo-Π k-fo)
             (C.⇉-∷ {a} {as} {b ⋯ c} {k} a⇇b⋯c _ k[a∈★]⇉as⇉l) =
    let k[a∈★]≡k[a] = trans (cong squashKind (Kind/⟨★⟩-/ k))
                            (squashKind-[] k a)
        k[a∈★]-fo   = subst FOKind (sym k[a∈★]≡k[a])
                            (FOKind-/ {σ = sub ⌞ squashElim a ⌟} k-fo)
    in ⇉-∷ (reduce-Nf⇇ Γ-fo a⇇b⋯c)
           (subst (_ ⊢_⇉∙ _ ⇉ _) k[a∈★]≡k[a]
                  (reduce-Sp⇉ Γ-fo k[a∈★]-fo k[a∈★]⇉as⇉l))

  reduce-<∷ : ∀ {n} {Γ : Ctx n} {j k} →
              FOCtx (squashCtx Γ) → FOKind (squashKind j) →
              Γ C.⊢ j <∷ k → squashCtx Γ ⊢ squashKind j <∷ squashKind k
  reduce-<∷ Γ-fo a₁⋯a₂-fo (C.<∷-⋯ a₂<:a₁ b₁<:b₂) =
    <∷-⋯ (reduce-<: Γ-fo a₂<:a₁) (reduce-<: Γ-fo b₁<:b₂)
  reduce-<∷ Γ-fo (fo-Π k₁-fo) (C.<∷-Π (C.<∷-⋯ a₁<:a₂ b₂<:b₁) k₁<∷k₂ bb) =
    <∷-Π (reduce-<: Γ-fo a₁<:a₂) (reduce-<: Γ-fo b₂<:b₁)
         (reduce-<∷ (fo-∷ (fo-kd fo-⋯) Γ-fo) k₁-fo k₁<∷k₂)

  reduce-<: : ∀ {n} {Γ : Ctx n} {a b} → FOCtx (squashCtx Γ) →
              Γ C.⊢ a <: b → squashCtx Γ ⊢ squashElim a ∼ squashElim b
  reduce-<: Γ-fo (C.<:-trans a<:b b<:c) =
    ∼-trans (reduce-<: Γ-fo a<:b) (reduce-<: Γ-fo b<:c)
  reduce-<: Γ-fo (C.<:-⊥ b⇉b⋯b) = ∼-⊥ (reduce-Nf⇉ Γ-fo b⇉b⋯b)
  reduce-<: Γ-fo (C.<:-⊤ a⇉a⋯a) = ∼-⊤ (reduce-Nf⇉ Γ-fo a⇉a⋯a)
  reduce-<: Γ-fo (C.<:-∀ _ _ ∀ka⇉⋯) =
    ∼-⊤ (⇉-⊤-f (Nf⇉-ctx (reduce-Nf⇉ Γ-fo ∀ka⇉⋯)))
  reduce-<: Γ-fo (C.<:-→ a₂<:a₁ _) =
    ∼-⊤ (⇉-⊤-f (∼-ctx (reduce-<: Γ-fo a₂<:a₁)))
  reduce-<: {_} {Γ} Γ-fo (C.<:-∙ {as₁ = as} {bs} x∈j₂ j₂⇉as∼bs⇉c₂⋯d₂) =
    let j₁ , x⇉j₁ , j₁<∷j₂ = reduce-Var∈ Γ-fo x∈j₂
        j₂-fo              = <∷-FOKind₂ j₁<∷j₂
        j₂⇉as∼bs⇉c₂⋯d₂′    = reduce-Sp≃ Γ-fo j₂-fo j₂⇉as∼bs⇉c₂⋯d₂
        k₁ , j₁⇉as∼bs⇉k₁ , k₁<∷c₂⋯d₂ = <∷-Sp∼ j₁<∷j₂ j₂⇉as∼bs⇉c₂⋯d₂′
        _ , _ , _ , _ , k₁≡c₁⋯d₁     = <∷-⋯-inv k₁<∷c₂⋯d₂
        j₁⇉as∼bs⇉c₁⋯d₁ = subst (squashCtx Γ ⊢ j₁ ⇉∙ squashSpine as ∼
                                                    squashSpine bs ⇉_)
                               k₁≡c₁⋯d₁ j₁⇉as∼bs⇉k₁
    in ∼-∙ x⇉j₁ j₁⇉as∼bs⇉c₁⋯d₁
  reduce-<: Γ-fo (C.<:-⟨| b∈a⋯c) with reduce-Ne∈ Γ-fo b∈a⋯c
  ... | b⇇a⋯c = ∼-⟨|-Nf⇇ b⇇a⋯c
  reduce-<: Γ-fo (C.<:-|⟩ a∈c⋯b) with reduce-Ne∈ Γ-fo a∈c⋯b
  ... | a⇇c⋯b = ∼-|⟩-Nf⇇ a⇇c⋯b

  reduce-Sp≃ : ∀ {n} {Γ : Ctx n} {j as bs k} →
               FOCtx (squashCtx Γ) → FOKind (squashKind j) →
               Γ C.⊢ j ⇉∙ as ≃ bs ⇉ k →
               squashCtx Γ ⊢ squashKind j ⇉∙ squashSpine as ∼
                                             squashSpine bs ⇉ squashKind k
  reduce-Sp≃ Γ-fo _ C.≃-[] = ∼-[]
  reduce-Sp≃ Γ-fo (fo-Π k-fo)
             (C.≃-∷ {j = c ⋯ d}
                    (C.<:-antisym _
                      (C.<:-⇇ (C.⇇-⇑ a⇉c₁⋯d₁ (C.<∷-⋯ _ _)) _ a<:b) _)
                    k[a∈★]⇉as≃bs⇉l)
             with C.Nf⇉-≡ a⇉c₁⋯d₁
  reduce-Sp≃ Γ-fo (fo-Π k-fo)
             (C.≃-∷ {a} {as} {b} {bs} {c ⋯ d} {k}
                    (C.<:-antisym _
                      (C.<:-⇇ (C.⇇-⇑ a⇉a⋯a (C.<∷-⋯ c<:a a<:d)) _ a<:b) _)
                    k[a∈★]⇉as≃bs⇉l)
             | refl , refl =
    let k[a∈★]≡k[a] = trans (cong squashKind (Kind/⟨★⟩-/ k))
                            (squashKind-[] k a)
        k[a∈★]-fo   = subst FOKind (sym k[a∈★]≡k[a])
                            (FOKind-/ {σ = sub ⌞ squashElim a ⌟} k-fo)
    in ∼-∷ (reduce-<: Γ-fo c<:a) (reduce-<: Γ-fo a<:d)
           (reduce-<: Γ-fo a<:b)
           (subst (_ ⊢_⇉∙ _ ∼ _ ⇉ _) k[a∈★]≡k[a]
                  (reduce-Sp≃ Γ-fo k[a∈★]-fo k[a∈★]⇉as≃bs⇉l))

  -- A helper to satisfy the termination checker.

  reduce-kd-ctx : ∀ {n} {Γ : Ctx n} {k} →
                  FOCtx (squashCtx Γ) → Γ C.⊢ k kd → squashCtx Γ ctx
  reduce-kd-ctx Γ-fo (C.kd-⋯ a⇉a⋯a _) = Nf⇉-ctx (reduce-Nf⇉ Γ-fo a⇉a⋯a)
  reduce-kd-ctx Γ-fo (C.kd-Π j-kd _)  = reduce-kd-ctx Γ-fo j-kd

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda