text:
------------------------------------------------------------------------
-- Syntax of Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Syntax where

open import Algebra using (Monoid)
import Data.Context as Context
open import Data.Context.Properties
open import Data.Fin using (Fin; suc; zero)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (ℕ; suc; zero)
open import Data.Product using (proj₂)
open import Data.Vec as Vec using ([]; _∷_)
open import Data.List as List using (List; []; _∷_; foldl; map; _++_; _∷ʳ_)
open import Data.List.Properties using (++-monoid)
import Data.Maybe as Maybe
open import Function using (_∘_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_)
open import Relation.Binary.PropositionalEquality as P hiding ([_])
open P.≡-Reasoning

----------------------------------------------------------------------
-- Raw terms: untyped syntax of terms, types and kinds.

-- NOTE 1.  Following the style of Pure Type System (PTS), we define
-- raw (i.e. untyped/unkinded) terms and types as a single syntactic
-- category rather than distinguishing them syntactically.
-- Concretely, we use the singe datatype Term to represent raw terms
-- and types.  This simplifies the definition of substitution in types
-- and terms as we don't need to distinguish between type and term
-- variables.  The difference between terms and types becomes manifest
-- only later in (sub-)typing and (sub-)kinding judgments.  However,
-- unlike PTS, we *do* treat kinds as a separate syntactic
-- category/datatype because there are no kind variables.  This
-- simplifies some definitions and proofs that rely on the syntactic
-- structure of kinds (e.g. kind simplification and related
-- properties).
--
-- NOTE 2.  We use well-scoped de Bruijn indexing to represent term
-- and type variables in raw terms/types.  The datatype `Term' is
-- indexed by the number of free variables its inhabitants may
-- contain, i.e. given a raw term
--
--    a : Term n
--
-- the set of "names" that may appear in `a' is
--
--   { 0, 1, ..., n-1 }.
--
-- Binders extend this set by increasing n by one for each fresh name
-- they introduce.  This ensures that raw terms are intrinsically
-- well-scoped.  This representation was adapted from previous Agda
-- formalizations of typed lambda calculi by Danielsson and others [1,
-- 2] and comes with some support in the Agda standard library.  See
-- Data.Fin.Substitution.Example for a simple example.
--
--  [1] N. A. Danielsson and T. Altenkirch, "Subtyping, Declaratively
--      An Exercise in Mixed Induction and Coinduction", Proc. MPC
--      2010.
--
--  [2] N. A. Danielsson, "Operational Semantics Using the Partiality
--      Monad", Proc. ICFP 2012.

module Syntax where

  infixl 9 _·_ _⊡_ _⊡∙_
  infixr 7 _⇒_ _⇒∙_
  infix  6 _⋯_

  -- Raw, T-dependent kinds with up to n free variables.

  data Kind (T : ℕ → Set) (n : ℕ) : Set where
    _⋯_ : (a b : T n)                         → Kind T n  -- interval
    Π   : (j : Kind T n) (k : Kind T (suc n)) → Kind T n  -- dependent arrow

  -- Raw terms and types with up to n free variables.
  --
  -- NOTE. The type instantiation operator _⊡_ should be considered
  -- specialized variant of the application operator _·_.  The reason
  -- for including a dedicated _⊡_ constructor is to distinguish term
  -- applications from type applications/instantiations in CBV
  -- reductions (see FOmegaInt.Reduction.Cbv).  Without the special
  -- treatment of type instantiation, CBV reduction would permit
  -- reduction of type arguments before contraction.  Not only is this
  -- counter to the usual CBV semantics for Fω (see e.g. TAPL p. 450),
  -- but it would require a proof of subject reduction (aka
  -- preservation) for kinding in order to prove preservation of
  -- typing even under CBV reduction.  By adopting the usual CBV
  -- semantics, this dependency can be avoided.  See
  -- FOmegaInt.Typing.Preservation for a proof of subject reduction
  -- for typing using the usual CBV semantics.

  data Term (n : ℕ) : Set where
    var : (x : Fin n)                          → Term n  -- variable
    ⊥   :                                        Term n  -- bottom (minimum)
    ⊤   :                                        Term n  -- top (maximum)
    Π   : (k : Kind Term n) (a : Term (suc n)) → Term n  -- universal quant.
    _⇒_ : (a b : Term n)                       → Term n  -- arrow
    Λ   : (k : Kind Term n) (a : Term (suc n)) → Term n  -- type abstraction
    ƛ   : (a : Term n)      (b : Term (suc n)) → Term n  -- term abstraction
    _⊡_ : (a b : Term n)                       → Term n  -- type instantiation
    _·_ : (a b : Term n)                       → Term n  -- term application

  -- A shorthand for the kind of proper types.

  * : ∀ {n} → Kind Term n
  * = ⊥ ⋯ ⊤

  infixl 9 _∙_

  -- Raw terms and types in spine form.
  --
  -- Spine form is an alternative representation of raw terms where
  -- the arguments of consecutive applications are grouped together
  -- into sequences of arguments called "spines".  This representation
  -- is better suited for the definition of "hereditary substitution"
  -- (see Syntax.HereditarySubstitution) and canonical kinding (see
  -- Kinding.Canonical).  The two representations are isomorphic, as
  -- witnessed by ⌜⌝∘⌞⌟-id and ⌞⌟∘⌜⌝-id below.
  --
  -- NOTE.  Below, we consider type instantiations (a ⊡ b) as heads
  -- rather than eliminations, despite the fact that, semantically,
  -- they are elimination forms.  However, for the purpose of
  -- hereditary substitution we will ignore their semantics and treat
  -- _⊡_ as an uninterpreted binary operation.  This is justified by
  -- the fact that *well-kinded* hereditary substitution is only
  -- defined on (well-kinded) types, in which _⊡_ cannot appear.
  --
  -- One may wonder: why include constructors for term-level forms
  -- such as ƛ or _⊡_ in this presentation of the syntax if it is only
  -- used to define type-level hereditary substitution?  The answer is
  -- that we often rely on the two presentations of the syntax being
  -- isomorphic to switch between them without loss of generality.  If
  -- we only included type formers, we could not prove this
  -- isomorphism.  Including the term formers thus adds a bit of
  -- overhead but simplifies things over all.

  mutual

    -- Eliminations are applications of (possibly empty) sequences of
    -- arguments to heads.

    data Elim (n : ℕ) : Set where
      _∙_ : (a : Head n) (as : Spine n) → Elim n  -- application

    -- Heads are those terms that are not eliminations.

    data Head (n : ℕ) : Set where
      var : (x : Fin n)                          → Head n  -- variable
      ⊥   :                                        Head n  -- bottom (minimum)
      ⊤   :                                        Head n  -- top (maximum)
      Π   : (k : Kind Elim n) (a : Elim (suc n)) → Head n  -- universal
      _⇒_ : (a b : Elim n)                       → Head n  -- arrow
      Λ   : (k : Kind Elim n) (a : Elim (suc n)) → Head n  -- type abstraction
      ƛ   : (a : Elim n)      (b : Elim (suc n)) → Head n  -- term abstraction
      _⊡_ : (a b : Elim n)                       → Head n  -- type inst.

    -- Spines are (possibly empty) sequences of eliminations.

    Spine : ℕ → Set
    Spine n = List (Elim n)

  -- Projections.

  headOf : ∀ {n} → Elim n → Head n
  headOf (a ∙ as) = a

  spineOf : ∀ {n} → Elim n → Spine n
  spineOf (a ∙ as) = as

  infixl 9 _⌜·⌝_ _⌞∙⌟_ _∙∙_

  -- Post-application of spines and eliminations to eliminations.

  _∙∙_ : ∀ {n} → Elim n → Spine n → Elim n
  a ∙ as ∙∙ bs = a ∙ (as ++ bs)

  _⌜·⌝_ : ∀ {n} → Elim n → Elim n → Elim n
  a ⌜·⌝ b = a ∙∙ (b ∷ [])

  -- Application of term sequences to terms.

  _⌞∙⌟_ : ∀ {n} → Term n → List (Term n) → Term n
  a ⌞∙⌟ as = foldl _·_ a as

  -- Shorthands for "unapplied" term/type constructors.

  var∙ : ∀ {n} → Fin n → Elim n
  var∙ x = var x ∙ []

  ⊥∙ : ∀ {n} → Elim n
  ⊥∙ = ⊥ ∙ []

  ⊤∙ : ∀ {n} → Elim n
  ⊤∙ = ⊤ ∙ []

  ∀∙ : ∀ {n} → Kind Elim n → Elim (suc n) → Elim n
  ∀∙ k a = Π k a ∙ []

  _⇒∙_ : ∀ {n} → Elim n → Elim n → Elim n
  a ⇒∙ b = (a ⇒ b) ∙ []

  Λ∙ : ∀ {n} → Kind Elim n → Elim (suc n) → Elim n
  Λ∙ k a = Λ k a ∙ []

  ƛ∙ : ∀ {n} → Elim n → Elim (suc n) → Elim n
  ƛ∙ a b = ƛ a b ∙ []

  _⊡∙_ : ∀ {n} → Elim n → Elim n → Elim n
  a ⊡∙ b = (a ⊡ b) ∙ []

  ⌜*⌝ : ∀ {n} → Kind Elim n
  ⌜*⌝ = ⊥∙ ⋯ ⊤∙

  -- Conversions between the two representations.

  mutual

    -- Turn raw eliminations into raw terms.

    ⌞_⌟ : ∀ {n} → Elim n → Term n
    ⌞ a ∙ as ⌟ = ⌞ a ⌟Hd ⌞∙⌟ ⌞ as ⌟Sp

    ⌞_⌟Kd : ∀ {n} → Kind Elim n → Kind Term n
    ⌞ a ⋯ b ⌟Kd = ⌞ a ⌟ ⋯ ⌞ b ⌟
    ⌞ Π j k ⌟Kd = Π ⌞ j ⌟Kd ⌞ k ⌟Kd

    ⌞_⌟Sp : ∀ {n} → Spine n → List (Term n)
    ⌞ []     ⌟Sp = []
    ⌞ a ∷ as ⌟Sp = ⌞ a ⌟ ∷ ⌞ as ⌟Sp

    ⌞_⌟Hd : ∀ {n} → Head n → Term n
    ⌞ var x ⌟Hd = var x
    ⌞ ⊥     ⌟Hd = ⊥
    ⌞ ⊤     ⌟Hd = ⊤
    ⌞ Π k a ⌟Hd = Π ⌞ k ⌟Kd ⌞ a ⌟
    ⌞ a ⇒ b ⌟Hd = ⌞ a ⌟ ⇒ ⌞ b ⌟
    ⌞ Λ k a ⌟Hd = Λ ⌞ k ⌟Kd ⌞ a ⌟
    ⌞ ƛ a b ⌟Hd = ƛ ⌞ a ⌟ ⌞ b ⌟
    ⌞ a ⊡ b ⌟Hd = ⌞ a ⌟ ⊡ ⌞ b ⌟

  mutual

    -- Turn raw terms into raw eliminations.

    ⌜_⌝ : ∀ {n} → Term n → Elim n
    ⌜ var x ⌝ = var x ∙ []
    ⌜ ⊥     ⌝ = ⊥∙
    ⌜ ⊤     ⌝ = ⊤∙
    ⌜ Π k a ⌝ = ∀∙ ⌜ k ⌝Kd ⌜ a ⌝
    ⌜ a ⇒ b ⌝ = ⌜ a ⌝ ⇒∙ ⌜ b ⌝
    ⌜ Λ k a ⌝ = Λ∙ ⌜ k ⌝Kd ⌜ a ⌝
    ⌜ ƛ a b ⌝ = ƛ∙ ⌜ a ⌝ ⌜ b ⌝
    ⌜ a ⊡ b ⌝ = ⌜ a ⌝ ⊡∙ ⌜ b ⌝
    ⌜ a · b ⌝ = ⌜ a ⌝ ⌜·⌝ ⌜ b ⌝

    ⌜_⌝Kd : ∀ {n} → Kind Term n → Kind Elim n
    ⌜ a ⋯ b ⌝Kd = ⌜ a ⌝ ⋯ ⌜ b ⌝
    ⌜ Π j k ⌝Kd = Π ⌜ j ⌝Kd ⌜ k ⌝Kd

  -- Shapes (aka simple kinds).

  data SKind : Set where
    ★   : SKind
    _⇒_ : SKind → SKind → SKind

  -- Kind simplification (aka erasure from kinds to shapes).

  ⌊_⌋ : ∀ {T n} → Kind T n → SKind
  ⌊ a ⋯ b ⌋ = ★
  ⌊ Π j k ⌋ = ⌊ j ⌋ ⇒ ⌊ k ⌋

  -- A wrapper for raw kind or type ascriptions.

  data KdOrTp (T : ℕ → Set) (n : ℕ) : Set where
    kd : Kind T n → KdOrTp T n
    tp : T n      → KdOrTp T n

  TermAsc = KdOrTp Term
  ElimAsc = KdOrTp Elim

  ⌞_⌟Asc : ∀ {n} → ElimAsc n → TermAsc n
  ⌞ kd k ⌟Asc = kd ⌞ k ⌟Kd
  ⌞ tp a ⌟Asc = tp ⌞ a ⌟

  ⌜_⌝Asc : ∀ {n} → TermAsc n → ElimAsc n
  ⌜ kd k ⌝Asc = kd ⌜ k ⌝Kd
  ⌜ tp a ⌝Asc = tp ⌜ a ⌝

open Syntax

----------------------------------------------------------------------
-- Some properties of raw terms and kinds

-- The kd constructor is injective.

kd-inj : ∀ {T n} {j k : Kind T n} → kd j ≡ kd k → j ≡ k
kd-inj refl = refl

-- Extensionality of eliminations.

∙-ext : ∀ {n} (a : Elim n) → headOf a ∙ spineOf a ≡ a
∙-ext (a ∙ as) = refl

-- The empty spine is a right unit of _∙∙_

∙∙-[] : ∀ {n} (a : Elim n) → a ∙∙ [] ≡ a
∙∙-[] (a ∙ as) = cong (a ∙_) (proj₂ identity as)
  where open Monoid (++-monoid (Elim _)) hiding (_∙_)

-- Spine application commutes with spine concatenation.

∙∙-++ : ∀ {n} (a : Elim n) bs cs → a ∙∙ bs ∙∙ cs ≡ a ∙∙ (bs ++ cs)
∙∙-++ (a ∙ as) bs cs = cong (a ∙_) (assoc as bs cs)
  where open Monoid (++-monoid (Elim _)) hiding (_∙_)

-- Spine application can be expressed as a left fold.

∙∙IsFold : ∀ {n} (a : Elim n) bs → a ∙∙ bs ≡ foldl _⌜·⌝_ a bs
∙∙IsFold (a ∙ as) []       = ∙∙-[] (a ∙ as)
∙∙IsFold (a ∙ as) (b ∷ bs) = begin
    a ∙ (as ++ b ∷ bs)
  ≡⟨ sym (∙∙-++ (a ∙ as) (b ∷ []) bs) ⟩
    a ∙ ((as ∷ʳ b) ++ bs)
  ≡⟨ ∙∙IsFold (a ∙ (as ∷ʳ b)) bs  ⟩
    foldl _⌜·⌝_ (a ∙ (as ∷ʳ b)) bs
  ∎

-- Conversion to raw terms commutes with (post-)application.

⌞⌟-· : ∀ {n} (a : Elim n) b → ⌞ a ⌜·⌝ b ⌟ ≡ ⌞ a ⌟ · ⌞ b ⌟
⌞⌟-· (a ∙ as) b = helper as b
  where
    helper : ∀ {n} {a : Term n} bs c →
             a ⌞∙⌟ ⌞ bs ∷ʳ c ⌟Sp ≡ a ⌞∙⌟ ⌞ bs ⌟Sp · ⌞ c ⌟
    helper []       c = refl
    helper (b ∷ bs) c = helper bs c

⌞⌟-∙∙ : ∀ {n} (a : Elim n) bs → ⌞ a ∙∙ bs ⌟ ≡ ⌞ a ⌟ ⌞∙⌟ ⌞ bs ⌟Sp
⌞⌟-∙∙ a []       = cong ⌞_⌟ (∙∙-[] a)
⌞⌟-∙∙ a (b ∷ bs) = begin
  ⌞ a ∙∙ (b ∷ bs) ⌟      ≡⟨ sym (cong ⌞_⌟ (∙∙-++ a (b ∷ []) bs)) ⟩
  ⌞ a ∙∙ (b ∷ []) ∙∙ bs ⌟          ≡⟨ ⌞⌟-∙∙ (a ∙∙ (b ∷ [])) bs ⟩
  ⌞ a ∙∙ (b ∷ []) ⌟ ⌞∙⌟ ⌞ bs ⌟Sp   ≡⟨ cong (_⌞∙⌟ ⌞ bs ⌟Sp) (⌞⌟-· a b) ⟩
  ⌞ a ⌟ · ⌞ b ⌟ ⌞∙⌟ ⌞ bs ⌟Sp  ∎

-- Conversion to eliminations commutes with spine application.

⌜⌝-∙ : ∀ {n} (a : Term n) bs → ⌜ a ⌞∙⌟ bs ⌝ ≡ ⌜ a ⌝ ∙∙ map ⌜_⌝ bs
⌜⌝-∙ a bs = begin
  ⌜ a ⌞∙⌟ bs ⌝                     ≡⟨ helper a bs ⟩
  foldl _⌜·⌝_ ⌜ a ⌝ (map ⌜_⌝ bs)   ≡⟨ sym (∙∙IsFold ⌜ a ⌝ (map ⌜_⌝ bs)) ⟩
  ⌜ a ⌝ ∙∙ map ⌜_⌝ bs              ∎
  where
    helper : ∀ {n} (a : Term n) bs →
             ⌜ a ⌞∙⌟ bs ⌝ ≡ foldl _⌜·⌝_ ⌜ a ⌝ (map ⌜_⌝ bs)
    helper a []       = refl
    helper a (b ∷ bs) = helper (a · b) bs

-- The two representations of raw terms are isomorphic.

mutual

  ⌞⌟∘⌜⌝-id : ∀ {n} (a : Term n) → ⌞ ⌜ a ⌝ ⌟ ≡ a
  ⌞⌟∘⌜⌝-id (var x) = refl
  ⌞⌟∘⌜⌝-id ⊥       = refl
  ⌞⌟∘⌜⌝-id ⊤       = refl
  ⌞⌟∘⌜⌝-id (Π k a) = cong₂ Π (⌞⌟Kd∘⌜⌝Kd-id k) (⌞⌟∘⌜⌝-id a)
  ⌞⌟∘⌜⌝-id (a ⇒ b) = cong₂ _⇒_ (⌞⌟∘⌜⌝-id a) (⌞⌟∘⌜⌝-id b)
  ⌞⌟∘⌜⌝-id (Λ k a) = cong₂ Λ (⌞⌟Kd∘⌜⌝Kd-id k) (⌞⌟∘⌜⌝-id a)
  ⌞⌟∘⌜⌝-id (ƛ a b) = cong₂ ƛ (⌞⌟∘⌜⌝-id a) (⌞⌟∘⌜⌝-id b)
  ⌞⌟∘⌜⌝-id (a ⊡ b) = cong₂ _⊡_ (⌞⌟∘⌜⌝-id a) (⌞⌟∘⌜⌝-id b)
  ⌞⌟∘⌜⌝-id (a · b) = begin
    ⌞ ⌜ a ⌝ ⌜·⌝ ⌜ b ⌝ ⌟     ≡⟨ ⌞⌟-· ⌜ a ⌝ ⌜ b ⌝ ⟩
    ⌞ ⌜ a ⌝ ⌟ · ⌞ ⌜ b ⌝ ⌟   ≡⟨ cong₂ _·_ (⌞⌟∘⌜⌝-id a) (⌞⌟∘⌜⌝-id b) ⟩
    a · b                   ∎

  ⌞⌟Kd∘⌜⌝Kd-id : ∀ {n} (k : Kind Term n) → ⌞ ⌜ k ⌝Kd ⌟Kd ≡ k
  ⌞⌟Kd∘⌜⌝Kd-id (a ⋯ b) = cong₂ _⋯_ (⌞⌟∘⌜⌝-id a) (⌞⌟∘⌜⌝-id b)
  ⌞⌟Kd∘⌜⌝Kd-id (Π j k) = cong₂ Π (⌞⌟Kd∘⌜⌝Kd-id j) (⌞⌟Kd∘⌜⌝Kd-id k)

mutual

  ⌜⌝∘⌞⌟-id : ∀ {n} (a : Elim n) → ⌜ ⌞ a ⌟ ⌝ ≡ a
  ⌜⌝∘⌞⌟-id (a ∙ bs) = begin
      ⌜ ⌞ a ⌟Hd ⌞∙⌟ ⌞ bs ⌟Sp ⌝
    ≡⟨ ⌜⌝-∙ ⌞ a ⌟Hd ⌞ bs ⌟Sp ⟩
      ⌜ ⌞ a ⌟Hd ⌝ ∙∙ map ⌜_⌝ ⌞ bs ⌟Sp
    ≡⟨ cong₂ _∙∙_ (⌜⌝∘⌞⌟Hd-∙-[] a) (map-⌜⌝∘⌞⌟Sp-id bs) ⟩
      a ∙ [] ∙∙ bs
    ∎

  map-⌜⌝∘⌞⌟Sp-id : ∀ {n} (as : Spine n) → map ⌜_⌝ ⌞ as ⌟Sp ≡ as
  map-⌜⌝∘⌞⌟Sp-id []       = refl
  map-⌜⌝∘⌞⌟Sp-id (a ∷ as) = cong₂ _∷_ (⌜⌝∘⌞⌟-id a) (map-⌜⌝∘⌞⌟Sp-id as)

  ⌜⌝∘⌞⌟Hd-∙-[] : ∀ {n} (a : Head n) → ⌜ ⌞ a ⌟Hd ⌝ ≡ a ∙ []
  ⌜⌝∘⌞⌟Hd-∙-[] (var x) = refl
  ⌜⌝∘⌞⌟Hd-∙-[] ⊥       = refl
  ⌜⌝∘⌞⌟Hd-∙-[] ⊤       = refl
  ⌜⌝∘⌞⌟Hd-∙-[] (Π k a) = cong₂ ∀∙ (⌜⌝Kd∘⌞⌟Kd-id k) (⌜⌝∘⌞⌟-id a)
  ⌜⌝∘⌞⌟Hd-∙-[] (a ⇒ b) = cong₂ _⇒∙_ (⌜⌝∘⌞⌟-id a) (⌜⌝∘⌞⌟-id b)
  ⌜⌝∘⌞⌟Hd-∙-[] (Λ k a) = cong₂ Λ∙ (⌜⌝Kd∘⌞⌟Kd-id k) (⌜⌝∘⌞⌟-id a)
  ⌜⌝∘⌞⌟Hd-∙-[] (ƛ a b) = cong₂ ƛ∙ (⌜⌝∘⌞⌟-id a) (⌜⌝∘⌞⌟-id b)
  ⌜⌝∘⌞⌟Hd-∙-[] (a ⊡ b) = cong₂ _⊡∙_ (⌜⌝∘⌞⌟-id a) (⌜⌝∘⌞⌟-id b)

  ⌜⌝Kd∘⌞⌟Kd-id : ∀ {n} (k : Kind Elim n) → ⌜ ⌞ k ⌟Kd ⌝Kd ≡ k
  ⌜⌝Kd∘⌞⌟Kd-id (a ⋯ b) = cong₂ _⋯_ (⌜⌝∘⌞⌟-id a) (⌜⌝∘⌞⌟-id b)
  ⌜⌝Kd∘⌞⌟Kd-id (Π j k) = cong₂ Π   (⌜⌝Kd∘⌞⌟Kd-id j) (⌜⌝Kd∘⌞⌟Kd-id k)

-- Simplified kinds are stable under conversions of term
-- representation.

⌊⌋-⌜⌝Kd : ∀ {n} (k : Kind Term n) → ⌊ ⌜ k ⌝Kd ⌋ ≡ ⌊ k ⌋
⌊⌋-⌜⌝Kd (a ⋯ b) = refl
⌊⌋-⌜⌝Kd (Π j k) = cong₂ _⇒_ (⌊⌋-⌜⌝Kd j) (⌊⌋-⌜⌝Kd k)

⌊⌋-⌞⌟Kd : ∀ {n} (k : Kind Elim n) → ⌊ ⌞ k ⌟Kd ⌋ ≡ ⌊ k ⌋
⌊⌋-⌞⌟Kd (a ⋯ b) = refl
⌊⌋-⌞⌟Kd (Π j k) = cong₂ _⇒_ (⌊⌋-⌞⌟Kd j) (⌊⌋-⌞⌟Kd k)

----------------------------------------------------------------------
-- Substitutions in raw terms
--
-- We use an intrinsically well-scoped variant of simultaneous
-- substitutions inspired by McBride's technique for defining
-- type-preserving substitutions [3].  These come with some support in
-- the Agda standard library.  In particular, the standard library
-- provides generic proofs for a plethora of standard untyped
-- substitution lemmas (e.g. substitutions commute, identity
-- substitutions vanish, etc.) which are easy but tedious to prove
-- (see the Data.Fin.Substitution.Lemmas module).  By using this
-- substitution framework, we get those lemmas for "free" (we still
-- need to provide some basic lemmas to bootstrap everything).
--
-- To use the standard framework, we must follow the following four
-- steps.
--
--  1. We define an application function `t / σ' of generic untyped
--     substitutions `σ' to well-scoped untyped terms `t'.  Generic
--     substitutions are defined over an abstract type `T', which will
--     later represent variables (to encode renamings) or terms (to
--     encode actual substitutions).  Hence the definition of
--     application must be parametrized over some abstract operations
--     on such substitutions (lifting, weakening, etc.) to be defined
--     later.  Concrete instances of these operations are collected in
--     the record `Lift' (see e.g. `SubstApp' module below).
--
--     Along with application, we define a few lemmas to be used in
--     step 4.  (They express the fact that application of
--     (multi-)substitutions is compositional w.r.t. the various
--     syntactic forms.)
--
--  2. Application is instantiated with `T = Fin' to obtain
--     well-scoped renamings, i.e. substitutions of variables in
--     terms.  The standard library provides a predefined instance of
--     `Lift Fin Term' to this end.
--
--  3. Using well-scoped renamings, an instance of `Lift Term Term' is
--     defined, and application is instantiated to concrete
--     substitutions of terms in terms.
--
--  4. Using the generic lemmas defined in step 1, many helpful
--     derived substitution lemmas are instantiated.
--     (E.g. "substitutions commute", "identity substitutions vanish",
--     etc.)
--
-- Most of the work is done in step 1, while steps 2-3 consists mostly
-- in calls to the substitution API of the Agda standard library.
--
--  [3] C. McBride, "Type-Preserving Renaming and Substitution"
--      http://strictlypositive.org/ren-sub.pdf

-- Application of generic substitutions lifted to type and kind
-- ascriptions.

module KdOrTpSubstApp {T T′ : ℕ → Set} (simple : Simple T)
                      (kdApp : Application (Kind T′) T)
                      (tpApp : Application T′ T) where
  open Simple simple
  open Application kdApp renaming (_/_ to _Kd/_; _/✶_ to _Kd/✶_)
  open Application tpApp renaming (_/_ to _Tp/_; _/✶_ to _Tp/✶_)

  infixl 8 _/_

  -- Apply a substitution to a kind or type ascription.

  _/_ : ∀ {m n} → KdOrTp T′ m → Sub T m n → KdOrTp T′ n
  (kd k) / σ = kd (k Kd/ σ)
  (tp a) / σ = tp (a Tp/ σ)

  open Application (record { _/_ = _/_     }) public hiding (_/_)

  -- Some helper lemmas about applying sequences of substitutions (to
  -- be used for instantiating TermSubstLemmas).

  -- Substitutions in kind ascriptions are compositional.

  kd-/✶-↑✶ : ∀ k {m n j} (σs : Subs T m n) →
             (kd j) /✶ σs ↑✶ k ≡ kd (j Kd/✶ σs ↑✶ k)
  kd-/✶-↑✶ k ε        = refl
  kd-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (kd-/✶-↑✶ k σs) refl

  -- Substitutions in type ascriptions are compositional.

  tp-/✶-↑✶ : ∀ k {m n a} (σs : Subs T m n) →
             (tp a) /✶ σs ↑✶ k ≡ tp (a Tp/✶ σs ↑✶ k)
  tp-/✶-↑✶ k ε        = refl
  tp-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (tp-/✶-↑✶ k σs) refl

-- Application of generic substitutions to terms

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

  infixl 8 _/_ _Kind/_ _Elim/_ _Head/_ _//_ _Kind′/_

  mutual

    -- Apply a substitution to a raw term/type.

    _/_ : ∀ {m n} → Term m → Sub T m n → Term n
    var x   / σ = lift (Vec.lookup σ x)
    ⊥       / σ = ⊥
    ⊤       / σ = ⊤
    Π k a   / σ = Π (k Kind/ σ) (a / σ ↑)
    (a ⇒ b) / σ = (a / σ) ⇒ (b / σ)
    Λ k a   / σ = Λ (k Kind/ σ) (a / σ ↑)
    ƛ a b   / σ = ƛ (a / σ) (b / σ ↑)
    a · b   / σ = (a / σ) · (b / σ)
    a ⊡ b   / σ = (a / σ) ⊡ (b / σ)

    -- Apply a substitution to a kind.

    _Kind/_ : ∀ {m n} → Kind Term m → Sub T m n → Kind Term n
    (a ⋯ b) Kind/ σ = (a / σ) ⋯ (b / σ)
    Π j k   Kind/ σ = Π (j Kind/ σ) (k Kind/ σ ↑)

  mutual

    -- Apply a substitution to an elimination.

    _Elim/_ : ∀ {m n} → Elim m → Sub T m n → Elim n
    a ∙ as Elim/ σ = (a Head/ σ) ∙∙ (as // σ)

    -- Apply a substitution to a head.

    _Head/_ : ∀ {m n} → Head m → Sub T m n → Elim n
    var x   Head/ σ = ⌜ lift (Vec.lookup σ x) ⌝
    ⊥       Head/ σ = ⊥∙
    ⊤       Head/ σ = ⊤∙
    Π k a   Head/ σ = ∀∙ (k Kind′/ σ) (a Elim/ σ ↑)
    (a ⇒ b) Head/ σ = (a Elim/ σ) ⇒∙ (b Elim/ σ)
    Λ k a   Head/ σ = Λ∙ (k Kind′/ σ) (a Elim/ σ ↑)
    ƛ a b   Head/ σ = ƛ∙ (a Elim/ σ) (b Elim/ σ ↑)
    a ⊡ b   Head/ σ = (a Elim/ σ) ⊡∙ (b Elim/ σ)

    -- Apply a substitution to a spine.

    _//_ : ∀ {m n} → Spine m → Sub T m n → Spine n
    []       // σ = []
    (a ∷ as) // σ = a Elim/ σ ∷ as // σ

    -- Apply a substitution to a (elimination-based) kind.
    _Kind′/_ : ∀ {m n} → Kind Elim m → Sub T m n → Kind Elim n
    (a ⋯ b) Kind′/ σ = (a Elim/ σ) ⋯ (b Elim/ σ)
    Π j k   Kind′/ σ = Π (j Kind′/ σ) (k Kind′/ σ ↑)

  private
    appTerm  = record { _/_ = _/_      }
    appKind  = record { _/_ = _Kind/_  }
    appElim  = record { _/_ = _Elim/_  }
    appKind′ = record { _/_ = _Kind′/_ }

  -- Some helper lemmas about applying sequences of substitutions (to
  -- be used for instantiating TermSubstLemmas).

  open Application appTerm hiding (_/_)
  open Application appKind using () renaming (_/✶_ to _Kind/✶_)

  -- The bottom and top types are invariant under substitution.

  ⊥-/✶-↑✶ : ∀ k {m n} (σs : Subs T m n) → ⊥ /✶ σs ↑✶ k ≡ ⊥
  ⊥-/✶-↑✶ k ε        = refl
  ⊥-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (⊥-/✶-↑✶ k σs) refl

  ⊤-/✶-↑✶ : ∀ k {m n} (σs : Subs T m n) → ⊤ /✶ σs ↑✶ k ≡ ⊤
  ⊤-/✶-↑✶ k ε        = refl
  ⊤-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (⊤-/✶-↑✶ k σs) refl

  -- Substitutions in the remaining term and type formers are
  -- compositional.

  Π-/✶-↑✶ : ∀ k {m n j a} (σs : Subs T m n) →
            (Π j a) /✶ σs ↑✶ k ≡ Π (j Kind/✶ σs ↑✶ k) (a /✶ σs ↑✶ suc k)
  Π-/✶-↑✶ k ε        = refl
  Π-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (Π-/✶-↑✶ k σs) refl

  ⇒-/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
            (a ⇒ b) /✶ σs ↑✶ k ≡ (a /✶ σs ↑✶ k) ⇒ (b /✶ σs ↑✶ k)
  ⇒-/✶-↑✶ k ε        = refl
  ⇒-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (⇒-/✶-↑✶ k σs) refl

  Λ-/✶-↑✶ : ∀ k {m n j a} (σs : Subs T m n) →
            (Λ j a) /✶ σs ↑✶ k ≡ Λ (j Kind/✶ σs ↑✶ k) (a /✶ σs ↑✶ suc k)
  Λ-/✶-↑✶ k ε        = refl
  Λ-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (Λ-/✶-↑✶ k σs) refl

  ƛ-/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
            (ƛ a b) /✶ σs ↑✶ k ≡ ƛ (a /✶ σs ↑✶ k) (b /✶ σs ↑✶ suc k)
  ƛ-/✶-↑✶ k ε        = refl
  ƛ-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (ƛ-/✶-↑✶ k σs) refl

  ·-/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
            (a · b) /✶ σs ↑✶ k ≡ (a /✶ σs ↑✶ k) · (b /✶ σs ↑✶ k)
  ·-/✶-↑✶ k ε        = refl
  ·-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (·-/✶-↑✶ k σs) refl

  ⊡-/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
            (a ⊡ b) /✶ σs ↑✶ k ≡ (a /✶ σs ↑✶ k) ⊡ (b /✶ σs ↑✶ k)
  ⊡-/✶-↑✶ k ε        = refl
  ⊡-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (⊡-/✶-↑✶ k σs) refl

  -- Substitutions in the kind formers are compositional.

  Π-Kind/✶-↑✶ : ∀ k {m n j l} (σs : Subs T m n) →
            (Π j l) Kind/✶ σs ↑✶ k ≡
              Π (j Kind/✶ σs ↑✶ k) (l Kind/✶ σs ↑✶ (suc k))
  Π-Kind/✶-↑✶ k ε        = refl
  Π-Kind/✶-↑✶ k (σ ◅ σs) = cong₂ _Kind/_ (Π-Kind/✶-↑✶ k σs) refl

  ⋯-Kind/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
            (a ⋯ b) Kind/✶ σs ↑✶ k ≡ (a /✶ σs ↑✶ k) ⋯ (b /✶ σs ↑✶ k)
  ⋯-Kind/✶-↑✶ k ε        = refl
  ⋯-Kind/✶-↑✶ k (σ ◅ σs) = cong₂ _Kind/_ (⋯-Kind/✶-↑✶ k σs) refl

  -- Application of substitutions commutes with concatenation of spines.

  ++-// : ∀ {m n} (as bs : Spine m) {σ : Sub T m n} →
         (as ++ bs) // σ ≡ as // σ ++ bs // σ
  ++-// []       bs = refl
  ++-// (a ∷ as) bs = cong (a Elim/ _ ∷_) (++-// as bs)

  -- Application of substitutions commutes application of spines and
  -- eliminations.

  ∙∙-/ : ∀ {m n} a (as : Spine m) {σ : Sub T m n} →
         a ∙∙ as Elim/ σ ≡ (a Elim/ σ) ∙∙ (as // σ)
  ∙∙-/ (a ∙ as) bs = begin
      (a Head/ _) ∙∙ ((as ++ bs) // _)
    ≡⟨ cong (_ ∙∙_) (++-// as bs) ⟩
      (a Head/ _) ∙∙ (as // _ ++ bs // _)
    ≡⟨ sym (∙∙-++ _ (as // _) (bs // _)) ⟩
      (a Head/ _) ∙∙ (as // _) ∙∙ (bs // _)
    ∎

  ⌜·⌝-/ : ∀ {m n} (a b : Elim m) {σ : Sub T m n} →
          a ⌜·⌝ b Elim/ σ ≡ (a Elim/ σ) ⌜·⌝ (b Elim/ σ)
  ⌜·⌝-/ (a ∙ as) b {σ} = begin
      (a Head/ σ) ∙∙ ((as ∷ʳ b) // σ)
    ≡⟨ cong ((a Head/ σ) ∙∙_) (++-// as (b ∷ [])) ⟩
      (a Head/ σ) ∙∙ (as // σ ++ (b ∷ []) // σ)
    ≡⟨ sym (∙∙-++ (a Head/ σ) (as // σ) ((b ∷ []) // σ)) ⟩
      (a Head/ σ) ∙∙ (as // σ) ∙∙ ((b ∷ []) // σ)
    ≡⟨ ∙∙IsFold ((a Head/ σ) ∙∙ (as // σ)) ((b ∷ []) // σ) ⟩
      (a Head/ σ) ∙∙ (as // σ) ⌜·⌝ (b Elim/ σ)
    ∎

  -- Application of substitutions commutes with the conversions.

  mutual

    ⌜⌝-/ : ∀ {m n} a {σ : Sub T m n} → ⌜ a / σ ⌝ ≡ ⌜ a ⌝ Elim/ σ
    ⌜⌝-/ (var x) = sym (∙∙-[] _)
    ⌜⌝-/ ⊥       = refl
    ⌜⌝-/ ⊤       = refl
    ⌜⌝-/ (Π k a) = cong₂ ∀∙ (⌜⌝Kd-/ k) (⌜⌝-/ a)
    ⌜⌝-/ (a ⇒ b) = cong₂ _⇒∙_ (⌜⌝-/ a) (⌜⌝-/ b)
    ⌜⌝-/ (Λ k a) = cong₂ Λ∙ (⌜⌝Kd-/ k) (⌜⌝-/ a)
    ⌜⌝-/ (ƛ a b) = cong₂ ƛ∙ (⌜⌝-/ a) (⌜⌝-/ b)
    ⌜⌝-/ (a · b) {σ} = begin
      ⌜ a / σ ⌝ ⌜·⌝ ⌜ b / σ ⌝               ≡⟨ cong₂ _⌜·⌝_ (⌜⌝-/ a) (⌜⌝-/ b) ⟩
      (⌜ a ⌝ Elim/ σ) ⌜·⌝ (⌜ b ⌝ Elim/ σ)   ≡⟨ sym (⌜·⌝-/ ⌜ a ⌝ ⌜ b ⌝) ⟩
      ⌜ a ⌝ ⌜·⌝ ⌜ b ⌝ Elim/ σ               ∎
    ⌜⌝-/ (a ⊡ b) = cong₂ _⊡∙_ (⌜⌝-/ a) (⌜⌝-/ b)

    ⌜⌝Kd-/ : ∀ {m n} k {σ : Sub T m n} → ⌜ k Kind/ σ ⌝Kd ≡ ⌜ k ⌝Kd Kind′/ σ
    ⌜⌝Kd-/ (a ⋯ b) = cong₂ _⋯_ (⌜⌝-/ a) (⌜⌝-/ b)
    ⌜⌝Kd-/ (Π j k) = cong₂ Π (⌜⌝Kd-/ j) (⌜⌝Kd-/ k)

  ⌞⌟-/ : ∀ {m n} a {σ : Sub T m n} → ⌞ a Elim/ σ ⌟ ≡ ⌞ a ⌟ / σ
  ⌞⌟-/ a {σ} = begin
    ⌞ a         Elim/ σ ⌟   ≡⟨ cong (⌞_⌟ ∘ (_Elim/ σ)) (sym (⌜⌝∘⌞⌟-id a)) ⟩
    ⌞ ⌜ ⌞ a ⌟ ⌝ Elim/ σ ⌟   ≡⟨ cong ⌞_⌟ (sym (⌜⌝-/ ⌞ a ⌟)) ⟩
    ⌞ ⌜ ⌞ a ⌟ / σ     ⌝ ⌟   ≡⟨ ⌞⌟∘⌜⌝-id (⌞ a ⌟ / σ) ⟩
        ⌞ a ⌟ / σ       ∎

  ⌞⌟Kd-/ : ∀ {m n} k {σ : Sub T m n} → ⌞ k Kind′/ σ ⌟Kd ≡ ⌞ k ⌟Kd Kind/ σ
  ⌞⌟Kd-/ (a ⋯ b) = cong₂ _⋯_ (⌞⌟-/ a) (⌞⌟-/ b)
  ⌞⌟Kd-/ (Π j k) = cong₂ Π (⌞⌟Kd-/ j) (⌞⌟Kd-/ k)

  open Application appElim  using () renaming (_/✶_ to _Elim/✶_)
  open Application appKind′ using () renaming (_/✶_ to _Kind′/✶_)

  -- Application of multiple substitutions commutes with conversion to
  -- eliminations.

  ⌜⌝-/✶-↑✶ : ∀ k {m n a} (σs : Subs T m n) →
             ⌜ a /✶ σs ↑✶ k ⌝ ≡ ⌜ a ⌝ Elim/✶ σs ↑✶ k
  ⌜⌝-/✶-↑✶ k ε        = refl
  ⌜⌝-/✶-↑✶ k (σ ◅ σs) = begin
    ⌜ _ /✶ (σ ◅ σs) ↑✶ k ⌝          ≡⟨ ⌜⌝-/ (_ /✶ σs ↑✶ k) ⟩
    ⌜ _ /✶ σs ↑✶ k ⌝ Elim/ σ ↑⋆ k   ≡⟨ cong (_Elim/ _) (⌜⌝-/✶-↑✶ k σs) ⟩
    _ Elim/✶ (σ ◅ σs) ↑✶ k          ∎

  ⌜⌝Kd-/✶-↑✶ : ∀ k {m n j} (σs : Subs T m n) →
               ⌜ j Kind/✶ σs ↑✶ k ⌝Kd ≡ ⌜ j ⌝Kd Kind′/✶ σs ↑✶ k
  ⌜⌝Kd-/✶-↑✶ k ε        = refl
  ⌜⌝Kd-/✶-↑✶ k (σ ◅ σs) = begin
      ⌜ _ Kind/✶ (σ ◅ σs) ↑✶ k ⌝Kd
    ≡⟨ ⌜⌝Kd-/ (_ Kind/✶ σs ↑✶ k) ⟩
      ⌜ _ Kind/✶ σs ↑✶ k ⌝Kd Kind′/ σ ↑⋆ k
    ≡⟨ cong (_Kind′/ _) (⌜⌝Kd-/✶-↑✶ k σs) ⟩
      _ Kind′/✶ (σ ◅ σs) ↑✶ k
    ∎

  -- Simplified kinds are stable under application of substitutions.

  ⌊⌋-Kind/ : ∀ {m n} (k : Kind Term m) {σ : Sub T m n} → ⌊ k Kind/ σ ⌋ ≡ ⌊ k ⌋
  ⌊⌋-Kind/ (a ⋯ b) = refl
  ⌊⌋-Kind/ (Π j k) = cong₂ _⇒_ (⌊⌋-Kind/ j) (⌊⌋-Kind/ k)

  ⌊⌋-Kind′/ : ∀ {m n} (k : Kind Elim m) {σ : Sub T m n} →
              ⌊ k Kind′/ σ ⌋ ≡ ⌊ k ⌋
  ⌊⌋-Kind′/ (a ⋯ b) = refl
  ⌊⌋-Kind′/ (Π j k) = cong₂ _⇒_ (⌊⌋-Kind′/ j) (⌊⌋-Kind′/ k)

  -- Application of substitutions to type and kind ascriptions.

  open KdOrTpSubstApp simple appKind  appTerm public using ()
    renaming (_/_ to _TermAsc/_)
  open KdOrTpSubstApp simple appKind′ appElim public using ()
    renaming (_/_ to _ElimAsc/_)

-- Substitutions in terms and associated lemmas.

module Substitution where

  -- Term substitutions.

  termSubst : TermSubst Term
  termSubst = record { var = var; app = SubstApp._/_ }

  -- Variable substitutions (renamings) in heads.
  --
  -- NOTE. The special treatment of heads here reflects the fact that
  -- the structure of heads is preserved by renamings but not by
  -- general term substitutions.

  module HeadRenamings where
    open Simple VarSubst.simple hiding (var)
    open SubstApp (TermSubst.varLift termSubst)

    infixl 8 _Head/Var_

    _Head/Var_ : ∀ {m n} → Head m → Sub Fin m n → Head n
    var x   Head/Var σ = var (Vec.lookup σ x)
    ⊥       Head/Var σ = ⊥
    ⊤       Head/Var σ = ⊤
    Π k a   Head/Var σ = Π (k Kind′/ σ) (a Elim/ σ ↑)
    (a ⇒ b) Head/Var σ = (a Elim/ σ) ⇒ (b Elim/ σ)
    Λ k a   Head/Var σ = Λ (k Kind′/ σ) (a Elim/ σ ↑)
    ƛ a b   Head/Var σ = ƛ (a Elim/ σ) (b Elim/ σ ↑)
    (a ⊡ b) Head/Var σ = (a Elim/ σ) ⊡ (b Elim/ σ)

    -- A lemma relating the above definition of application to the
    -- previous ones.

    Head/Var-∙ : ∀ {m n} {σ : Sub Fin m n} a → (a Head/Var σ) ∙ [] ≡ a Head/ σ
    Head/Var-∙ (var x) = refl
    Head/Var-∙ ⊥       = refl
    Head/Var-∙ ⊤       = refl
    Head/Var-∙ (Π k a) = refl
    Head/Var-∙ (a ⇒ b) = refl
    Head/Var-∙ (Λ k a) = refl
    Head/Var-∙ (ƛ a b) = refl
    Head/Var-∙ (a ⊡ b) = refl

    headOf-Head/Var : ∀ {m n} {σ : Sub Fin m n} a →
                      a Head/Var σ ≡ headOf (a Head/ σ)
    headOf-Head/Var a = cong headOf (Head/Var-∙ a)

    Elim/Var-Head/Var : ∀ {m n} {σ : Sub Fin m n} a →
                        a ∙ [] Elim/ σ ≡ (a Head/Var σ) ∙ []
    Elim/Var-Head/Var {σ = σ} a = begin
      a ∙ [] Elim/ σ        ≡⟨ ∙∙-[] (a Head/ σ) ⟩
      a Head/ σ             ≡⟨ sym (Head/Var-∙ a) ⟩
      (a Head/Var σ) ∙ []   ∎

  open HeadRenamings public

  -- Lemmas relating application of sequences of generic substitutions
  -- lifted to any number of additional variables.
  --
  -- Using these generic lemmas, we can instantiate the record
  -- Data.Fin.Substitution.Lemmas.TermLemmas below, which gives access
  -- to a number of useful (derived) lemmas about path substitutions.

  module Lemmas {T₁ T₂ : ℕ → Set}
                {lift₁ : Lift T₁ Term} {lift₂ : Lift T₂ Term} where
    open SubstApp
    open Lift lift₁ using () renaming (_↑✶_ to _↑✶₁_)
    open Lift lift₂ using () renaming (_↑✶_ to _↑✶₂_)
    open Application (record { _/_ = SubstApp._/_ lift₁ }) using ()
      renaming (_/✶_ to _/✶₁_)
    open Application (record { _/_ = SubstApp._/_ lift₂ }) using ()
      renaming (_/✶_ to _/✶₂_)
    open Application (record { _/_ = SubstApp._Kind/_ lift₁ }) using ()
      renaming (_/✶_ to _Kind/✶₁_)
    open Application (record { _/_ = SubstApp._Kind/_ lift₂ }) using ()
      renaming (_/✶_ to _Kind/✶₂_)

    -- Sequences of (lifted) T₁ and T₂-substitutions are equivalent
    -- when applied to raw terms/types/kinds if they are equivalent
    -- when applied to variables.

    mutual

      /✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                (∀ k x → var x /✶₁ σs₁ ↑✶₁ k ≡ var x /✶₂ σs₂ ↑✶₂ k) →
                 ∀ k a → a     /✶₁ σs₁ ↑✶₁ k ≡ a     /✶₂ σs₂ ↑✶₂ k
      /✶-↑✶ σs₁ σs₂ hyp k (var x) = hyp k x
      /✶-↑✶ σs₁ σs₂ hyp k ⊥ = begin
        ⊥ /✶₁ σs₁ ↑✶₁ k   ≡⟨ ⊥-/✶-↑✶ _ k σs₁ ⟩
        ⊥                 ≡⟨ sym (⊥-/✶-↑✶ _ k σs₂) ⟩
        ⊥ /✶₂ σs₂ ↑✶₂ k   ∎
      /✶-↑✶ σs₁ σs₂ hyp k ⊤ = begin
        ⊤ /✶₁ σs₁ ↑✶₁ k   ≡⟨ ⊤-/✶-↑✶ _ k σs₁ ⟩
        ⊤                 ≡⟨ sym (⊤-/✶-↑✶ _ k σs₂) ⟩
        ⊤ /✶₂ σs₂ ↑✶₂ k   ∎
      /✶-↑✶ σs₁ σs₂ hyp k (Π j a) = begin
          (Π j a) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ Π-/✶-↑✶ _ k σs₁ ⟩
          Π (j Kind/✶₁ σs₁ ↑✶₁ k) (a /✶₁ σs₁ ↑✶₁ suc k)
        ≡⟨ cong₂ Π (Kind/✶-↑✶ σs₁ σs₂ hyp k j) (/✶-↑✶ σs₁ σs₂ hyp (suc k) a) ⟩
          Π (j Kind/✶₂ σs₂ ↑✶₂ k) (a /✶₂ σs₂ ↑✶₂ suc k)
        ≡⟨ sym (Π-/✶-↑✶ _ k σs₂) ⟩
          (Π j a) /✶₂ σs₂ ↑✶₂ k
        ∎
      /✶-↑✶ σs₁ σs₂ hyp k (a ⇒ b) = begin
          (a ⇒ b) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ ⇒-/✶-↑✶ _ k σs₁ ⟩
          (a /✶₁ σs₁ ↑✶₁ k) ⇒ (b /✶₁ σs₁ ↑✶₁ k)
        ≡⟨ cong₂ _⇒_ (/✶-↑✶ σs₁ σs₂ hyp k a) (/✶-↑✶ σs₁ σs₂ hyp k b) ⟩
          (a /✶₂ σs₂ ↑✶₂ k) ⇒ (b /✶₂ σs₂ ↑✶₂ k)
        ≡⟨ sym (⇒-/✶-↑✶ _ k σs₂) ⟩
          (a ⇒ b) /✶₂ σs₂ ↑✶₂ k
        ∎
      /✶-↑✶ σs₁ σs₂ hyp k (Λ j a) = begin
          (Λ j a) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ Λ-/✶-↑✶ _ k σs₁ ⟩
          Λ (j Kind/✶₁ σs₁ ↑✶₁ k) (a /✶₁ σs₁ ↑✶₁ suc k)
        ≡⟨ cong₂ Λ (Kind/✶-↑✶ σs₁ σs₂ hyp k j) (/✶-↑✶ σs₁ σs₂ hyp (suc k) a) ⟩
          Λ (j Kind/✶₂ σs₂ ↑✶₂ k) (a /✶₂ σs₂ ↑✶₂ suc k)
        ≡⟨ sym (Λ-/✶-↑✶ _ k σs₂) ⟩
          (Λ j a) /✶₂ σs₂ ↑✶₂ k
        ∎
      /✶-↑✶ σs₁ σs₂ hyp k (ƛ a b) = begin
          (ƛ a b) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ ƛ-/✶-↑✶ _ k σs₁ ⟩
          ƛ (a /✶₁ σs₁ ↑✶₁ k) (b /✶₁ σs₁ ↑✶₁ suc k)
        ≡⟨ cong₂ ƛ (/✶-↑✶ σs₁ σs₂ hyp k a) (/✶-↑✶ σs₁ σs₂ hyp (suc k) b) ⟩
          ƛ (a /✶₂ σs₂ ↑✶₂ k) (b /✶₂ σs₂ ↑✶₂ suc k)
        ≡⟨ sym (ƛ-/✶-↑✶ _ k σs₂) ⟩
          (ƛ a b) /✶₂ σs₂ ↑✶₂ k
        ∎
      /✶-↑✶ σs₁ σs₂ hyp k (a · b) = begin
          (a · b) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ ·-/✶-↑✶ _ k σs₁ ⟩
          (a /✶₁ σs₁ ↑✶₁ k) · (b /✶₁ σs₁ ↑✶₁ k)
        ≡⟨ cong₂ _·_ (/✶-↑✶ σs₁ σs₂ hyp k a) (/✶-↑✶ σs₁ σs₂ hyp k b) ⟩
          (a /✶₂ σs₂ ↑✶₂ k) · (b /✶₂ σs₂ ↑✶₂ k)
        ≡⟨ sym (·-/✶-↑✶ _ k σs₂) ⟩
          (a · b) /✶₂ σs₂ ↑✶₂ k
        ∎
      /✶-↑✶ σs₁ σs₂ hyp k (a ⊡ b) = begin
          (a ⊡ b) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ ⊡-/✶-↑✶ _ k σs₁ ⟩
          (a /✶₁ σs₁ ↑✶₁ k) ⊡ (b /✶₁ σs₁ ↑✶₁ k)
        ≡⟨ cong₂ _⊡_ (/✶-↑✶ σs₁ σs₂ hyp k a) (/✶-↑✶ σs₁ σs₂ hyp k b) ⟩
          (a /✶₂ σs₂ ↑✶₂ k) ⊡ (b /✶₂ σs₂ ↑✶₂ k)
        ≡⟨ sym (⊡-/✶-↑✶ _ k σs₂) ⟩
          (a ⊡ b) /✶₂ σs₂ ↑✶₂ k
        ∎

      Kind/✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                  (∀ k x → var x /✶₁ σs₁ ↑✶₁ k ≡ var x /✶₂ σs₂ ↑✶₂ k) →
                   ∀ k j → j Kind/✶₁ σs₁ ↑✶₁ k ≡ j Kind/✶₂ σs₂ ↑✶₂ k
      Kind/✶-↑✶ σs₁ σs₂ hyp k (a ⋯ b) = begin
          (a ⋯ b) Kind/✶₁ σs₁ ↑✶₁ k
        ≡⟨ ⋯-Kind/✶-↑✶ _ k σs₁ ⟩
          (a /✶₁ σs₁ ↑✶₁ k) ⋯ (b /✶₁ σs₁ ↑✶₁ k)
        ≡⟨ cong₂ _⋯_ (/✶-↑✶ σs₁ σs₂ hyp k a) (/✶-↑✶ σs₁ σs₂ hyp k b) ⟩
          (a /✶₂ σs₂ ↑✶₂ k) ⋯ (b /✶₂ σs₂ ↑✶₂ k)
        ≡⟨ sym (⋯-Kind/✶-↑✶ _ k σs₂) ⟩
          (a ⋯ b) Kind/✶₂ σs₂ ↑✶₂ k
        ∎
      Kind/✶-↑✶ σs₁ σs₂ hyp k (Π j l) = begin
          (Π j l) Kind/✶₁ σs₁ ↑✶₁ k
        ≡⟨ Π-Kind/✶-↑✶ _ k σs₁ ⟩
          Π (j Kind/✶₁ σs₁ ↑✶₁ k) (l Kind/✶₁ σs₁ ↑✶₁ suc k)
        ≡⟨ cong₂ Π (Kind/✶-↑✶ σs₁ σs₂ hyp k j)
                   (Kind/✶-↑✶ σs₁ σs₂ hyp (suc k) l) ⟩
          Π (j Kind/✶₂ σs₂ ↑✶₂ k) (l Kind/✶₂ σs₂ ↑✶₂ suc k)
        ≡⟨ sym (Π-Kind/✶-↑✶ _ k σs₂) ⟩
          (Π j l) Kind/✶₂ σs₂ ↑✶₂ k
        ∎

    open Application (record { _/_ = SubstApp._Elim/_ lift₁ }) using ()
      renaming (_/✶_ to _Elim/✶₁_)
    open Application (record { _/_ = SubstApp._Elim/_ lift₂ }) using ()
      renaming (_/✶_ to _Elim/✶₂_)

    Elim/✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                  (∀ k x → var x /✶₁ σs₁ ↑✶₁ k ≡ var x /✶₂ σs₂ ↑✶₂ k) →
                   ∀ k a → a Elim/✶₁ σs₁ ↑✶₁ k ≡ a Elim/✶₂ σs₂ ↑✶₂ k
    Elim/✶-↑✶ σs₁ σs₂ hyp k a = begin
        a Elim/✶₁ σs₁ ↑✶₁ k
      ≡⟨ sym (cong (_Elim/✶₁ σs₁ ↑✶₁ k) (⌜⌝∘⌞⌟-id a)) ⟩
        ⌜ ⌞ a ⌟ ⌝ Elim/✶₁ σs₁ ↑✶₁ k
      ≡⟨ sym (⌜⌝-/✶-↑✶ _ k σs₁) ⟩
        ⌜ ⌞ a ⌟ /✶₁ σs₁ ↑✶₁ k ⌝
      ≡⟨ cong ⌜_⌝ (/✶-↑✶ σs₁ σs₂ hyp k ⌞ a ⌟) ⟩
        ⌜ ⌞ a ⌟ /✶₂ σs₂ ↑✶₂ k ⌝
      ≡⟨ ⌜⌝-/✶-↑✶ _ k σs₂ ⟩
        ⌜ ⌞ a ⌟ ⌝ Elim/✶₂ σs₂ ↑✶₂ k
      ≡⟨ cong (_Elim/✶₂ σs₂ ↑✶₂ k) (⌜⌝∘⌞⌟-id a) ⟩
        a Elim/✶₂ σs₂ ↑✶₂ k
      ∎

    open Application (record { _/_ = SubstApp._Kind′/_ lift₁ }) using ()
      renaming (_/✶_ to _Kind′/✶₁_)
    open Application (record { _/_ = SubstApp._Kind′/_ lift₂ }) using ()
      renaming (_/✶_ to _Kind′/✶₂_)

    Kind′/✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                  (∀ k x → var x  /✶₁ σs₁ ↑✶₁ k ≡ var x  /✶₂ σs₂ ↑✶₂ k) →
                   ∀ k j → j Kind′/✶₁ σs₁ ↑✶₁ k ≡ j Kind′/✶₂ σs₂ ↑✶₂ k
    Kind′/✶-↑✶ σs₁ σs₂ hyp k j = begin
        j Kind′/✶₁ σs₁ ↑✶₁ k
      ≡⟨ sym (cong (_Kind′/✶₁ σs₁ ↑✶₁ k) (⌜⌝Kd∘⌞⌟Kd-id j)) ⟩
        ⌜ ⌞ j ⌟Kd ⌝Kd Kind′/✶₁ σs₁ ↑✶₁ k
      ≡⟨ sym (⌜⌝Kd-/✶-↑✶ _ k σs₁) ⟩
        ⌜ ⌞ j ⌟Kd Kind/✶₁ σs₁ ↑✶₁ k ⌝Kd
      ≡⟨ cong ⌜_⌝Kd (Kind/✶-↑✶ σs₁ σs₂ hyp k ⌞ j ⌟Kd) ⟩
        ⌜ ⌞ j ⌟Kd Kind/✶₂ σs₂ ↑✶₂ k ⌝Kd
      ≡⟨ ⌜⌝Kd-/✶-↑✶ _ k σs₂ ⟩
        ⌜ ⌞ j ⌟Kd ⌝Kd Kind′/✶₂ σs₂ ↑✶₂ k
      ≡⟨ cong (_Kind′/✶₂ σs₂ ↑✶₂ k) (⌜⌝Kd∘⌞⌟Kd-id j) ⟩
        j Kind′/✶₂ σs₂ ↑✶₂ k
      ∎

  -- Lemmas relating application of sequences of generic substitutions
  -- in generic kind or type ascriptions, provided substitutions on
  -- the underlying kinds or types are similarly related.

  record KdOrTpLemmas {T₁ T₂ T′ : ℕ → Set}
                      (lift₁ : Lift T₁ Term)
                      (lift₂ : Lift T₂ Term)
                      : Set where
    field
      kdApp₁ : Application (Kind T′) T₁
      kdApp₂ : Application (Kind T′) T₂
      tpApp₁ : Application T′ T₁
      tpApp₂ : Application T′ T₂

    open Lift lift₁ using () renaming (_↑✶_ to _↑✶₁_)
    open Lift lift₂ using () renaming (_↑✶_ to _↑✶₂_)
    private
      module A₁  = Application (record { _/_ = SubstApp._/_ lift₁ })
      module A₂  = Application (record { _/_ = SubstApp._/_ lift₂ })
      module T₁  = Application tpApp₁
      module T₂  = Application tpApp₂
      module K₁  = Application kdApp₁
      module K₂  = Application kdApp₂
      module KT₁ = KdOrTpSubstApp (Lift.simple lift₁) kdApp₁ tpApp₁
      module KT₂ = KdOrTpSubstApp (Lift.simple lift₂) kdApp₂ tpApp₂

    -- Sequences of (lifted) T₁ and T₂-substitutions are equivalent
    -- when applied to kinds and raw types (represented as T′s) if
    -- they are equivalent when applied to variables (represented as
    -- raw terms).

    field
      Kd/✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                (∀ k x → var x A₁./✶ σs₁ ↑✶₁ k ≡ var x A₂./✶ σs₂ ↑✶₂ k) →
                 ∀ k a → a     K₁./✶ σs₁ ↑✶₁ k ≡ a      K₂./✶ σs₂ ↑✶₂ k

      Tp/✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                (∀ k x → var x A₁./✶ σs₁ ↑✶₁ k ≡ var x A₂./✶ σs₂ ↑✶₂ k) →
                 ∀ k a → a     T₁./✶ σs₁ ↑✶₁ k ≡ a     T₂./✶ σs₂ ↑✶₂ k

    /✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
            (∀ k x → var x A₁./✶  σs₁ ↑✶₁ k ≡ var x A₂./✶  σs₂ ↑✶₂ k) →
             ∀ k a → a     KT₁./✶ σs₁ ↑✶₁ k ≡ a     KT₂./✶ σs₂ ↑✶₂ k
    /✶-↑✶ σs₁ σs₂ hyp k (kd j) = begin
      kd j KT₁./✶ σs₁ ↑✶₁ k    ≡⟨ KT₁.kd-/✶-↑✶ k σs₁ ⟩
      kd (j K₁./✶ σs₁ ↑✶₁ k)   ≡⟨ cong kd (Kd/✶-↑✶ σs₁ σs₂ hyp k j) ⟩
      kd (j K₂./✶ σs₂ ↑✶₂ k)   ≡⟨ sym (KT₂.kd-/✶-↑✶ k σs₂) ⟩
      kd j KT₂./✶ σs₂ ↑✶₂ k    ∎
    /✶-↑✶ σs₁ σs₂ hyp k (tp a) = begin
      tp a KT₁./✶ σs₁ ↑✶₁ k      ≡⟨ KT₁.tp-/✶-↑✶ k σs₁ ⟩
      tp (a T₁./✶ σs₁ ↑✶₁ k)   ≡⟨ cong tp (Tp/✶-↑✶ σs₁ σs₂ hyp k a) ⟩
      tp (a T₂./✶ σs₂ ↑✶₂ k)   ≡⟨ sym (KT₂.tp-/✶-↑✶ k σs₂) ⟩
      tp a KT₂./✶ σs₂ ↑✶₂ k      ∎

  termAscLemmas : ∀ {T₁ T₂} lift₁ lift₂ → KdOrTpLemmas {T₁} {T₂} lift₁ lift₂
  termAscLemmas lift₁ lift₂ = record
    { kdApp₁  = record { _/_ = SubstApp._Kind/_ lift₁ }
    ; kdApp₂  = record { _/_ = SubstApp._Kind/_ lift₂ }
    ; tpApp₁  = record { _/_ = SubstApp._/_ lift₁ }
    ; tpApp₂  = record { _/_ = SubstApp._/_ lift₂ }
    ; Kd/✶-↑✶ = Lemmas.Kind/✶-↑✶
    ; Tp/✶-↑✶ = Lemmas./✶-↑✶
    }

  elimAscLemmas : ∀ {T₁ T₂} lift₁ lift₂ → KdOrTpLemmas {T₁} {T₂} lift₁ lift₂
  elimAscLemmas lift₁ lift₂ = record
    { kdApp₁  = record { _/_ = SubstApp._Kind′/_ lift₁ }
    ; kdApp₂  = record { _/_ = SubstApp._Kind′/_ lift₂ }
    ; tpApp₁  = record { _/_ = SubstApp._Elim/_ lift₁ }
    ; tpApp₂  = record { _/_ = SubstApp._Elim/_ lift₂ }
    ; Kd/✶-↑✶ = Lemmas.Kind′/✶-↑✶
    ; Tp/✶-↑✶ = Lemmas.Elim/✶-↑✶
    }

  -- By instantiating TermLemmas, we get access to a number of useful
  -- (derived) lemmas about path substitutions.

  termLemmas : TermLemmas Term
  termLemmas = record
    { termSubst = termSubst
    ; app-var   = refl
    ; /✶-↑✶     = Lemmas./✶-↑✶
    }

  open TermLemmas termLemmas public hiding (var; termSubst; weaken-sub)
  open SubstApp (TermSubst.termLift termSubst) public using
    ( _Head/_; _//_
    ; ++-//; ∙∙-/; ⌜·⌝-/; ⌜⌝-/; ⌜⌝Kd-/; ⌞⌟-/; ⌞⌟Kd-/; ⌊⌋-Kind/; ⌊⌋-Kind′/
    )
  open SubstApp (TermSubst.varLift termSubst) public using () renaming
    ( _Head/_   to _Head/Var′_
    ; _//_      to _//Var_
    ; ++-//     to ++-//Var
    ; ∙∙-/      to ∙∙-/Var
    ; ⌜·⌝-/     to ⌜·⌝-/Var
    ; ⌜⌝-/      to ⌜⌝-/Var
    ; ⌜⌝Kd-/    to ⌜⌝Kd-/Var
    ; ⌞⌟-/      to ⌞⌟-/Var
    ; ⌞⌟Kd-/    to ⌞⌟Kd-/Var
    ; ⌊⌋-Kind/  to ⌊⌋-Kind/Var
    ; ⌊⌋-Kind′/ to ⌊⌋-Kind′/Var
    )

  -- By instantiating TermLikeLemmas, we get access to a number of
  -- useful (derived) lemmas about variable substitutions (renamings)
  -- and substitutions in kinds, eliminations and ascriptions.

  private
    termLikeLemmas : TermLikeLemmas Term Term
    termLikeLemmas = record
      { app        = SubstApp._/_
      ; termLemmas = termLemmas
      ; /✶-↑✶₁     = Lemmas./✶-↑✶
      ; /✶-↑✶₂     = Lemmas./✶-↑✶
      }

  open TermLikeLemmas termLikeLemmas public using
    ( varLiftAppLemmas; varLiftSubLemmas; _/Var_
    ; weaken-sub; weaken-/; weaken⋆; /-wk⋆
    )

  termLikeLemmasKind : TermLikeLemmas (Kind Term) Term
  termLikeLemmasKind = record
    { app        = SubstApp._Kind/_
    ; termLemmas = termLemmas
    ; /✶-↑✶₁     = Lemmas.Kind/✶-↑✶
    ; /✶-↑✶₂     = Lemmas.Kind/✶-↑✶
    }

  open TermLikeLemmas termLikeLemmasKind public using () renaming
    ( _/_     to _Kind/_
    ; _/Var_  to _Kind/Var_
    ; weaken  to weakenKind
    ; weaken⋆ to weakenKind⋆
    )

  termLikeLemmasElim : TermLikeLemmas Elim Term
  termLikeLemmasElim = record
    { app        = SubstApp._Elim/_
    ; termLemmas = termLemmas
    ; /✶-↑✶₁     = Lemmas.Elim/✶-↑✶
    ; /✶-↑✶₂     = Lemmas.Elim/✶-↑✶
    }

  open TermLikeLemmas termLikeLemmasElim public using () renaming
    ( _/_     to _Elim/_
    ; _/Var_  to _Elim/Var_
    ; weaken  to weakenElim
    ; weaken⋆ to weakenElim⋆
    )

  termLikeLemmasKind′ : TermLikeLemmas (Kind Elim) Term
  termLikeLemmasKind′ = record
    { app        = SubstApp._Kind′/_
    ; termLemmas = termLemmas
    ; /✶-↑✶₁     = Lemmas.Kind′/✶-↑✶
    ; /✶-↑✶₂     = Lemmas.Kind′/✶-↑✶
    }

  open TermLikeLemmas termLikeLemmasKind′ public using () renaming
    ( _/_     to _Kind′/_
    ; _/Var_  to _Kind′/Var_
    ; weaken  to weakenKind′
    ; weaken⋆ to weakenKind′⋆
    )

  termLikeLemmasTermAsc : TermLikeLemmas TermAsc Term
  termLikeLemmasTermAsc = record
    { app        = SubstApp._TermAsc/_
    ; termLemmas = termLemmas
    ; /✶-↑✶₁     = KdOrTpLemmas./✶-↑✶ (termAscLemmas _ _)
    ; /✶-↑✶₂     = KdOrTpLemmas./✶-↑✶ (termAscLemmas _ _)
    }

  open TermLikeLemmas termLikeLemmasTermAsc public using () renaming
    ( termLikeSubst to termAscTermSubst
    ; _/_           to _TermAsc/_
    ; _/Var_        to _TermAsc/Var_
    ; weaken        to weakenTermAsc
    )

  termLikeLemmasElimAsc : TermLikeLemmas ElimAsc Term
  termLikeLemmasElimAsc = record
    { app        = SubstApp._ElimAsc/_
    ; termLemmas = termLemmas
    ; /✶-↑✶₁     = KdOrTpLemmas./✶-↑✶ (elimAscLemmas _ _)
    ; /✶-↑✶₂     = KdOrTpLemmas./✶-↑✶ (elimAscLemmas _ _)
    }

  open TermLikeLemmas termLikeLemmasElimAsc public using () renaming
    ( termLikeSubst to elimAscTermSubst
    ; _/_           to _ElimAsc/_
    ; _/Var_        to _ElimAsc/Var_
    ; weaken        to weakenElimAsc
    ; weaken⋆       to weakenElimAsc⋆
    )

  -- Weakening of heads and spines.

  weakenHead : ∀ {n} → Head n → Head (suc n)
  weakenHead a = a Head/Var VarSubst.wk

  weakenSpine : ∀ {n} → Spine n → Spine (suc n)
  weakenSpine a = a //Var VarSubst.wk

  -- Conversion of ascriptions commutes with weakening.

  ⌜⌝Asc-weaken : ∀ {n} (a : TermAsc n) →
                 ⌜ weakenTermAsc a ⌝Asc ≡ weakenElimAsc ⌜ a ⌝Asc
  ⌜⌝Asc-weaken (kd k) = cong kd (⌜⌝Kd-/Var k)
  ⌜⌝Asc-weaken (tp a) = cong tp (⌜⌝-/Var a)

  ⌞⌟Asc-weaken : ∀ {n} (a : ElimAsc n) →
                 ⌞ weakenElimAsc a ⌟Asc ≡ weakenTermAsc ⌞ a ⌟Asc
  ⌞⌟Asc-weaken (kd k) = cong kd (⌞⌟Kd-/Var k)
  ⌞⌟Asc-weaken (tp a) = cong tp (⌞⌟-/Var a)

  -- Simplified kinds are stable under weakening.

  ⌊⌋-weaken : ∀ {n} (k : Kind Term n) → ⌊ weakenKind k ⌋ ≡ ⌊ k ⌋
  ⌊⌋-weaken k = ⌊⌋-Kind/Var k

  ⌊⌋-weaken′ : ∀ {n} (k : Kind Elim n) → ⌊ weakenKind′ k ⌋ ≡ ⌊ k ⌋
  ⌊⌋-weaken′ k = ⌊⌋-Kind′/Var k

  ⌊⌋-weaken⋆′ : ∀ {m} n (k : Kind Elim m) → ⌊ weakenKind′⋆ n k ⌋ ≡ ⌊ k ⌋
  ⌊⌋-weaken⋆′ zero    k = refl
  ⌊⌋-weaken⋆′ (suc n) k = begin
    ⌊ weakenKind′ (weakenKind′⋆ n k) ⌋   ≡⟨ ⌊⌋-weaken′ (weakenKind′⋆ n k) ⟩
    ⌊ weakenKind′⋆ n k ⌋                 ≡⟨ ⌊⌋-weaken⋆′ n k ⟩
    ⌊ k ⌋                                ∎

  infix 10 _[_] _Elim[_] _Kind[_] _Kind′[_] _TermAsc[_] _ElimAsc[_]

  -- Shorthands for single-variable term substitutions.

  _[_] : ∀ {n} → Term (suc n) → Term n → Term n
  a [ b ] = a / sub b

  _Elim[_] : ∀ {n} → Elim (suc n) → Term n → Elim n
  a Elim[ b ] = a Elim/ sub b

  _Kind[_] : ∀ {n} → Kind Term (suc n) → Term n → Kind Term n
  k Kind[ b ] = k Kind/ (sub b)

  _Kind′[_] : ∀ {n} → Kind Elim (suc n) → Term n → Kind Elim n
  k Kind′[ b ] = k Kind′/ (sub b)

  _TermAsc[_] : ∀ {n} → TermAsc (suc n) → Term n → TermAsc n
  a TermAsc[ b ] = a TermAsc/ sub b

  _ElimAsc[_] : ∀ {n} → ElimAsc (suc n) → Term n → ElimAsc n
  a ElimAsc[ b ] = a ElimAsc/ sub b

  private module V  = VarSubst

  -- Kinds are stable under substitutions of a variable for a fresh
  -- variable (up to α-equivalence).

  Kind-wk↑-sub-zero-vanishes : ∀ {n} (k : Kind Term (suc n)) →
                               (k Kind/Var V.wk V.↑) Kind[ var zero ] ≡ k
  Kind-wk↑-sub-zero-vanishes k = begin
      (k Kind/Var V.wk V.↑) Kind[ var zero ]
    ≡⟨ sym (KL./-sub (k Kind/Var _) zero) ⟩
      k Kind/Var V.wk V.↑ Kind/Var V.sub zero
    ≡⟨ sym (LiftAppLemmas./-⊙ KL.varLiftAppLemmas k) ⟩
      k Kind/Var V.wk V.↑ V.⊙ V.sub zero
    ≡⟨⟩
      k Kind/Var (zero ∷ (Vec.map suc V.wk V.⊙ V.sub zero))
    ≡⟨ cong (λ σ → k Kind/Var (zero ∷ σ)) VarLemmas.map-weaken-⊙-sub ⟩
      k Kind/Var (zero ∷ V.wk)
    ≡⟨⟩
      k Kind/Var V.id
    ≡⟨ LiftAppLemmas.id-vanishes KL.varLiftAppLemmas k ⟩
      k
    ∎
    where
      open ≡-Reasoning
      module KL = TermLikeLemmas termLikeLemmasKind

----------------------------------------------------------------------
-- Typing contexts containing kind and type ascriptions.

-- Generic typing contexts over T-ascriptions and useful operations.

record KdOrTpCtx (T : ℕ → Set) : Set₁ where
  open Context public hiding (Ctx; CtxExt)

  -- Contexts and context extensions.

  Ctx     = Context.Ctx     (KdOrTp T)
  CtxExt  = Context.CtxExt  (KdOrTp T)

  -- Operations such as context lookup and substitutions in context
  -- extensions require some extra substitution machinery for
  -- T-ascriptions, all of which is provided by the following instance
  -- of TermLikeLemmas.

  field termLikeLemmas : TermLikeLemmas (KdOrTp T) Term
  open TermLikeLemmas termLikeLemmas
    using (termApplication; weaken; termLemmas)
  open TermLemmas termLemmas using (simple)

  weakenOps : Extension (KdOrTp T)
  weakenOps = record { weaken = weaken }

  open WeakenOps        weakenOps           public hiding (weaken; weaken⋆)
  open WeakenOpsLemmas  weakenOps           public
  open ConversionLemmas weakenOps weakenOps public

  open SubstOps termApplication simple public using (_E/_)

open Substitution

-- Concrete typing contexts over raw term and raw elimination
-- ascriptions.

termCtx : KdOrTpCtx Term
termCtx = record { termLikeLemmas = termLikeLemmasTermAsc }
module TermCtx = KdOrTpCtx termCtx

elimCtx : KdOrTpCtx Elim
elimCtx = record { termLikeLemmas = termLikeLemmasElimAsc }
module ElimCtx = KdOrTpCtx elimCtx

-- Concrete typing contexts over shape ascriptions and useful
-- operations.

module SimpleCtx where
  open Context public hiding (Ctx; CtxExt)
  open Maybe   public using  (Maybe) renaming (just to kd; nothing to tp)

  -- Shape ascriptions.
  --
  -- NOTE.  We only use shape ascriptions (or "simple" kind
  -- ascriptions) in the simplified kinding system, which is defined
  -- exclusively on types (see the FOmegaInt.Kinding.Simple module).
  -- Because simple kinding judgments can never refer to term
  -- variables, we may as well forget the type of such variables.  We
  -- just need to remember that there are such variables in the
  -- context so as to maintain the de Bruijn indexes of (type)
  -- variables, e.g. when we convert full kinding judgments to
  -- simplified ones.  Accordingly, we implement shape ascriptions
  -- using `Maybe' from the standard library, but with the
  -- constructors `just' and `nothing' renamed to `kd' and `tp' to
  -- better reflect their meaning.  (This renaming happens during the
  -- import of the `Maybe' module above.)

  SAsc : ℕ → Set
  SAsc _ = Maybe SKind

  -- Simplification/erasure of ascriptions.

  ⌊_⌋Asc : ∀ {T n} → KdOrTp T n → SAsc n
  ⌊ kd k ⌋Asc = kd ⌊ k ⌋
  ⌊ tp a ⌋Asc = tp

  -- Injectivity of the (simple) `kd' constructor.

  kd-inj′ : {j k : SKind} → _≡_ {A = Maybe SKind} (kd j) (kd k) → j ≡ k
  kd-inj′ refl = refl

  -- Contexts and context extensions over shape ascriptions.

  Ctx     = Context.Ctx     SAsc
  CtxExt  = Context.CtxExt  SAsc

  weakenOps : Extension SAsc
  weakenOps = record { weaken = Function.id }

  open WeakenOps        weakenOps           public hiding (weaken; weaken⋆)
  open WeakenOpsLemmas  weakenOps           public
  open ConversionLemmas weakenOps weakenOps public

  -- Change the indexing of a context extension.

  re-idx : ∀ {k m n} → CtxExt k n → CtxExt m n
  re-idx Γ = mapExt (λ _ k → k) Γ

  open Extension weakenOps public using () renaming (weaken⋆ to weakenSAsc⋆)

  weakenSAsc⋆-id : ∀ m {n a} → weakenSAsc⋆ m {n} a ≡ a
  weakenSAsc⋆-id zero    = refl
  weakenSAsc⋆-id (suc m) = weakenSAsc⋆-id m

  ⌊⌋-TermAsc/ : ∀ {m n} a {σ : Sub Term m n} → ⌊ a TermAsc/ σ ⌋Asc ≡ ⌊ a ⌋Asc
  ⌊⌋-TermAsc/ (kd k) = cong kd (⌊⌋-Kind/ k)
  ⌊⌋-TermAsc/ (tp t) = refl

  ⌊⌋-ElimAsc/ : ∀ {m n} a {σ : Sub Term m n} → ⌊ a ElimAsc/ σ ⌋Asc ≡ ⌊ a ⌋Asc
  ⌊⌋-ElimAsc/ (kd k) = cong kd (⌊⌋-Kind′/ k)
  ⌊⌋-ElimAsc/ (tp t) = refl

  ⌊⌋-ElimAsc/Var : ∀ {m n} a {σ : Sub Fin m n} →
                   ⌊ a ElimAsc/Var σ ⌋Asc ≡ ⌊ a ⌋Asc
  ⌊⌋-ElimAsc/Var (kd k) = cong kd (⌊⌋-Kind′/Var k)
  ⌊⌋-ElimAsc/Var (tp t) = refl

-- Conversions between the different context representations.

module ContextConversions where
  open Context
  open SimpleCtx using (kd; ⌊_⌋Asc; ⌊⌋-ElimAsc/Var)

  ⌞_⌟Ctx : ∀ {n} → ElimCtx.Ctx n → TermCtx.Ctx n
  ⌞ Γ ⌟Ctx = ElimCtx.map ⌞_⌟Asc Γ

  ⌜_⌝Ctx : ∀ {n} → TermCtx.Ctx n → ElimCtx.Ctx n
  ⌜ Γ ⌝Ctx = TermCtx.map ⌜_⌝Asc Γ

  ⌊_⌋Ctx : ∀ {T n} → Ctx (KdOrTp T) n → SimpleCtx.Ctx n
  ⌊ Γ ⌋Ctx = SimpleCtx.map ⌊_⌋Asc Γ

  ⌊_⌋CtxExt : ∀ {T m n} → CtxExt (KdOrTp T) m n → SimpleCtx.CtxExt m n
  ⌊ Γ ⌋CtxExt = SimpleCtx.mapExt (λ _ → ⌊_⌋Asc) Γ

  module ⌞⌟Ctx-Lemmas = ConversionLemmas ElimCtx.weakenOps TermCtx.weakenOps
  module ⌜⌝Ctx-Lemmas = ConversionLemmas TermCtx.weakenOps ElimCtx.weakenOps
  module ⌊⌋Ctx-Lemmas = ConversionLemmas ElimCtx.weakenOps SimpleCtx.weakenOps

  -- Context conversions commute with context lookup.

  ⌞⌟Asc-lookup : ∀ {n} (Γ : ElimCtx.Ctx n) x →
                 TermCtx.lookup ⌞ Γ ⌟Ctx x ≡ ⌞ ElimCtx.lookup Γ x ⌟Asc
  ⌞⌟Asc-lookup Γ x =
    ⌞⌟Ctx-Lemmas.lookup-map ⌞_⌟Asc Γ x (λ a → sym (⌞⌟Asc-weaken a))

  ⌜⌝Asc-lookup : ∀ {n} (Γ : TermCtx.Ctx n) x →
                 ElimCtx.lookup ⌜ Γ ⌝Ctx x ≡ ⌜ TermCtx.lookup Γ x ⌝Asc
  ⌜⌝Asc-lookup Γ x =
    ⌜⌝Ctx-Lemmas.lookup-map ⌜_⌝Asc Γ x (λ a → sym (⌜⌝Asc-weaken a))

  ⌊⌋Asc-lookup : ∀ {n} (Γ : ElimCtx.Ctx n) x →
                 SimpleCtx.lookup ⌊ Γ ⌋Ctx x ≡ ⌊ ElimCtx.lookup Γ x ⌋Asc
  ⌊⌋Asc-lookup Γ x =
    ⌊⌋Ctx-Lemmas.lookup-map ⌊_⌋Asc Γ x (λ a → sym (⌊⌋-ElimAsc/Var a))

  ⌊⌋-lookup : ∀ {n} (Γ : ElimCtx.Ctx n) x {k} → ElimCtx.lookup Γ x ≡ kd k →
              SimpleCtx.lookup ⌊ Γ ⌋Ctx x ≡ kd ⌊ k ⌋
  ⌊⌋-lookup Γ x {k} Γ[x]≡kd-k = begin
      SimpleCtx.lookup ⌊ Γ ⌋Ctx x
    ≡⟨ ⌊⌋Asc-lookup Γ x ⟩
      ⌊ ElimCtx.lookup Γ x ⌋Asc
    ≡⟨ cong ⌊_⌋Asc Γ[x]≡kd-k ⟩
      kd ⌊ k ⌋
    ∎
    where open ≡-Reasoning

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


text:
open import Poly
open import Function
open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Product as Prod
open import Data.Sum
open import Relation.Binary.PropositionalEquality

data ℕ∞ : Set where
  fin : ℕ → ℕ∞
  ω : ℕ∞

data _<'_ : ℕ∞ → ℕ∞ → Set where
  ltSuc : (n : ℕ) → fin n <' fin (suc n)
  ltω : (n : ℕ) → fin n <' ω

z : ⊤ → ℕ∞
z _ = fin 0

suc' : ℕ∞ → ℕ∞
suc' (fin x) = fin (suc x)
suc' ω = ω

F : (ℕ∞ → Set) → (ℕ∞ → Set)
F X n = (n ≡ z tt → ⊥)
        × ((k : ℕ∞) → n ≡ suc' k → X k)
        × ((n ≡ ω) → (∃ λ k → k <' ω × X k))

A = ℕ∞ × (⊥ ⊎ ⊤ ⊎ (∃ λ k → k <' ω))
B = ⊥ ⊎ ℕ∞ ⊎ (∃ λ k → k <' ω)

f : B → A
f (inj₁ x) = (z tt , inj₁ x)
f (inj₂ (inj₁ x)) = (suc' x , inj₂ (inj₁ tt))
f (inj₂ (inj₂ y)) = (ω , inj₂ (inj₂ y))

s : B → ℕ∞
s (inj₁ x) = ⊥-elim x
s (inj₂ (inj₁ x)) = x
s (inj₂ (inj₂ y)) = proj₁ y

t : A → ℕ∞
t = proj₁

P : DPoly
P = dpoly A t B f s

-- Claim : F ≅ ⟦ P ⟧

F→P : ∀{X} n → F X n → T P X n
F→P {X} (fin zero) v = ins a (abs'' a u)
  where
    a = (z tt , inj₁ (proj₁ v refl))
    u : (b : B) → f b ≡ a → X (s b)
    u b p with b
    u b refl | inj₁ _ = ⊥-elim (proj₁ v refl)
    u b ()   | inj₂ (inj₁ x)
    u b ()   | inj₂ (inj₂ y)

F→P {X} (fin (suc k)) (_ , v , _) = ins a (abs'' a u)
  where
    a = (fin (suc k) , inj₂ (inj₁ tt))
    u : (b : B) → f b ≡ a → X (s b)
    u b p with b
    u b ()   | inj₁ x
    u b refl | inj₂ (inj₁ (fin .k)) = v (fin k) refl
    u b ()   | inj₂ (inj₁ ω)
    u b ()   | inj₂ (inj₂ y)

F→P {X} ω (_ , _ , v) = ins a (abs'' a u)
  where
    i : ∃ λ k → k <' ω
    i = Prod.map id proj₁ (v refl)

    a = (ω , inj₂ (inj₂ i))

    u : (b : B) → f b ≡ a → X (s b)
    u b p with b
    u b ()   | inj₁ x
    u b ()   | inj₂ (inj₁ x)
    u b refl | inj₂ (inj₂ _) = proj₂ (proj₂ (v refl))

P→F : ∀{X} n → T P X n → F X n
P→F (fin zero) (ins (.(fin 0) , v) x) = ? -- ({!!} , {!!})
P→F (fin (suc n)) v = {!!}
P→F ω v = {!!}

ext: agda

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Numeric.Nat.Divide where

open import Prelude
open import Control.WellFounded
open import Numeric.Nat.Properties
open import Numeric.Nat.DivMod
open import Tactic.Nat

--- Divides predicate ---

data _Divides_ (a b : Nat) : Set where
  factor : ∀ q (eq : q * a ≡ b) → a Divides b

pattern factor! q = factor q refl

get-factor : ∀ {a b} → a Divides b → Nat
get-factor (factor q _) = q

dividesToDivMod : ∀ {a b} {{_ : NonZero b}} → b Divides a → DivMod a b
dividesToDivMod {b = zero } {{}}
dividesToDivMod {b = suc b} (factor q eq) = qr q 0 auto (by eq)

mod-divides : ∀ {a b} {{_ : NonZero a}} → a Divides b → b mod a ≡ 0
mod-divides {zero} {{}}
mod-divides {suc a} {b} (factor q eq) =
  rem-unique (b divmod suc a) (dividesToDivMod (factor q eq))

div-divides : ∀ {a b} {{_ : NonZero a}} → a Divides b → (b div a) * a ≡ b
div-divides {a} {b} a|b with divmod-sound a b
... | eq rewrite mod-divides a|b = by eq

private
  safediv : Nat → Nat → Nat
  safediv a 0 = 0
  safediv a (suc b) = a div suc b

  divides-safediv : ∀ {a b} → a Divides b → safediv b a * a ≡ b
  divides-safediv {zero } (factor! _) = auto
  divides-safediv {suc a} a|b = div-divides a|b

fast-divides : ∀ {a b} → a Divides b → a Divides b
fast-divides {a} {b} a|b = factor (safediv b a) (eraseEquality (divides-safediv a|b))

private
  no-divides-suc-mod : ∀ {a b} q {r} → LessNat (suc r) a → q * a + suc r ≡ b → ¬ (a Divides b)
  no-divides-suc-mod {zero} _ (diff _ ())
  no-divides-suc-mod {suc a} q {r} lt eq (factor q′ eq′) =
    refute (rem-unique
              (dividesToDivMod (factor q′ eq′))
              (qr q (suc r) lt eq))

  no-divides-zero : ∀ {a} → ¬ (0 Divides suc a)
  no-divides-zero {a} (factor q eq) = refute eq

_divides?_ : ∀ a b → Dec (a Divides b)
a     divides? zero  = yes (factor! 0)
zero  divides? suc b = no no-divides-zero
suc a divides? suc b with suc b divmod suc a
suc a divides? suc b | qr q  zero    _ eq  = yes (factor q (by eq))
suc a divides? suc b | qr q (suc r) lt eq₁ = no (no-divides-suc-mod q lt eq₁)

--- Instances ---

instance
  SmashDivides : ∀ {a b} {{_ : NonZero a}} → Smashed (a Divides b)
  SmashDivides {0} {{}}
  smashed {{SmashDivides {a@(suc _)}}} {factor q eq} {factor q₁ refl} =
    case mul-inj₁ q q₁ (suc _) eq of λ where refl → factor q $≡ smashed

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --prop --rewriting #-}

module Examples.Gcd.Clocked where

open import Calf.CostMonoid
import Calf.CostMonoids as CM

open import Calf CM.ℕ-CostMonoid
open import Calf.Types.Nat
open import Data.Nat using (_≤_; z≤n)
open import Calf.Types.Unit
open import Calf.Types.Bounded CM.ℕ-CostMonoid
open import Calf.Types.BoundedFunction CM.ℕ-CostMonoid

open import Data.Nat.DivMod
open import Relation.Binary.PropositionalEquality as P
open import Data.Product

open import Examples.Gcd.Euclid

{- Alternative definition of gcd with an explicit clock parameter.
   It is easier to see the computational behavior of the code in this version:
   1) when the clock is nonzero: the algorithm proceeds as normal
   2) clock is zero: algorithm terminates
   Crucially, if the recursor is by-name, then the value of the clock does not
   affect asymptotic behavior of the algorithm.
   Two things one can do in calf:
   1) give a good characterization of the clock in terms of the input by refining the raw recurrence (see Refine.agda)
   2) give a good characterization for of the clock for running the code; this usually
   means finding a clock computation that is simpler to compute
   than the "good" upperbound. For gcd, one can reuse the argument as the clock (see Spec.agda)
-}
gcd/clocked : cmp (Π nat λ _ → Π gcd/i λ _ → F nat)
gcd/clocked zero (x , y , h) = ret x
gcd/clocked (suc k) (x , 0 , h) =  ret {nat} x
gcd/clocked (suc k) (x , suc y , h) =
  bind {mod-tp x (suc y) triv} (F nat) (mod x (suc y) triv)
  λ { (z , eqn2) →
  let h2 = P.subst (λ k → suc k ≤ suc y) (P.sym eqn2) (m%n<n' x _ triv) in
  gcd/clocked k (suc y , z , h2) }

gcd : cmp (Π gcd/i λ _ → F nat)
gcd i = gcd/clocked (gcd/depth i) i

-- cost of clocked gcd is bounded by for any (not necessarily safe)
-- instantiation of the clock
gcd/clocked≤gcd/depth : ∀ k i → IsBounded nat (gcd/clocked k i) (gcd/depth i)
gcd/clocked≤gcd/depth zero i = bound/relax (λ _ → z≤n) bound/ret
gcd/clocked≤gcd/depth (suc k) (x , zero , h) = bound/ret
gcd/clocked≤gcd/depth (suc k) (x , suc y , h) rewrite gcd/depth-unfold-suc {x} {y} {h} =
  bound/step 1 _ (gcd/clocked≤gcd/depth k (suc y , x % suc y , m%n<n' x _ triv))

gcd≤gcd/depth : ∀ i → IsBounded nat (gcd i) (gcd/depth i)
gcd≤gcd/depth i = gcd/clocked≤gcd/depth (gcd/depth i) i

gcd/bounded : cmp (Ψ gcd/i (λ { _ → nat }) gcd/depth)
gcd/bounded = gcd , gcd≤gcd/depth

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

module LeibnizEquality where

------------------------------------------------------------------------------
-- The identity type.
data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

-- Leibniz equality (see [Luo 1994, sec. 5.1.3])

-- (From Agda/examples/lib/Logic/Leibniz.agda)
_≐_ : {A : Set} → A → A → Set₁
x ≐ y = (P : _ → Set) → P x → P y

-- Properties
≐-refl : {A : Set}{x : A} → x ≐ x
≐-refl P Px = Px

≐-sym : {A : Set}{x y : A} → x ≐ y → y ≐ x
≐-sym {x = x} {y} h P Py = h (λ z → P z → P x) (λ Px → Px) Py

≐-trans : {A : Set}{x y z : A} → x ≐ y → y ≐ z → x ≐ z
≐-trans h₁ h₂ P Px = h₂ P (h₁ P Px)

≐-subst : {A : Set}(P : A → Set){x y : A} → x ≐ y → P x → P y
≐-subst P h = h P

------------------------------------------------------------------------------
-- Leibniz's equality and the identity type

-- "In the presence of a type of propositions "Prop" one can also
-- define propositional equality by Leibniz's principle." [Hofmman
-- 1995, p. 4]

≐→≡ : {A : Set}{x y : A} → x ≐ y → x ≡ y
≐→≡ {x = x} h = h (λ z → x ≡ z) refl

≡→≐ : {A : Set}{x y : A} → x ≡ y → x ≐ y
≡→≐ refl P Px = Px

------------------------------------------------------------------------------
-- References
--
-- Hofmann, Martin (1995). Extensional concepts in intensional type
-- theory. PhD thesis. University of Edinburgh.

-- Luo, Zhaohui (1994). Computation and Reasoning. A Type Theory for
-- Computer Science. Oxford University Press.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

-- Definition of Pi with fractionals

module PiFrac where

-- From the standard library:
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂)

-- The basic types we add:
open import Singleton

infixr 70 _×ᵤ_
infixr 60 _+ᵤ_
infixr 50 _⊚_

------------------------------------------------------------------------------
-- Pi with fractionals

-- The following are all mutually dependent:

data 𝕌 : Set                               -- 𝕌niverse of types
⟦_⟧ : (A : 𝕌) → Set                        -- denotation of types
data _⟷_ : 𝕌 → 𝕌 → Set                     -- type equivalences
eval : {A B : 𝕌} → (A ⟷ B) → ⟦ A ⟧ → ⟦ B ⟧ -- evaluating an equivalence

data 𝕌 where
  𝟘       : 𝕌
  𝟙       : 𝕌
  _+ᵤ_    : 𝕌 → 𝕌 → 𝕌
  _×ᵤ_    : 𝕌 → 𝕌 → 𝕌
  ●_[_]   : (A : 𝕌) → ⟦ A ⟧ → 𝕌
  𝟙/●_[_] : (A : 𝕌) → ⟦ A ⟧ → 𝕌

⟦ 𝟘 ⟧ = ⊥
⟦ 𝟙 ⟧ = ⊤
⟦ t₁ +ᵤ t₂ ⟧ = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ t₁ ×ᵤ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
⟦ ● A [ v ] ⟧ = Singleton ⟦ A ⟧ v
⟦ 𝟙/● A [ v ] ⟧ = Recip ⟦ A ⟧ v

data _⟷_ where
  unite₊l : {t : 𝕌} → 𝟘 +ᵤ t ⟷ t
  uniti₊l : {t : 𝕌} → t ⟷ 𝟘 +ᵤ t
  unite₊r : {t : 𝕌} → t +ᵤ 𝟘 ⟷ t
  uniti₊r : {t : 𝕌} → t ⟷ t +ᵤ 𝟘
  swap₊   : {t₁ t₂ : 𝕌} → t₁ +ᵤ t₂ ⟷ t₂ +ᵤ t₁
  assocl₊ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ +ᵤ t₂) +ᵤ t₃
  assocr₊ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) +ᵤ t₃ ⟷ t₁ +ᵤ (t₂ +ᵤ t₃)
  unite⋆l : {t : 𝕌} → 𝟙 ×ᵤ t ⟷ t
  uniti⋆l : {t : 𝕌} → t ⟷ 𝟙 ×ᵤ t
  unite⋆r : {t : 𝕌} → t ×ᵤ 𝟙 ⟷ t
  uniti⋆r : {t : 𝕌} → t ⟷ t ×ᵤ 𝟙
  swap⋆   : {t₁ t₂ : 𝕌} → t₁ ×ᵤ t₂ ⟷ t₂ ×ᵤ t₁
  assocl⋆ : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) ×ᵤ t₃
  assocr⋆ : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₂) ×ᵤ t₃ ⟷ t₁ ×ᵤ (t₂ ×ᵤ t₃)
  absorbr : {t : 𝕌} → 𝟘 ×ᵤ t ⟷ 𝟘
  absorbl : {t : 𝕌} → t ×ᵤ 𝟘 ⟷ 𝟘
  factorzr : {t : 𝕌} → 𝟘 ⟷ t ×ᵤ 𝟘
  factorzl : {t : 𝕌} → 𝟘 ⟷ 𝟘 ×ᵤ t
  dist    : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) ×ᵤ t₃ ⟷ (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃)
  factor  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ +ᵤ t₂) ×ᵤ t₃
  distl   : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)
  factorl : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃) ⟷ t₁ ×ᵤ (t₂ +ᵤ t₃)
  id⟷     : {t : 𝕌} → t ⟷ t
  _⊚_     : {t₁ t₂ t₃ : 𝕌} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ +ᵤ t₂ ⟷ t₃ +ᵤ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ ×ᵤ t₂ ⟷ t₃ ×ᵤ t₄)
  -- new operations on Singleton
  lift : {t₁ t₂ : 𝕌} → {v₁ : ⟦ t₁ ⟧} →
           (c : t₁ ⟷ t₂) →
           (● t₁ [ v₁ ] ⟷ ● t₂ [ eval c v₁ ])
  tensorl : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            ● t₁ ×ᵤ t₂ [ v₁ , v₂ ] ⟷ ● t₁ [ v₁ ] ×ᵤ ● t₂ [ v₂ ]
  tensorr : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            ● t₁ [ v₁ ] ×ᵤ ● t₂ [ v₂ ] ⟷ ● t₁ ×ᵤ t₂ [ v₁ , v₂ ]
  plusll : {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} →
            ● (t₁ +ᵤ t₂) [ inj₁ v ] ⟷ ● t₁ [ v ]
  pluslr : {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} →
             ● t₁ [ v ] ⟷ ● (t₁ +ᵤ t₂) [ inj₁ v ]
  plusrl : {t₁ t₂ : 𝕌} {v : ⟦ t₂ ⟧} →
            ● (t₁ +ᵤ t₂) [ inj₂ v ] ⟷ ● t₂ [ v ]
  plusrr : {t₁ t₂ : 𝕌} {v : ⟦ t₂ ⟧} →
             ● t₂ [ v ] ⟷ ● (t₁ +ᵤ t₂) [ inj₂ v ]
  fracl : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            𝟙/● t₁ ×ᵤ t₂ [ v₁ , v₂ ] ⟷ 𝟙/● t₁ [ v₁ ] ×ᵤ 𝟙/● t₂ [ v₂ ]
  fracr : {t₁ t₂ : 𝕌} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} →
            𝟙/● t₁ [ v₁ ] ×ᵤ 𝟙/● t₂ [ v₂ ] ⟷ 𝟙/● t₁ ×ᵤ t₂ [ v₁ , v₂ ]
  -- fractionals
  η : {t : 𝕌} → (v : ⟦ t ⟧) → 𝟙 ⟷ ● t [ v ] ×ᵤ 𝟙/● t [ v ]
  ε : {t : 𝕌} → (v : ⟦ t ⟧) → ● t [ v ] ×ᵤ 𝟙/● t [ v ] ⟷ 𝟙
  -- double lift prop eq
  ll : ∀ {t : 𝕌} {v : ⟦ t ⟧} {w : ⟦ ● t [ v ] ⟧} →
        ● (● t [ v ]) [ w ]  ⟷ ● t [ v ]
  == : ∀ {t₁ t₂ : 𝕌} {v : ⟦ t₁ ⟧} {w w' : ⟦ t₂ ⟧} →
       (● t₁ [ v ] ⟷ ● t₂ [ w ]) → (w ≡ w') → (● t₁ [ v ] ⟷ ● t₂ [ w' ])

eval unite₊l (inj₂ v) = v
eval uniti₊l v  = inj₂ v
eval unite₊r (inj₁ v) = v
eval uniti₊r 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⋆l (tt , v) = v
eval uniti⋆l v = (tt , v)
eval unite⋆r (v , tt) = v
eval uniti⋆r v = (v , tt)
eval swap⋆ (v₁ , v₂)          = (v₂ , v₁)
eval assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
eval assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
eval absorbl ()
eval absorbr ()
eval factorzl ()
eval factorzr ()
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 distl (v , inj₁ v₁) = inj₁ (v , v₁)
eval distl (v , inj₂ v₂) = inj₂ (v , v₂)
eval factorl (inj₁ (v , v₁)) = (v , inj₁ v₁)
eval factorl (inj₂ (v , v₂)) = (v , inj₂ v₂)
eval id⟷ v = 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₂)
eval (lift c) (w , v≡w) = eval c w , cong (eval c) v≡w
eval tensorl ((w₁ , w₂) , vp≡wp) =
  (w₁ , cong proj₁ vp≡wp) , (w₂ , cong proj₂ vp≡wp)
eval tensorr ((w₁ , p₁) , (w₂ , p₂)) =
  (w₁ , w₂) , cong₂ _,_ p₁ p₂
eval (η v) tt = (v , refl) , λ _ → tt
eval (ε v) (p , f) = f p
eval (plusll {v = .w₁}) (inj₁ w₁ , refl) = w₁ , refl
eval pluslr (v₁ , refl) = inj₁ v₁ , refl
eval (plusrl {v = .w₂}) (inj₂ w₂ , refl) = w₂ , refl
eval plusrr (v₂ , refl) = inj₂ v₂ , refl
eval (fracl {v₁ = v₁} {v₂ = v₂}) f = (λ _ → f ((v₁ , v₂) , refl)) , (λ _ → f ((v₁ , v₂) , refl))
eval fracr (f₁ , f₂) ((w₁ , w₂) , refl) = let _ = f₁ (w₁ , refl) ; _ = f₂ (w₂ , refl) in tt
eval (ll {t} {v} {.w}) (w , refl) = v , refl
eval (== c eq) s₁ = let (w₂ , p) = eval c s₁ in w₂ , trans (sym eq) p

focus : {t : 𝕌} → (v : ⟦ t ⟧) → Singleton ⟦ t ⟧ v
focus v = (v , refl)

unfocus : {t : 𝕌} {v : ⟦ t ⟧} → Singleton ⟦ t ⟧ v → ⟦ t ⟧
unfocus (v , refl) = v

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )

import Web.Semantic.DL.Category.Composition
import Web.Semantic.DL.Category.Morphism
import Web.Semantic.DL.Category.Object
import Web.Semantic.DL.Category.Properties
import Web.Semantic.DL.Category.Tensor
import Web.Semantic.DL.Category.Unit
import Web.Semantic.DL.Category.Wiring

module Web.Semantic.DL.Category {Σ : Signature} where

infix 2 _≣_ _⇒_
infixr 5 _∙_ _⊗_ _⟨⊗⟩_

-- Categorial structure

Object : TBox Σ → TBox Σ → Set₁
Object = Web.Semantic.DL.Category.Object.Object

_⇒_ : ∀ {S T} → (Object S T) → (Object S T) → Set₁
_⇒_ = Web.Semantic.DL.Category.Morphism._⇒_

identity : ∀ {S T} (A : Object S T) → (A ⇒ A)
identity = Web.Semantic.DL.Category.Wiring.identity

_∙_ : ∀ {S T} {A B C : Object S T} → (A ⇒ B) → (B ⇒ C) → (A ⇒ C)
_∙_ = Web.Semantic.DL.Category.Composition._∙_

-- Symmetric monoidal structure

I : ∀ {S T} → Object S T
I = Web.Semantic.DL.Category.Unit.I

_⊗_ :  ∀ {S T} → Object S T → Object S T → Object S T
_⊗_ = Web.Semantic.DL.Category.Tensor._⊗_

_⟨⊗⟩_ : ∀ {S T : TBox Σ} {A₁ A₂ B₁ B₂ : Object S T} →
  (A₁ ⇒ B₁) → (A₂ ⇒ B₂) → ((A₁ ⊗ A₂) ⇒ (B₁ ⊗ B₂))
_⟨⊗⟩_ = Web.Semantic.DL.Category.Tensor._⟨⊗⟩_

symm : ∀ {S T : TBox Σ} → (A B : Object S T) → ((A ⊗ B) ⇒ (B ⊗ A))
symm = Web.Semantic.DL.Category.Wiring.symm

assoc : ∀ {S T : TBox Σ} → (A B C : Object S T) →
  (((A ⊗ B) ⊗ C) ⇒ (A ⊗ (B ⊗ C)))
assoc = Web.Semantic.DL.Category.Wiring.assoc

assoc⁻¹ : ∀ {S T : TBox Σ} → (A B C : Object S T) →
  ((A ⊗ (B ⊗ C)) ⇒ ((A ⊗ B) ⊗ C))
assoc⁻¹ = Web.Semantic.DL.Category.Wiring.assoc⁻¹

unit₁ : ∀ {S T : TBox Σ} (A : Object S T) → ((I ⊗ A) ⇒ A)
unit₁ = Web.Semantic.DL.Category.Wiring.unit₁

unit₁⁻¹ : ∀ {S T : TBox Σ} (A : Object S T) → (A ⇒ (I ⊗ A))
unit₁⁻¹ = Web.Semantic.DL.Category.Wiring.unit₁⁻¹

unit₂ : ∀ {S T : TBox Σ} (A : Object S T) → ((A ⊗ I) ⇒ A)
unit₂ = Web.Semantic.DL.Category.Wiring.unit₂

unit₂⁻¹ : ∀ {S T : TBox Σ} (A : Object S T) → (A ⇒ (A ⊗ I))
unit₂⁻¹ = Web.Semantic.DL.Category.Wiring.unit₂⁻¹

-- Equivalence of morphisms

_≣_ :  ∀ {S T} {A B : Object S T} → (A ⇒ B) → (A ⇒ B) → Set₁
_≣_ = Web.Semantic.DL.Category.Morphism._≣_

≣-refl : ∀ {S T} {A B : Object S T} (F : A ⇒ B) →
  (F ≣ F)
≣-refl = Web.Semantic.DL.Category.Properties.≣-refl

≣-sym :  ∀ {S T} {A B : Object S T} {F G : A ⇒ B} →
  (F ≣ G) → (G ≣ F)
≣-sym = Web.Semantic.DL.Category.Properties.≣-sym

≣-trans :  ∀ {S T} {A B : Object S T} {F G H : A ⇒ B} →
  (F ≣ G) → (G ≣ H) → (F ≣ H)
≣-trans = Web.Semantic.DL.Category.Properties.≣-trans

-- Equations of a category

compose-resp-≣ : ∀ {S T} {A B C : Object S T} {F₁ F₂ : A ⇒ B} {G₁ G₂ : B ⇒ C} →
  (F₁ ≣ F₂) → (G₁ ≣ G₂) → (F₁ ∙ G₁ ≣ F₂ ∙ G₂)
compose-resp-≣ = Web.Semantic.DL.Category.Properties.compose-resp-≣

compose-unit₁ : ∀ {S T} {A B C : Object S T} (F : A ⇒ B) →
  (identity A ∙ F ≣ F)
compose-unit₁ = Web.Semantic.DL.Category.Properties.compose-unit₁

compose-unit₂ : ∀ {S T} {A B C : Object S T} (F : A ⇒ B) →
  (F ∙ identity B ≣ F)
compose-unit₂ = Web.Semantic.DL.Category.Properties.compose-unit₂

compose-assoc : ∀ {S T} {A B C D : Object S T}
  (F : A ⇒ B) (G : B ⇒ C) (H : C ⇒ D) →
    ((F ∙ G) ∙ H ≣ F ∙ (G ∙ H))
compose-assoc = Web.Semantic.DL.Category.Properties.compose-assoc

-- Tensor is a bifunctor

tensor-resp-≣ : ∀ {S T} {A₁ A₂ B₁ B₂ : Object S T}
  {F₁ G₁ : A₁ ⇒ B₁} {F₂ G₂ : A₂ ⇒ B₂} →
    (F₁ ≣ G₁) → (F₂ ≣ G₂) → (F₁ ⟨⊗⟩ F₂ ≣ G₁ ⟨⊗⟩ G₂)
tensor-resp-≣ = Web.Semantic.DL.Category.Properties.tensor-resp-≣

tensor-resp-compose : ∀ {S T} {A₁ A₂ B₁ B₂ C₁ C₂ : Object S T}
  (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) (G₁ : B₁ ⇒ C₁) (G₂ : B₂ ⇒ C₂) →
    (((F₁ ∙ G₁) ⟨⊗⟩ (F₂ ∙ G₂)) ≣ ((F₁ ⟨⊗⟩ F₂) ∙ (G₁ ⟨⊗⟩ G₂)))
tensor-resp-compose = Web.Semantic.DL.Category.Properties.tensor-resp-compose

tensor-resp-id : ∀ {S T} (A₁ A₂ : Object S T) →
  ((identity A₁ ⟨⊗⟩ identity A₂) ≣ identity (A₁ ⊗ A₂))
tensor-resp-id = Web.Semantic.DL.Category.Properties.tensor-resp-id

-- Isomorphisms of a symmetric monoidal category

symm-iso : ∀ {S T} (A₁ A₂ : Object S T) →
  (symm A₁ A₂ ∙ symm A₂ A₁ ≣ identity (A₁ ⊗ A₂))
symm-iso = Web.Semantic.DL.Category.Properties.symm-iso

assoc-iso : ∀ {S T} (A₁ A₂ A₃ : Object S T) →
  (assoc A₁ A₂ A₃ ∙ assoc⁻¹ A₁ A₂ A₃ ≣ identity ((A₁ ⊗ A₂) ⊗ A₃))
assoc-iso = Web.Semantic.DL.Category.Properties.assoc-iso

assoc⁻¹-iso : ∀ {S T} (A₁ A₂ A₃ : Object S T) →
  (assoc⁻¹ A₁ A₂ A₃ ∙ assoc A₁ A₂ A₃ ≣ identity (A₁ ⊗ (A₂ ⊗ A₃)))
assoc⁻¹-iso = Web.Semantic.DL.Category.Properties.assoc⁻¹-iso

unit₁-iso : ∀ {S T} (A : Object S T) →
  (unit₁ A ∙ unit₁⁻¹ A ≣ identity (I ⊗ A))
unit₁-iso = Web.Semantic.DL.Category.Properties.unit₁-iso

unit₁⁻¹-iso : ∀ {S T} (A : Object S T) →
  (unit₁⁻¹ A ∙ unit₁ A ≣ identity A)
unit₁⁻¹-iso = Web.Semantic.DL.Category.Properties.unit₁⁻¹-iso

unit₂-iso : ∀ {S T} (A : Object S T) →
  (unit₂ A ∙ unit₂⁻¹ A ≣ identity (A ⊗ I))
unit₂-iso = Web.Semantic.DL.Category.Properties.unit₂-iso

unit₂⁻¹-iso : ∀ {S T} (A : Object S T) →
  (unit₂⁻¹ A ∙ unit₂ A ≣ identity A)
unit₂⁻¹-iso = Web.Semantic.DL.Category.Properties.unit₂⁻¹-iso

-- Coherence conditions of a symmetric monoidal category

assoc-unit : ∀ {S T} (A₁ A₂ : Object S T) →
  (assoc A₁ I A₂ ∙ (identity A₁ ⟨⊗⟩ unit₁ A₂) ≣ unit₂ A₁ ⟨⊗⟩ identity A₂)
assoc-unit = Web.Semantic.DL.Category.Properties.assoc-unit

assoc-assoc : ∀ {S T} (A₁ A₂ A₃ A₄ : Object S T) →
  (assoc (A₁ ⊗ A₂) A₃ A₄ ∙ assoc A₁ A₂ (A₃ ⊗ A₄) ≣
    (assoc A₁ A₂ A₃ ⟨⊗⟩ identity A₄) ∙ assoc A₁ (A₂ ⊗ A₃) A₄ ∙ (identity A₁ ⟨⊗⟩ assoc A₂ A₃ A₄))
assoc-assoc = Web.Semantic.DL.Category.Properties.assoc-assoc

assoc-symm : ∀ {S T} (A₁ A₂ A₃ : Object S T) →
  (symm (A₁ ⊗ A₂) A₃ ∙ assoc⁻¹ A₃ A₁ A₂ ≣
    assoc A₁ A₂ A₃ ∙ (identity A₁ ⟨⊗⟩ symm A₂ A₃) ∙ assoc⁻¹ A₁ A₃ A₂ ∙ (symm A₁ A₃ ⟨⊗⟩ identity A₂))
assoc-symm = Web.Semantic.DL.Category.Properties.assoc-symm

-- Naturality conditions of a symmetric monoidal category

unit₁-natural : ∀ {S T} {A B : Object S T} (F : A ⇒ B) →
  ((identity I ⟨⊗⟩ F) ∙ unit₁ B ≣ unit₁ A ∙ F)
unit₁-natural = Web.Semantic.DL.Category.Properties.unit₁-natural

unit₂-natural : ∀ {S T} {A B : Object S T} (F : A ⇒ B) →
  ((F ⟨⊗⟩ identity I) ∙ unit₂ B ≣ unit₂ A ∙ F)
unit₂-natural = Web.Semantic.DL.Category.Properties.unit₂-natural

symm-natural : ∀ {S T} {A₁ A₂ B₁ B₂ : Object S T}
  (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) →
    ((F₁ ⟨⊗⟩ F₂) ∙ symm B₁ B₂ ≣ symm A₁ A₂ ∙ (F₂ ⟨⊗⟩ F₁))
symm-natural = Web.Semantic.DL.Category.Properties.symm-natural

assoc-natural : ∀ {S T} {A₁ A₂ A₃ B₁ B₂ B₃ : Object S T}
  (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) (F₃ : A₃ ⇒ B₃) →
    (((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) ∙ assoc B₁ B₂ B₃ ≣
      assoc A₁ A₂ A₃ ∙ (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)))
assoc-natural = Web.Semantic.DL.Category.Properties.assoc-natural

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Explaining how to use the inspect idiom and elaborating on the way
-- it is implemented in the standard library.
------------------------------------------------------------------------

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

module README.Inspect where

open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Product
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Using inspect

-- We start with the definition of a (silly) predicate: `Plus m n p` states
-- that `m + n` is equal to `p` in a rather convoluted way. Crucially, it
-- distinguishes two cases: whether `p` is 0 or not.

Plus-eq : (m n p : ℕ) → Set
Plus-eq m n zero      = m ≡ 0 × n ≡ 0
Plus-eq m n p@(suc _) = m + n ≡ p

-- A sensible lemma to prove of this predicate is that whenever `p` is literally
-- `m + n` then `Plus m n p` holds. That is to say `∀ m n → Plus m n (m + n)`.
-- To be able to prove `Plus-eq m n (m + n)`, we need `m + n` to have either
-- the shape `zero` or `suc _` so that `Plus-eq` may reduce.

-- We could follow the way `_+_` computes by mimicking the same splitting
-- strategy, thus forcing `m + n` to reduce:

plus-eq-+ : ∀ m n → Plus-eq m n (m + n)
plus-eq-+ zero   zero    = refl , refl
plus-eq-+ zero   (suc n) = refl
plus-eq-+ (suc m) n      = refl

-- Or we could attempt to compute `m + n` first and check whether the result
-- is `zero` or `suc p`. By using `with m + n` and naming the result `p`,
-- the goal will become `Plus-eq m n p`. We can further refine this definition
-- by distinguishing two cases like so:

-- plus-eq-with : ∀ m n → Plus-eq m n (m + n)
-- plus-eq-with m n with m + n
-- ... | zero  = {!!}
-- ... | suc p = {!!}

-- The problem however is that we have abolutely lost the connection between the
-- computation `m + n` and its result `p`. Which makes the two goals unprovable:

-- 1. `m ≡ 0 × n ≡ 0`, with no assumption whatsoever
-- 2. `m + n ≡ suc p`, with no assumption either

-- By using the `with` construct, we have generated an auxiliary function that
-- looks like this:
-- `plus-eq-with-aux : ∀ m n p → Plus-eq m n p`
-- when we would have wanted a more precise type of the form:
-- `plus-eq-aux : ∀ m n p → m + n ≡ p → Plus-eq m n p`.

-- This is where we can use `inspect`. By using `with f x | inspect f x`,
-- we get both a `y` which is the result of `f x` and a proof that `f x ≡ y`.
-- Splitting on the result of `m + n`, we get two cases:

-- 1. `m ≡ 0 × n ≡ 0` under the assumption that `m + n ≡ zero`
-- 2. `m + n ≡ suc p` under the assumption that `m + n ≡ suc p`

-- The first one can be discharged using lemmas from Data.Nat.Properties and
-- the second one is trivial.

plus-eq-with : ∀ m n → Plus-eq m n (m + n)
plus-eq-with m n with m + n | inspect (m +_) n
... | zero  | [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
... | suc p | [ m+n≡1+p ] = m+n≡1+p

------------------------------------------------------------------------
-- Understanding the implementation of inspect

-- So why is it that we have to go through the record type `Reveal_·_is_`
-- and the ̀inspect` function? The fact is: we don't have to if we write
-- our own auxiliary lemma:

plus-eq-aux : ∀ m n → Plus-eq m n (m + n)
plus-eq-aux m n = aux m n (m + n) refl where

  aux : ∀ m n p → m + n ≡ p → Plus-eq m n p
  aux m n zero    m+n≡0   = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
  aux m n (suc p) m+n≡1+p = m+n≡1+p

-- The problem is that when we write ̀with f x | pr`, `with` decides to call `y`
-- the result `f x` and to replace *all* of the occurences of `f x` in the type
-- of `pr` with `y`. That is to say that if we were to write:

-- plus-eq-naïve : ∀ m n → Plus-eq m n (m + n)
-- plus-eq-naïve m n with m + n | refl {x = m + n}
-- ... | p | eq = {!!}

-- then `with` would abstract `m + n` as `p` on *both* sides of the equality
-- proven by `refl` thus giving us the following goal with an extra, useless,
-- assumption:

-- 1. `Plus-eq m n p` under the assumption that `p ≡ p`

-- So how does `inspect` work? The standard library uses a more general version
-- of the following type and function:

record MyReveal_·_is_ (f : ℕ → ℕ) (x y : ℕ) : Set where
  constructor [_]
  field eq : f x ≡ y

my-inspect : ∀ f n → MyReveal f · n is (f n)
my-inspect f n = [ refl ]

-- Given that `inspect` has the type `∀ f n → Reveal f · n is (f n)`, when we
-- write `with f n | inspect f n`, the only `f n` that can be abstracted in the
-- type of `inspect f n` is the third argument to `Reveal_·_is_`.

-- That is to say that the auxiliary definition generated looks like this:

plus-eq-reveal : ∀ m n → Plus-eq m n (m + n)
plus-eq-reveal m n = aux m n (m + n) (my-inspect (m +_) n) where

  aux : ∀ m n p → MyReveal (m +_) · n is p → Plus-eq m n p
  aux m n zero    [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
  aux m n (suc p) [ m+n≡1+p ] = m+n≡1+p

-- At the cost of having to unwrap the constructor `[_]` around the equality
-- we care about, we can keep relying on `with` and avoid having to roll out
-- handwritten auxiliary definitions.


text:
-- named arguments should be allowed in module applications
module Issue420 where

module M {A : Set₁} where

open M {A = Set}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Data.Bool.Base where

open import Level
open import Agda.Builtin.Bool using (Bool; true; false) public
open import Data.Unit

bool : ∀ {ℓ} {P : Bool → Type ℓ} (f : P false) (t : P true) → (x : Bool) → P x
bool f t false = f
bool f t true = t
{-# INLINE bool #-}

bool′ : A → A → Bool → A
bool′ = bool
{-# INLINE bool′ #-}

not : Bool → Bool
not false = true
not true = false

infixl 6 _or_
_or_ : Bool → Bool → Bool
false or y = y
true  or y = true

infixl 7 _and_
_and_ : Bool → Bool → Bool
false and y = false
true  and y = y

infixr 0 if_then_else_
if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if p then x else y = bool y x p
{-# INLINE if_then_else_ #-}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module sn-calculus-compatconf.in-lift where

open import sn-calculus-compatconf.base

open import sn-calculus
open import utility renaming (_U̬_ to _∪_)
open import context-properties
  using (get-view ; wrap-rho ; unwrap-rho
       ; ->E-view ; E-view-main-bind ; _a~_
       ; ->E-view-term ; ->E-view-inner-term ; done-E-view-term-disjoint)

open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.Binding
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Context.Properties
  using (plug)
open import Esterel.Environment as Env
  using (Env ; []env ; _←_)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; cong ; trans ; subst ; module ≡-Reasoning)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; _∷_ ; [] ; _++_ ; map)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)

open ->E-view

open EvaluationContext1
open _≐_⟦_⟧e
open Context1
open _≐_⟦_⟧c

{-
Base case where (E , C) = (_∷_ , []). LHS is arbitrary ->E-view reduction
and RHS is a merge. This case is delegated to R-confluence.

     p
  ρθ. E⟦E₁⟦qin⟧⟧       -- sn⟶₁ ->    ρθq. E⟦E₁⟦qo⟧⟧
 (ρθ) E⟦E₂⟦ρθ'.rin⟧⟧   -- sn⟶₁ ->   (ρθ)  E⟦ρθ'.E₂⟦rin⟧⟧
-}
1-steplρ-E-view-ecin-lift : ∀{E E₁ Ei p qin q qo rin r ro θ θq BV FV A Aq} →
  {ρθ·psn⟶₁ρθq·q  :  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θq  , Aq ⟩· q} →
  CorrectBinding p BV FV →

  (p≐E⟦qin⟧  :  p ≐ (E ++ (E₁ ∷ Ei)) ⟦ qin ⟧e) →
  (q≐E⟦qo⟧   :  q ≐ (E ++ (E₁ ∷ Ei)) ⟦ qo ⟧e) →
  ->E-view  ρθ·psn⟶₁ρθq·q  p≐E⟦qin⟧  q≐E⟦qo⟧ →

  (p≐E⟦rin⟧  :  p ≐ (map ceval E) ⟦ rin ⟧c) →
  (r≐E⟦ro⟧   :  r ≐ (map ceval E) ⟦ ro ⟧c) →
  (rinsn⟶₁ro  :  rin sn⟶₁ ro) →

  ⊥

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (depar₁ p'≐E⟦qin⟧) q≐E⟦qo⟧ e-view dchole dchole
  (rpar-done-right p'/halted q'/done) =
         (done-E-view-term-disjoint
           (dhalted (halted-⟦⟧e p'/halted p'≐E⟦qin⟧))
           (->E-view-inner-term e-view))

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (depar₂ q'≐E⟦qin⟧) q≐E⟦qo⟧ e-view dchole dchole
  (rpar-done-right p'/halted q'/done) =
         (done-E-view-term-disjoint
           (done-⟦⟧e q'/done q'≐E⟦qin⟧)
           (->E-view-inner-term e-view))

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (depar₁ p'≐E⟦qin⟧) q≐E⟦qo⟧ e-view dchole dchole
  (rpar-done-left p'/done q'/halted) =
         (done-E-view-term-disjoint
           (done-⟦⟧e p'/done p'≐E⟦qin⟧)
           (->E-view-inner-term e-view))

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (depar₂ q'≐E⟦qin⟧) q≐E⟦qo⟧ e-view dchole dchole
  (rpar-done-left p'/done q'/halted) =
         (done-E-view-term-disjoint
           (dhalted (halted-⟦⟧e q'/halted q'≐E⟦qin⟧))
           (->E-view-inner-term e-view))

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (deseq dehole) q≐E⟦qo⟧ () dchole dchole
  rseq-done

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (deseq dehole) q≐E⟦qo⟧ () dchole dchole
  rseq-exit

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (deloopˢ dehole) q≐E⟦qo⟧ () dchole dchole
  rloopˢ-exit

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (desuspend p≐E⟦qin⟧) q≐E⟦qo⟧ e-view dchole dchole
  (rsuspend-done p/halted) =
         (done-E-view-term-disjoint
           (dhalted (halted-⟦⟧e p/halted p≐E⟦qin⟧))
           (->E-view-inner-term e-view))

1-steplρ-E-view-ecin-lift {[]} {ρθ·psn⟶₁ρθq·q = ρθ·psn⟶₁ρθq·q} cb
  (detrap p≐E⟦qin⟧) q≐E⟦qo⟧ e-view dchole dchole
  (rtrap-done p/halted) =
         (done-E-view-term-disjoint
           (dhalted (halted-⟦⟧e p/halted p≐E⟦qin⟧))
           (->E-view-inner-term e-view))

1-steplρ-E-view-ecin-lift {E₁ ∷ E} {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBpar cbp cbq _ _ _ _)
  (depar₁ p≐E⟦qin⟧) (depar₁ q≐E⟦qo⟧) e-view-E₁
  (dcpar₁ p≐E⟦rin⟧) (dcpar₁ r≐E⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (depar₁ p≐E⟦qin⟧) (depar₁ q≐E⟦qo⟧)
         p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view) =
  1-steplρ-E-view-ecin-lift cbp p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐E⟦rin⟧ r≐E⟦ro⟧ rinsn⟶₁ro

1-steplρ-E-view-ecin-lift {E₁ ∷ E} {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBpar cbp cbq _ _ _ _)
  (depar₂ p≐E⟦qin⟧) (depar₂ q≐E⟦qo⟧) e-view-E₁
  (dcpar₂ p≐E⟦rin⟧) (dcpar₂ r≐E⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (depar₂ p≐E⟦qin⟧) (depar₂ q≐E⟦qo⟧)
         p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view) =
  1-steplρ-E-view-ecin-lift cbq p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐E⟦rin⟧ r≐E⟦ro⟧ rinsn⟶₁ro

1-steplρ-E-view-ecin-lift {E₁ ∷ E} {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBseq cbp cbq _)
  (deseq p≐E⟦qin⟧) (deseq q≐E⟦qo⟧) e-view-E₁
  (dcseq₁ p≐E⟦rin⟧) (dcseq₁ r≐E⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (deseq p≐E⟦qin⟧) (deseq q≐E⟦qo⟧)
         p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view) =
  1-steplρ-E-view-ecin-lift cbp p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐E⟦rin⟧ r≐E⟦ro⟧ rinsn⟶₁ro

1-steplρ-E-view-ecin-lift {E₁ ∷ E} {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBloopˢ cbp cbq _ _)
  (deloopˢ p≐E⟦qin⟧) (deloopˢ q≐E⟦qo⟧) e-view-E₁
  (dcloopˢ₁ p≐E⟦rin⟧) (dcloopˢ₁ r≐E⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (deloopˢ p≐E⟦qin⟧) (deloopˢ q≐E⟦qo⟧)
         p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view) =
  1-steplρ-E-view-ecin-lift cbp p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐E⟦rin⟧ r≐E⟦ro⟧ rinsn⟶₁ro

1-steplρ-E-view-ecin-lift {E₁ ∷ E} {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBsusp cb' _)
  (desuspend p≐E⟦qin⟧) (desuspend q≐E⟦qo⟧) e-view-E₁
  (dcsuspend p≐E⟦rin⟧) (dcsuspend r≐E⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (desuspend p≐E⟦qin⟧) (desuspend q≐E⟦qo⟧)
         p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view) =
  1-steplρ-E-view-ecin-lift cb' p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐E⟦rin⟧ r≐E⟦ro⟧ rinsn⟶₁ro

1-steplρ-E-view-ecin-lift {E₁ ∷ E} {ρθ·psn⟶₁ρθq·q = ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧}
  cb@(CBtrap cb')
  (detrap p≐E⟦qin⟧) (detrap q≐E⟦qo⟧) e-view-E₁
  (dctrap p≐E⟦rin⟧) (dctrap r≐E⟦ro⟧) rinsn⟶₁ro
  with unwrap-rho ρθ·E₁⟦p⟧sn⟶₁ρθq·E₁⟦q⟧ (detrap p≐E⟦qin⟧) (detrap q≐E⟦qo⟧)
         p≐E⟦qin⟧ q≐E⟦qo⟧ e-view-E₁
... | (ρθ·psn⟶₁ρθq·q , e-view) =
  1-steplρ-E-view-ecin-lift cb' p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐E⟦rin⟧ r≐E⟦ro⟧ rinsn⟶₁ro

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
-- Modified: Andreas, 2011-04-11 freezing metas, removed unused uni.poly

{-# OPTIONS --guardedness-preserving-type-constructors #-}

module UnusedArgsInPositivity where

open import Common.Coinduction

module Ex₁ where
  data Unit : Set where
    unit : Unit

  unused : Set → Unit → Set → Set
  unused X unit Y = Y

  mutual

    data D : Set where
      d : (x : Unit) → (El x x → D) → D

    El : Unit → Unit → Set
    El unit x = unused D x Unit

module Ex₂ where

  data Maybe (A : Set) : Set where

  data Rec (A : ∞ Set) : Set where
    fold : ♭ A → Rec A

  mutual

    data Data : Set where
      maybe : ∞ Data -> Data
      sigma : (A : Data) → (El A → Data) -> Data

    El : Data → Set
    El (maybe A) = Rec (♯ Maybe (El (♭ {A = Data} A)))
    El (sigma A B) = El A

  {- This fails for 2 reasons:
     1. Rec doesn't preserve guardedness (hence -no-termination-check)
     2. Data "appears" in the definition of El
  The 1st one is now fixed.
  It is not clear how to fix the 2nd. Irrelevant parameters?
  -}

{-
/Users/txa/current/AIMXI/DataGuard.agda:15,8-12
Data is not strictly positive, because it occurs in the type of the
constructor sigma in the definition of Data, which occurs in the
second argument to ♭ in the first argument to El in the second
argument to Maybe in the first clause in the definition of
.DataGuard.♯-0, which occurs in the third clause in the definition
of El.
-}

module Ex₃ where
  data D (A : Set) : Set where
    d : D A

  data E : Set where
    e : (D E → E) → E

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


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

module M-types.Base.Axiom where
    open import M-types.Base.Core public
    open import M-types.Base.Sum public
    open import M-types.Base.Prod public
    open import M-types.Base.Eq public
    open import M-types.Base.Equi public

    postulate
        funext-axiom : {X : Ty ℓ₀} {Y : X → Ty ℓ₁} {f₀ f₁ : ∏ X Y} →
            IsEqui {_} {_} {f₀ ≡ f₁} {∏[ x ∈ X ] f₀ x ≡ f₁ x} (≡-apply)

    funext :  {X : Ty ℓ₀} {Y : X → Ty ℓ₁} {f₀ f₁ : ∏ X Y} →
        (∏[ x ∈ X ] f₀ x ≡ f₁ x) → f₀ ≡ f₁
    funext = inv (≡-apply , funext-axiom)

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


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

module Dodo.Binary.Product where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Function using (flip)
open import Data.Product using (_×_; _,_; map₁; map₂)
open import Relation.Unary using (Pred; _∈_)
open import Relation.Binary using (REL; Rel)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Binary.Equality
open import Dodo.Binary.Domain
open import Dodo.Binary.Composition

infix 40 _×₂_

_×₂_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
  → Pred A ℓ₁
  → Pred B ℓ₂
    -----------------
  → REL A B (ℓ₁ ⊔ ℓ₂)
_×₂_ P Q x y = P x × Q y

-- ## Operations: ×₂ ##

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {d : Pred A ℓ₁} {r : Pred B ℓ₂} where

  ×₂-dom : ∀ {x : A} {y : B} → ( d ×₂ r ) x y → d x
  ×₂-dom (dx , ry) = dx

  ×₂-codom : ∀ {x : A} {y : B} → ( d ×₂ r ) x y → r y
  ×₂-codom (dx , ry) = ry

  ×₂-flip : ∀ {x : A} {y : B} → ( d ×₂ r ) x y → ( r ×₂ d ) y x
  ×₂-flip (dx , ry) = (ry , dx)

module _ {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b}
    {d₁ : Pred A ℓ₁} {d₂ : Pred A ℓ₂} {r₁ : Pred B ℓ₃} {r₂ : Pred B ℓ₄} where

  ×₂-lift : ( d₁ ⊆₁ d₂ ) → ( r₁ ⊆₁ r₂ ) → d₁ ×₂ r₁ ⊆₂ d₂ ×₂ r₂
  ×₂-lift f g = ⊆: lemma
    where
    lemma : d₁ ×₂ r₁ ⊆₂' d₂ ×₂ r₂
    lemma x y (d₁x , r₁y) = (⊆₁-apply f d₁x , ⊆₁-apply g r₁y)

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b} {R : REL A B ℓ₁}
    {d : Pred A ℓ₂} {r : Pred B ℓ₃} where

  ×₂-applyˡ : R ⊆₂ ( d ×₂ r ) → {x : A} {y : B} → R x y → d x
  ×₂-applyˡ R⊆₂d×r Rxy = ×₂-dom {d = d} {r = r} (⊆₂-apply R⊆₂d×r Rxy)

  ×₂-apply-dom : R ⊆₂ (d ×₂ r) → {x : A} → x ∈ dom R → d x
  ×₂-apply-dom R⊆d×r (y , Rxy) = ×₂-applyˡ R⊆d×r Rxy

  ×₂-applyʳ : R ⊆₂ ( d ×₂ r ) → {x : A} {y : B} → R x y → r y
  ×₂-applyʳ R⊆₂d×r Rxy = ×₂-codom {d = d} {r = r} (⊆₂-apply R⊆₂d×r Rxy)

  ×₂-apply-codom : R ⊆₂ (d ×₂ r) → {y : B} → y ∈ codom R → r y
  ×₂-apply-codom R⊆d×r (x , Rxy) = ×₂-applyʳ R⊆d×r Rxy

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {Q : REL A B ℓ₁} {d : A → Set ℓ₂} {r : B → Set ℓ₃} where

  ×₂-flip-⊆₂ : Q ⊆₂ d ×₂ r → flip Q ⊆₂ r ×₂ d
  ×₂-flip-⊆₂ (⊆: Q⊆×) = ⊆: lemma
    where
    lemma : flip Q ⊆₂' r ×₂ d
    lemma x y Qyx with Q⊆× y x Qyx
    ... | (dy , rx) = (rx , dy)

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a}
    {R : Rel A ℓ₁} {P : Pred A ℓ₂} where

  ×₂-lift-udr :
      udr R ⊆₁ P
      -----------
    → R ⊆₂ P ×₂ P
  ×₂-lift-udr udrR⊆P = ⊆: lemma
    where
    lemma : R ⊆₂' P ×₂ P
    lemma x y Rxy = ⊆₁-apply udrR⊆P (take-udrˡ R Rxy) , ⊆₁-apply udrR⊆P (take-udrʳ R Rxy)

module _ {a b ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {B : Set b}
    {R : REL A B ℓ₁} {P : Pred A ℓ₂} {Q : Pred B ℓ₃} where

  ×₂-lift-dom :
      dom R ⊆₁ P
    → codom R ⊆₁ Q
      ------------
    → R ⊆₂ P ×₂ Q
  ×₂-lift-dom (⊆: dom⊆P) (⊆: codom⊆Q) = ⊆: lemma
    where
    lemma : R ⊆₂' P ×₂ Q
    lemma x y Rxy = (dom⊆P x (take-dom R Rxy) , codom⊆Q y (take-codom R Rxy))

module _ {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b}
    {Q : REL A B ℓ₁} {d₁ : Pred A ℓ₂} {d₂ : Pred A ℓ₃} {r : B → Set ℓ₄} where

  ×₂-⊆ˡ :
      d₁ ⊆₁ d₂
      ------------------
    → d₁ ×₂ r ⊆₂ d₂ ×₂ r
  ×₂-⊆ˡ d₁⊆d₂ = ⊆: lemma
    where
    lemma : d₁ ×₂ r ⊆₂' d₂ ×₂ r
    lemma x y = map₁ (⊆₁-apply d₁⊆d₂)

module _ {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b}
    {Q : REL A B ℓ₁} {d : Pred A ℓ₂} {r₁ : Pred B ℓ₃} {r₂ : Pred B ℓ₄} where

  ×₂-⊆ʳ :
      r₁ ⊆₁ r₂
      ------------------
    → d ×₂ r₁ ⊆₂ d ×₂ r₂
  ×₂-⊆ʳ r₁⊆r₂ = ⊆: lemma
    where
    lemma : d ×₂ r₁ ⊆₂' d ×₂ r₂
    lemma x y = map₂ (⊆₁-apply r₁⊆r₂)

module _ {a b c ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b} {C : Set c}
    {d₁ : Pred A ℓ₁} {r₁ : Pred B ℓ₂} {d₂ : Pred B ℓ₃} {r₂ : Pred C ℓ₄} where

  ×₂-combine-⨾ : ( d₁ ×₂ r₁ ) ⨾ ( d₂ ×₂ r₂ ) ⊆₂ d₁ ×₂ r₂
  ×₂-combine-⨾ = ⊆: lemma
    where
    lemma : ( d₁ ×₂ r₁ ) ⨾ ( d₂ ×₂ r₂ ) ⊆₂' d₁ ×₂ r₂
    lemma x y ((d₁x , r₁z) ⨾[ z ]⨾ (d₂z , r₂y)) = (d₁x , r₂y)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo