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

-- Monoidal natural isomorphisms between lax and strong braided
-- monoidal functors.
--
-- NOTE. Braided monoidal natural isomorphisms are really just
-- monoidal natural isomorphisms that happen to go between braided
-- monoidal functors.  No additional conditions are necessary.
-- Nevertheless, the definitions in this module are useful when one is
-- working in a braided monoidal setting.  They also help Agda's type
-- checker by bundling the (braided monoidal) categories and functors
-- involved.

module Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Braided
  where

open import Level
open import Relation.Binary using (IsEquivalence)

open import Categories.Category.Monoidal using (BraidedMonoidalCategory)
import Categories.Functor.Monoidal.Braided as BMF
open import Categories.Functor.Monoidal.Properties using () renaming
  ( idF-BraidedMonoidal to idFˡ  ; idF-StrongBraidedMonoidal to idFˢ
  ; ∘-BraidedMonoidal   to _∘Fˡ_ ; ∘-StrongBraidedMonoidal   to _∘Fˢ_
  )
open import Categories.NaturalTransformation.NaturalIsomorphism as NI
  using (NaturalIsomorphism)
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal as MNI

module Lax where
  open BMF.Lax using (BraidedMonoidalFunctor)
  open MNI.Lax using (IsMonoidalNaturalIsomorphism)
  open BraidedMonoidalFunctor using () renaming (F to UF; monoidalFunctor to MF)
  private module U = MNI.Lax

  module _ {o ℓ e o′ ℓ′ e′}
           {C : BraidedMonoidalCategory o ℓ e}
           {D : BraidedMonoidalCategory o′ ℓ′ e′} where

    -- Monoidal natural isomorphisms between lax braided monoidal functors.

    record BraidedMonoidalNaturalIsomorphism
           (F G : BraidedMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where

      field
        U              : NaturalIsomorphism (UF F) (UF G)
        F⇒G-isMonoidal : IsMonoidalNaturalIsomorphism (MF F) (MF G) U

      ⌊_⌋ : U.MonoidalNaturalIsomorphism (MF F) (MF G)
      ⌊_⌋ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }

      open U.MonoidalNaturalIsomorphism ⌊_⌋ public hiding (U; F⇒G-isMonoidal)

    infix 4 _≃_

    _≃_ = BraidedMonoidalNaturalIsomorphism

    -- "Strengthening"

    ⌈_⌉ : {F G : BraidedMonoidalFunctor C D} →
          U.MonoidalNaturalIsomorphism (MF F) (MF G) → F ≃ G
    ⌈ α ⌉ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }
      where open U.MonoidalNaturalIsomorphism α

    open BraidedMonoidalNaturalIsomorphism

    -- Identity and compositions

    infixr 9 _ⓘᵥ_

    id : {F : BraidedMonoidalFunctor C D} → F ≃ F
    id = ⌈ U.id ⌉

    _ⓘᵥ_ : {F G H : BraidedMonoidalFunctor C D} → G ≃ H → F ≃ G → F ≃ H
    α ⓘᵥ β   = ⌈ ⌊ α ⌋ U.ⓘᵥ ⌊ β ⌋ ⌉

    isEquivalence : IsEquivalence _≃_
    isEquivalence = record
      { refl  = id
      ; sym   = λ α → record
        { U              = NI.sym (U α)
        ; F⇒G-isMonoidal = F⇐G-isMonoidal α
        }
      ; trans = λ α β → β ⓘᵥ α
      }
      where

  open BraidedMonoidalNaturalIsomorphism

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : BraidedMonoidalCategory o ℓ e}
           {D : BraidedMonoidalCategory o′ ℓ′ e′}
           {E : BraidedMonoidalCategory o″ ℓ″ e″} where

    infixr 9 _ⓘₕ_ _ⓘˡ_ _ⓘʳ_

    _ⓘₕ_ : {F G : BraidedMonoidalFunctor C D}
           {H I : BraidedMonoidalFunctor D E} →
           H ≃ I → F ≃ G → (H ∘Fˡ F) ≃ (I ∘Fˡ G)
    -- NOTE: this definition is clearly equivalent to
    --
    --   α ⓘₕ β = ⌈ ⌊ α ⌋ U.ⓘₕ ⌊ β ⌋ ⌉
    --
    -- but the latter takes an unreasonably long time to typecheck,
    -- while the unfolded version typechecks almost immediately.
    α ⓘₕ β = record
      { U               = C.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = C.ε-compat
        ; ⊗-homo-compat = C.⊗-homo-compat }
        }
      where module C = U.MonoidalNaturalIsomorphism (⌊ α ⌋ U.ⓘₕ ⌊ β ⌋)

    _ⓘˡ_ : {F G : BraidedMonoidalFunctor C D}
           (H : BraidedMonoidalFunctor D E) → F ≃ G → (H ∘Fˡ F) ≃ (H ∘Fˡ G)
    H ⓘˡ α = id {F = H} ⓘₕ α

    _ⓘʳ_ : {G H : BraidedMonoidalFunctor D E} →
           G ≃ H → (F : BraidedMonoidalFunctor C D) → (G ∘Fˡ F) ≃ (H ∘Fˡ F)
    α ⓘʳ F = α ⓘₕ id {F = F}

  -- Left and right unitors.

  module _ {o ℓ e o′ ℓ′ e′}
           {C : BraidedMonoidalCategory o ℓ e}
           {D : BraidedMonoidalCategory o′ ℓ′ e′}
           {F : BraidedMonoidalFunctor C D} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    unitorˡ : idFˡ D ∘Fˡ F ≃ F
    unitorˡ = record
      { U               = LU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = LU.ε-compat
        ; ⊗-homo-compat = LU.⊗-homo-compat
        }
      }
      where module LU = U.MonoidalNaturalIsomorphism (U.unitorˡ {F = MF F})

    unitorʳ : F ∘Fˡ idFˡ C ≃ F
    unitorʳ = record
      { U               = RU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = RU.ε-compat
        ; ⊗-homo-compat = RU.⊗-homo-compat
        }
      }
      where module RU = U.MonoidalNaturalIsomorphism (U.unitorʳ {F = MF F})

  -- Associator.

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
           {B : BraidedMonoidalCategory o ℓ e}
           {C : BraidedMonoidalCategory o′ ℓ′ e′}
           {D : BraidedMonoidalCategory o″ ℓ″ e″}
           {E : BraidedMonoidalCategory o‴ ℓ‴ e‴}
           {F : BraidedMonoidalFunctor B C} {G : BraidedMonoidalFunctor C D}
           {H : BraidedMonoidalFunctor D E} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    associator : (H ∘Fˡ G) ∘Fˡ F ≃ H ∘Fˡ (G ∘Fˡ F)
    associator = record
      { U               = AU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = AU.ε-compat
        ; ⊗-homo-compat = AU.⊗-homo-compat
        }
      }
      where
        module AU =
          U.MonoidalNaturalIsomorphism (U.associator {F = MF F} {MF G} {MF H})

module Strong where
  open BMF.Strong using (BraidedMonoidalFunctor)
  open MNI.Strong using (IsMonoidalNaturalIsomorphism)
  open BraidedMonoidalFunctor using () renaming
    ( F                         to UF
    ; monoidalFunctor           to MF
    ; laxBraidedMonoidalFunctor to laxBMF
    )
  private module U = MNI.Strong

  module _ {o ℓ e o′ ℓ′ e′}
           {C : BraidedMonoidalCategory o ℓ e}
           {D : BraidedMonoidalCategory o′ ℓ′ e′} where

    -- Monoidal natural isomorphisms between strong braided monoidal functors.

    record BraidedMonoidalNaturalIsomorphism
           (F G : BraidedMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where

      field
        U              : NaturalIsomorphism (UF F) (UF G)
        F⇒G-isMonoidal : IsMonoidalNaturalIsomorphism (MF F) (MF G) U

      ⌊_⌋ : U.MonoidalNaturalIsomorphism (MF F) (MF G)
      ⌊_⌋ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }

      laxBNI : Lax.BraidedMonoidalNaturalIsomorphism (laxBMF F) (laxBMF G)
      laxBNI = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }

      open Lax.BraidedMonoidalNaturalIsomorphism laxBNI public
        hiding (U; F⇒G-isMonoidal; ⌊_⌋)

    infix 4 _≃_

    _≃_ = BraidedMonoidalNaturalIsomorphism

    -- "Strengthening"

    ⌈_⌉ : {F G : BraidedMonoidalFunctor C D} →
          U.MonoidalNaturalIsomorphism (MF F) (MF G) → F ≃ G
    ⌈ α ⌉ = record { U = U ; F⇒G-isMonoidal = F⇒G-isMonoidal }
      where open U.MonoidalNaturalIsomorphism α

    open BraidedMonoidalNaturalIsomorphism

    -- Identity and compositions

    infixr 9 _ⓘᵥ_

    id : {F : BraidedMonoidalFunctor C D} → F ≃ F
    id = ⌈ U.id ⌉

    _ⓘᵥ_ : {F G H : BraidedMonoidalFunctor C D} → G ≃ H → F ≃ G → F ≃ H
    α ⓘᵥ β   = ⌈ ⌊ α ⌋ U.ⓘᵥ ⌊ β ⌋ ⌉

    isEquivalence : IsEquivalence _≃_
    isEquivalence = record
      { refl  = id
      ; sym   = λ α → record
        { U              = NI.sym (U α)
        ; F⇒G-isMonoidal = F⇐G-isMonoidal α
        }
      ; trans = λ α β → β ⓘᵥ α
      }
      where

  open BraidedMonoidalNaturalIsomorphism

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : BraidedMonoidalCategory o ℓ e}
           {D : BraidedMonoidalCategory o′ ℓ′ e′}
           {E : BraidedMonoidalCategory o″ ℓ″ e″} where

    infixr 9 _ⓘₕ_ _ⓘˡ_ _ⓘʳ_

    _ⓘₕ_ : {F G : BraidedMonoidalFunctor C D}
           {H I : BraidedMonoidalFunctor D E} →
           H ≃ I → F ≃ G → (H ∘Fˢ F) ≃ (I ∘Fˢ G)
    -- NOTE: this definition is clearly equivalent to
    --
    --   α ⓘₕ β = ⌈ ⌊ α ⌋ U.ⓘₕ ⌊ β ⌋ ⌉
    --
    -- but the latter takes an unreasonably long time to typecheck,
    -- while the unfolded version typechecks almost immediately.
    α ⓘₕ β = record
      { U               = C.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = C.ε-compat
        ; ⊗-homo-compat = C.⊗-homo-compat }
        }
      where module C = U.MonoidalNaturalIsomorphism (⌊ α ⌋ U.ⓘₕ ⌊ β ⌋)

    _ⓘˡ_ : {F G : BraidedMonoidalFunctor C D}
           (H : BraidedMonoidalFunctor D E) → F ≃ G → (H ∘Fˢ F) ≃ (H ∘Fˢ G)
    H ⓘˡ α = id {F = H} ⓘₕ α

    _ⓘʳ_ : {G H : BraidedMonoidalFunctor D E} →
           G ≃ H → (F : BraidedMonoidalFunctor C D) → (G ∘Fˢ F) ≃ (H ∘Fˢ F)
    α ⓘʳ F = α ⓘₕ id {F = F}

  -- Left and right unitors.

  module _ {o ℓ e o′ ℓ′ e′}
           {C : BraidedMonoidalCategory o ℓ e}
           {D : BraidedMonoidalCategory o′ ℓ′ e′}
           {F : BraidedMonoidalFunctor C D} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    unitorˡ : idFˢ D ∘Fˢ F ≃ F
    unitorˡ = record
      { U               = LU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = LU.ε-compat
        ; ⊗-homo-compat = LU.⊗-homo-compat
        }
      }
      where module LU = U.MonoidalNaturalIsomorphism (U.unitorˡ {F = MF F})

    unitorʳ : F ∘Fˢ idFˢ C ≃ F
    unitorʳ = record
      { U               = RU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = RU.ε-compat
        ; ⊗-homo-compat = RU.⊗-homo-compat
        }
      }
      where module RU = U.MonoidalNaturalIsomorphism (U.unitorʳ {F = MF F})

  -- Associator.

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
           {B : BraidedMonoidalCategory o ℓ e}
           {C : BraidedMonoidalCategory o′ ℓ′ e′}
           {D : BraidedMonoidalCategory o″ ℓ″ e″}
           {E : BraidedMonoidalCategory o‴ ℓ‴ e‴}
           {F : BraidedMonoidalFunctor B C} {G : BraidedMonoidalFunctor C D}
           {H : BraidedMonoidalFunctor D E} where

    -- NOTE: Again, manual expansion seems necessary to type check in
    -- reasonable time.

    associator : (H ∘Fˢ G) ∘Fˢ F ≃ H ∘Fˢ (G ∘Fˢ F)
    associator = record
      { U               = AU.U
      ; F⇒G-isMonoidal  = record
        { ε-compat      = AU.ε-compat
        ; ⊗-homo-compat = AU.⊗-homo-compat
        }
      }
      where
        module AU =
          U.MonoidalNaturalIsomorphism (U.associator {F = MF F} {MF G} {MF H})


text:
module Bool where

data Bool : Set where
  true  : Bool
  false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

ext: agda

max_stars_repo_name: mjhopkins/PowerOfPi

max_issues_repo_name: mjhopkins/PowerOfPi

max_forks_repo_name: mjhopkins/PowerOfPi


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module SelectSort  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Data.List
open import Data.Product
open import Data.Sum
open import Size
open import SList
open import SList.Order _≤_

select : {ι : Size} → A →  SList A {ι} → A × SList A {ι}
select x snil = (x , snil)
select x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y
    with select x ys
select x (y ∙ ys) | inj₁ x≤y  | (z , zs) = (z , y ∙ zs)
select x (y ∙ ys) | inj₂ y≤x
    with select y ys
select x (y ∙ ys) | inj₂ y≤x | (z , zs) = (z , x ∙ zs)

selectSort : {ι : Size} → SList A {ι} → SList A {ι}
selectSort snil = snil
selectSort (x ∙ xs)
    with select x xs
... | (y , ys) = y ∙ (selectSort ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Categories.Category.Instance.Monoidals where

open import Level

open import Categories.Category
open import Categories.Category.Helper
open import Categories.Category.Monoidal
open import Categories.Functor.Monoidal
open import Categories.Functor.Monoidal.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism

module _ o ℓ e where

  Monoidals : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
  Monoidals = categoryHelper record
    { Obj       = MonoidalCategory o ℓ e
    ; _⇒_       = MonoidalFunctor
    ; _≈_       = λ F G → M.F F ≃ M.F G
    ; id        = idF-Monoidal _
    ; _∘_       = ∘-Monoidal
    ; assoc     = λ {_ _ _ _ F G H} → associator (M.F F) (M.F G) (M.F H)
    ; identityˡ = unitorˡ
    ; identityʳ = unitorʳ
    ; equiv     = record
      { refl  = ≃.refl
      ; sym   = ≃.sym
      ; trans = ≃.trans
      }
    ; ∘-resp-≈  = _ⓘₕ_
    }
    where module M = MonoidalFunctor

  StrongMonoidals : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
  StrongMonoidals = categoryHelper record
    { Obj       = MonoidalCategory o ℓ e
    ; _⇒_       = StrongMonoidalFunctor
    ; _≈_       = λ F G → M.F F ≃ M.F G
    ; id        = idF-StrongMonoidal _
    ; _∘_       = ∘-StrongMonoidal
    ; assoc     = λ {_ _ _ _ F G H} → associator (M.F F) (M.F G) (M.F H)
    ; identityˡ = unitorˡ
    ; identityʳ = unitorʳ
    ; equiv     = record
      { refl  = ≃.refl
      ; sym   = ≃.sym
      ; trans = ≃.trans
      }
    ; ∘-resp-≈  = _ⓘₕ_
    }
    where module M = StrongMonoidalFunctor

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

module LogicalFramework.Disjunction where

module LF where
  postulate
    _∨_  : Set → Set → Set
    inj₁ : {A B : Set} → A → A ∨ B
    inj₂ : {A B : Set} → B → A ∨ B
    case : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C

  ∨-comm : {A B : Set} → A ∨ B → B ∨ A
  ∨-comm = case inj₂ inj₁

module Inductive where

  open import Common.FOL.FOL

  ∨-comm-el : {A B : Set} → A ∨ B → B ∨ A
  ∨-comm-el = case inj₂ inj₁

  ∨-comm : {A B : Set} → A ∨ B → B ∨ A
  ∨-comm (inj₁ a) = inj₂ a
  ∨-comm (inj₂ b) = inj₁ b

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- A type soundness result
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Lambda.Delay-monad.Type-soundness where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

open import Function-universe equality-with-J
open import Maybe equality-with-J
open import Monad equality-with-J
open import Vec.Function equality-with-J

open import Delay-monad.Always
open import Delay-monad.Bisimilarity
open import Delay-monad.Monad

open import Lambda.Delay-monad.Interpreter
open import Lambda.Syntax

open Closure Tm

-- If we can prove □ ∞ (WF-MV σ) (run x), then x does not "go wrong".

does-not-go-wrong : ∀ {σ} {x : M ∞ Value} →
                    □ ∞ (WF-MV σ) (run x) → ¬ x ≈M fail
does-not-go-wrong (now {x = nothing} ())
does-not-go-wrong (now {x = just x} x-wf) ()
does-not-go-wrong (later x-wf)            (laterˡ x↯) =
  does-not-go-wrong (force x-wf) x↯

-- A "constructor" for □ i ∘ WF-MV.

_>>=-wf_ :
  ∀ {i σ τ} {x : M ∞ Value} {f : Value → M ∞ Value} →
  □ i (WF-MV σ) (run x) →
  (∀ {v} → WF-Value σ v → □ i (WF-MV τ) (run (f v))) →
  □ i (WF-MV τ) (MaybeT.run (x >>= f))
x-wf >>=-wf f-wf =
  □->>= x-wf λ { {nothing} ()
               ; {just v}  v-wf → f-wf v-wf
               }

-- Well-typed programs do not "go wrong".

mutual

  ⟦⟧-wf : ∀ {i n Γ} (t : Tm n) {σ} → Γ ⊢ t ∈ σ →
          ∀ {ρ} → WF-Env Γ ρ →
          □ i (WF-MV σ) (run (⟦ t ⟧ ρ))
  ⟦⟧-wf (con i)   con             ρ-wf = now con
  ⟦⟧-wf (var x)   var             ρ-wf = now (ρ-wf x)
  ⟦⟧-wf (ƛ t)     (ƛ t∈)          ρ-wf = now (ƛ t∈ ρ-wf)
  ⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) {ρ} ρ-wf =
    ⟦⟧-wf t₁ t₁∈ ρ-wf >>=-wf λ f-wf →
    ⟦⟧-wf t₂ t₂∈ ρ-wf >>=-wf λ v-wf →
    ∙-wf f-wf v-wf

  ∙-wf : ∀ {i σ τ f v} →
         WF-Value (σ ⇾ τ) f → WF-Value (force σ) v →
         □ i (WF-MV (force τ)) (run (f ∙ v))
  ∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf =
    later λ { .force → ⟦⟧-wf _ t₁∈ (cons-wf v₂-wf ρ₁-wf) }

type-soundness : ∀ {t : Tm 0} {σ} →
                 nil ⊢ t ∈ σ → ¬ ⟦ t ⟧ nil ≈M fail
type-soundness {t} {σ} =
  nil ⊢ t ∈ σ                      ↝⟨ (λ t∈ → ⟦⟧-wf _ t∈ nil-wf) ⟩
  □ ∞ (WF-MV σ) (run (⟦ t ⟧ nil))  ↝⟨ does-not-go-wrong ⟩□
  ¬ ⟦ t ⟧ nil ≈M fail              □

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module _ where

module Test₁ where
  postulate
    id : {X : Set} → X → X
    A : Set
    x : A

  record S : Set where
    field
      a : A

  postulate
    B : S → Set

  record T : Set where
    field
      s : S
      b : B s

  -- Agda hangs here
  t : T
  t = λ
    { .T.s .S.a → x
    ; .T.b      → id {!!}
    }

module Test₂ where
  postulate
    id : (X : Set) → X → X
    A : Set
    B : A → Set
    x : A

  record T : Set where
    field
      a : A
      b : B a

  -- Agda hangs here
  t : T
  t = λ
    { .T.a → x
    ; .T.b → id {!!} {!!}
    }

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Data.Maybe.Sugar where

open import Prelude
open import Data.Maybe

_>>=_ : Maybe A → (A → Maybe B) → Maybe B
nothing >>= f = nothing
just x >>= f = f x

pure : A → Maybe A
pure = just

_<*>_ : Maybe (A → B) → Maybe A → Maybe B
nothing <*> xs = nothing
just f <*> nothing = nothing
just f <*> just x = just (f x)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Automatic solvers for equations over booleans
------------------------------------------------------------------------

-- See README.Nat for examples of how to use similar solvers

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

module Data.Bool.Solver where

import Algebra.Solver.Ring.Simple as Solver
import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
open import Data.Bool using (_≟_)
open import Data.Bool.Properties

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _∨_ and _∧_

module ∨-∧-Solver =
  Solver (ACR.fromCommutativeSemiring ∨-∧-commutativeSemiring) _≟_

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _xor_ and _∧_

module xor-∧-Solver =
  Solver (ACR.fromCommutativeRing xor-∧-commutativeRing) _≟_


text:
module WithInParModule (A : Set) where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Bool : Set where
  true : Bool
  false : Bool

isZero : Nat -> Bool
isZero zero = true
isZero (suc _) = false

f : Nat -> Nat
f n with isZero n
f n | true = zero
f n | false = suc zero

g : Nat -> Nat
g zero = zero
g (suc n) with g n
g (suc n) | zero  = n
g (suc n) | suc _ = n

data T : Set where
  tt : T

module A (x : T) where
  h : T
  h with x
  h | y = y

postulate
  C : T -> Set

test : C (A.h tt) -> C tt
test x = x

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Issue348 where

import Common.Irrelevance

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

record R : Set1 where
  constructor mkR
  field
    .fromR : Set

reflR : (r : R) -> r == r
reflR r = refl {a = _}
-- issue: unsolved metavars resolved 2010-10-15 by making eta-expansion
-- more lazy (do not eta expand all meta variable listeners, see MetaVars.hs


text:
module Cats.End where

open import Level using (_⊔_)

open import Cats.Category
open import Cats.Category.Wedges using (Wedge ; Wedges)
open import Cats.Profunctor

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  where

  IsEnd : {F : Profunctor C C D} → Wedge F → Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′)
  IsEnd {F} = Wdg.IsTerminal
    where
      module Wdg = Category (Wedges F)

  record End (F : Profunctor C C D) : Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) where
    field
      wedge : Wedge F
      isEnd : IsEnd wedge

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An example of how Algebra.IdempotentCommutativeMonoidSolver can be
-- used
------------------------------------------------------------------------

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

module Algebra.Solver.IdempotentCommutativeMonoid.Example where

open import Relation.Binary.PropositionalEquality using (_≡_)

open import Data.Bool.Base using (_∨_)
open import Data.Bool.Properties using (∨-idempotentCommutativeMonoid)

open import Data.Fin using (zero; suc)
open import Data.Vec using ([]; _∷_)

open import Algebra.Solver.IdempotentCommutativeMonoid
  ∨-idempotentCommutativeMonoid

test : ∀ x y z → (x ∨ y) ∨ (x ∨ z) ≡ (z ∨ y) ∨ x
test a b c = let _∨_ = _⊕_ in
  prove 3 ((x ∨ y) ∨ (x ∨ z)) ((z ∨ y) ∨ x) (a ∷ b ∷ c ∷ [])
  where
  x = var zero
  y = var (suc zero)
  z = var (suc (suc zero))


text:
{-# OPTIONS --allow-unsolved-metas #-}
open import Agda.Builtin.Equality
open import Agda.Builtin.List

postulate
  A : Set
  nilA : A
  consA : A → List A → A
  w/e : {x y : A} → x ≡ y

data D : List A → Set where
  nil  : D []
  cons : (x : A) (xs : List A) → D (x ∷ xs)

foo : ∀ {xs} (d : D xs)
      (let f : D xs → A
           f = λ where nil         → nilA
                       (cons y ys) → consA y ys) →
      f d ≡ nilA
foo nil        = {!!}
foo (cons _ _) = w/e

max_forks_repo_name: shlevy/agda


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

module mwe where

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

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

data ℕ : Set lzero where
  zero-ℕ : ℕ
  succ-ℕ : ℕ → ℕ

add-ℕ : ℕ → ℕ → ℕ
add-ℕ x zero-ℕ = x
add-ℕ x (succ-ℕ y) = succ-ℕ (add-ℕ x y)

{- The following function returns the triangular numbers. In other words,
   test-with n = (1/2) * n * (n+1) -}

test-with-1 : ℕ → ℕ
test-with-1 x with x
test-with-1 zero-ℕ | y = y
test-with-1 (succ-ℕ x) | y = add-ℕ y (test-with-1 x)

{- Now we construct a function with manual with-abstraction, of which the
   definition *looks* the same. But actually we will have
   test-with-2 n = n * (n+1). -}

cases-test-with-2 : ℕ → ℕ → ℕ
cases-test-with-2 zero-ℕ y = y
cases-test-with-2 (succ-ℕ x) y = add-ℕ y (cases-test-with-2 x y)

test-with-2 : ℕ → ℕ
test-with-2 x = cases-test-with-2 x x

{- The following function test-with-3 is again the same as test-with-1. -}

cases-test-with-3 : ℕ → ℕ → ℕ
cases-test-with-3 zero-ℕ y = y
cases-test-with-3 (succ-ℕ x) zero-ℕ = zero-ℕ
cases-test-with-3 (succ-ℕ x) (succ-ℕ y) =
  add-ℕ (succ-ℕ y) (cases-test-with-3 x y)

test-with-3 : ℕ → ℕ
test-with-3 x = cases-test-with-3 x x

-- test-with-1 (succ-ℕ (succ-ℕ (succ-ℕ (succ-ℕ zero-ℕ))))
-- test-with-2 (succ-ℕ (succ-ℕ (succ-ℕ (succ-ℕ zero-ℕ))))
-- test-with-3 (succ-ℕ (succ-ℕ (succ-ℕ (succ-ℕ zero-ℕ))))

-- We do some basic setup, introducing only what we need. All else is removed.

id : {i : Level} {A : Set i} → A → A
id a = a

data empty : Set lzero where

ex-falso : {i : Level} {A : Set i} → empty → A
ex-falso ()

¬ : {i : Level} → Set i → Set i
¬ A = A → empty

data unit : Set lzero where
  star : unit

data coprod {i j : Level} (A : Set i) (B : Set j) : Set (i ⊔ j)  where
  inl : A → coprod A B
  inr : B → coprod A B

is-decidable : {l : Level} (A : Set l) → Set l
is-decidable A = coprod A (¬ A)

data Id {i : Level} {A : Set i} (x : A) : A → Set i where
  refl : Id x x

_∙_ :
  {i : Level} {A : Set i} {x y z : A} → Id x y → Id y z → Id x z
refl ∙ q = q

inv :
  {i : Level} {A : Set i} {x y : A} → Id x y → Id y x
inv refl = refl

ap :
  {i j : Level} {A : Set i} {B : Set j} (f : A → B) {x y : A} (p : Id x y) →
  Id (f x) (f y)
ap f refl = refl

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

-- We introduce the finite types

Fin : ℕ → Set lzero
Fin zero-ℕ = empty
Fin (succ-ℕ k) = coprod (Fin k) unit

Eq-Fin : (k : ℕ) → Fin k → Fin k → Set lzero
Eq-Fin (succ-ℕ k) (inl x) (inl y) = Eq-Fin k x y
Eq-Fin (succ-ℕ k) (inl x) (inr y) = empty
Eq-Fin (succ-ℕ k) (inr x) (inl y) = empty
Eq-Fin (succ-ℕ k) (inr x) (inr y) = unit

eq-Eq-Fin :
  {k : ℕ} {x y : Fin k} → Eq-Fin k x y → Id x y
eq-Eq-Fin {succ-ℕ k} {inl x} {inl y} e = ap inl (eq-Eq-Fin e)
eq-Eq-Fin {succ-ℕ k} {inr star} {inr star} star = refl

is-decidable-Eq-Fin :
  (k : ℕ) (x y : Fin k) → is-decidable (Eq-Fin k x y)
is-decidable-Eq-Fin (succ-ℕ k) (inl x) (inl y) = is-decidable-Eq-Fin k x y
is-decidable-Eq-Fin (succ-ℕ k) (inl x) (inr y) = inr id
is-decidable-Eq-Fin (succ-ℕ k) (inr x) (inl y) = inr id
is-decidable-Eq-Fin (succ-ℕ k) (inr x) (inr y) = inl star

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

-- We now study the successor and predecessor functions on Fin k

zero-Fin : {k : ℕ} → Fin (succ-ℕ k)
zero-Fin {zero-ℕ} = inr star
zero-Fin {succ-ℕ k} = inl zero-Fin

neg-one-Fin : {k : ℕ} → Fin (succ-ℕ k)
neg-one-Fin {k} = inr star

succ-Fin : {k : ℕ} → Fin k → Fin k
succ-Fin {succ-ℕ zero-ℕ} x = x
succ-Fin {succ-ℕ (succ-ℕ k)} (inl (inl x)) = inl (succ-Fin (inl x))
succ-Fin {succ-ℕ (succ-ℕ k)} (inl (inr x)) = neg-one-Fin
succ-Fin {succ-ℕ (succ-ℕ k)} (inr x) = zero-Fin

succ-neg-one-Fin : {k : ℕ} → Id (succ-Fin (neg-one-Fin {k})) zero-Fin
succ-neg-one-Fin {zero-ℕ} = refl
succ-neg-one-Fin {succ-ℕ k} = refl

pred-Fin' : {k : ℕ} → Fin k → Fin k
pred-Fin' {succ-ℕ k} x with (is-decidable-Eq-Fin (succ-ℕ k) x zero-Fin)
pred-Fin' {succ-ℕ zero-ℕ} (inr star) | d = zero-Fin
pred-Fin' {succ-ℕ (succ-ℕ k)} (inl x) | inl e = neg-one-Fin
pred-Fin' {succ-ℕ (succ-ℕ k)} (inl x) | inr f = inl (pred-Fin' {succ-ℕ k} x)
pred-Fin' {succ-ℕ (succ-ℕ k)} (inr x) | inr f = inl neg-one-Fin

succ-pred-Fin' :
  {k : ℕ} (x : Fin k) → Id (succ-Fin (pred-Fin' x)) x
succ-pred-Fin' {succ-ℕ k} x with is-decidable-Eq-Fin (succ-ℕ k) x zero-Fin
succ-pred-Fin' {succ-ℕ zero-ℕ} (inr star) | d = refl
succ-pred-Fin' {succ-ℕ (succ-ℕ k)} (inl x) | inl e =
  succ-neg-one-Fin ∙ inv (eq-Eq-Fin e)
succ-pred-Fin' {succ-ℕ (succ-ℕ zero-ℕ)} (inl (inr star)) | inr f =
  ex-falso (f star)
succ-pred-Fin' {succ-ℕ (succ-ℕ (succ-ℕ k))} (inl (inl x)) | inr f =
  {!!} ∙ ap inl (succ-pred-Fin' {succ-ℕ (succ-ℕ k)} (inl x))
succ-pred-Fin' {succ-ℕ (succ-ℕ (succ-ℕ k))} (inl (inr star)) | inr f = refl
succ-pred-Fin' {succ-ℕ (succ-ℕ k)} (inr star) | inr f = refl

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
-- Andreas, 2012-09-13
-- (The signature on the previous line does not apply to all of the
-- text in this file.)
module RelevanceSubtyping where

-- this naturally type-checks:
one : {A B : Set} → (.A → B) → A → B
one f x = f x

-- Subtyping is no longer supported for irrelevance, so the following
-- code is no longer accepted.

-- -- this type-checks because of subtyping
-- one' : {A B : Set} → (.A → B) → A → B
-- one' f = f

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module Definition.Typed.EqualityRelation where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening using (_∷_⊆_)

-- Generic equality relation used with the logical relation

record EqRelSet : Set₁ where
  constructor eqRel
  field
    ---------------
    -- Relations --
    ---------------

    -- Equality of types
    _⊢_≅_   : Con Term → (A B : Term)   → Set

    -- Equality of terms
    _⊢_≅_∷_ : Con Term → (t u A : Term) → Set

    -- Equality of neutral terms
    _⊢_~_∷_ : Con Term → (t u A : Term) → Set

    ----------------
    -- Properties --
    ----------------

    -- Generic equality compatibility
    ~-to-≅ₜ : ∀ {k l A Γ}
            → Γ ⊢ k ~ l ∷ A
            → Γ ⊢ k ≅ l ∷ A

    -- Judgmental conversion compatibility
    ≅-eq  : ∀ {A B Γ}
          → Γ ⊢ A ≅ B
          → Γ ⊢ A ≡ B
    ≅ₜ-eq : ∀ {t u A Γ}
          → Γ ⊢ t ≅ u ∷ A
          → Γ ⊢ t ≡ u ∷ A

    -- Universe
    ≅-univ : ∀ {A B Γ}
           → Γ ⊢ A ≅ B ∷ U
           → Γ ⊢ A ≅ B

    -- Symmetry
    ≅-sym  : ∀ {A B Γ}   → Γ ⊢ A ≅ B     → Γ ⊢ B ≅ A
    ≅ₜ-sym : ∀ {t u A Γ} → Γ ⊢ t ≅ u ∷ A → Γ ⊢ u ≅ t ∷ A
    ~-sym  : ∀ {k l A Γ} → Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ k ∷ A

    -- Transitivity
    ≅-trans  : ∀ {A B C Γ}   → Γ ⊢ A ≅ B     → Γ ⊢ B ≅ C     → Γ ⊢ A ≅ C
    ≅ₜ-trans : ∀ {t u v A Γ} → Γ ⊢ t ≅ u ∷ A → Γ ⊢ u ≅ v ∷ A → Γ ⊢ t ≅ v ∷ A
    ~-trans  : ∀ {k l m A Γ} → Γ ⊢ k ~ l ∷ A → Γ ⊢ l ~ m ∷ A → Γ ⊢ k ~ m ∷ A

    -- Conversion
    ≅-conv : ∀ {t u A B Γ} → Γ ⊢ t ≅ u ∷ A → Γ ⊢ A ≡ B → Γ ⊢ t ≅ u ∷ B
    ~-conv : ∀ {k l A B Γ} → Γ ⊢ k ~ l ∷ A → Γ ⊢ A ≡ B → Γ ⊢ k ~ l ∷ B

    -- Weakening
    ≅-wk  : ∀ {A B ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ A ≅ B
          → Δ ⊢ wk ρ A ≅ wk ρ B
    ≅ₜ-wk : ∀ {t u A ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ t ≅ u ∷ A
          → Δ ⊢ wk ρ t ≅ wk ρ u ∷ wk ρ A
    ~-wk  : ∀ {k l A ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ k ~ l ∷ A
          → Δ ⊢ wk ρ k ~ wk ρ l ∷ wk ρ A

    -- Weak head expansion
    ≅-red : ∀ {A A′ B B′ Γ}
          → Γ ⊢ A ⇒* A′
          → Γ ⊢ B ⇒* B′
          → Whnf A′
          → Whnf B′
          → Γ ⊢ A′ ≅ B′
          → Γ ⊢ A  ≅ B

    ≅ₜ-red : ∀ {a a′ b b′ A B Γ}
           → Γ ⊢ A ⇒* B
           → Γ ⊢ a ⇒* a′ ∷ B
           → Γ ⊢ b ⇒* b′ ∷ B
           → Whnf B
           → Whnf a′
           → Whnf b′
           → Γ ⊢ a′ ≅ b′ ∷ B
           → Γ ⊢ a  ≅ b  ∷ A

    -- Universe type reflexivity
    ≅-Urefl   : ∀ {Γ} → ⊢ Γ → Γ ⊢ U ≅ U

    -- Natural number type reflexivity
    ≅-ℕrefl   : ∀ {Γ} → ⊢ Γ → Γ ⊢ ℕ ≅ ℕ
    ≅ₜ-ℕrefl  : ∀ {Γ} → ⊢ Γ → Γ ⊢ ℕ ≅ ℕ ∷ U

    -- Π-congurence

    ≅-Π-cong  : ∀ {F G H E Γ}
              → Γ ⊢ F
              → Γ ⊢ F ≅ H
              → Γ ∙ F ⊢ G ≅ E
              → Γ ⊢ Π F ▹ G ≅ Π H ▹ E

    ≅ₜ-Π-cong : ∀ {F G H E Γ}
              → Γ ⊢ F
              → Γ ⊢ F ≅ H ∷ U
              → Γ ∙ F ⊢ G ≅ E ∷ U
              → Γ ⊢ Π F ▹ G ≅ Π H ▹ E ∷ U

    -- Zero reflexivity
    ≅ₜ-zerorefl : ∀ {Γ} → ⊢ Γ → Γ ⊢ zero ≅ zero ∷ ℕ

    -- Successor congurence
    ≅-suc-cong : ∀ {m n Γ} → Γ ⊢ m ≅ n ∷ ℕ → Γ ⊢ suc m ≅ suc n ∷ ℕ

    -- η-equality
    ≅-η-eq : ∀ {f g F G Γ}
              → Γ ⊢ F
              → Γ ⊢ f ∷ Π F ▹ G
              → Γ ⊢ g ∷ Π F ▹ G
              → Function f
              → Function g
              → Γ ∙ F ⊢ wk1 f ∘ var 0 ≅ wk1 g ∘ var 0 ∷ G
              → Γ ⊢ f ≅ g ∷ Π F ▹ G

    -- Variable reflexivity
    ~-var : ∀ {x A Γ} → Γ ⊢ var x ∷ A → Γ ⊢ var x ~ var x ∷ A

    -- Application congurence
    ~-app : ∀ {a b f g F G Γ}
          → Γ ⊢ f ~ g ∷ Π F ▹ G
          → Γ ⊢ a ≅ b ∷ F
          → Γ ⊢ f ∘ a ~ g ∘ b ∷ G [ a ]

    -- Natural recursion congurence
    ~-natrec : ∀ {z z′ s s′ n n′ F F′ Γ}
             → Γ ∙ ℕ ⊢ F ≅ F′
             → Γ     ⊢ z ≅ z′ ∷ F [ zero ]
             → Γ     ⊢ s ≅ s′ ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
             → Γ     ⊢ n ~ n′ ∷ ℕ
             → Γ     ⊢ natrec F z s n ~ natrec F′ z′ s′ n′ ∷ F [ n ]

  -- Composition of universe and generic equality compatibility
  ~-to-≅ : ∀ {k l Γ} → Γ ⊢ k ~ l ∷ U → Γ ⊢ k ≅ l
  ~-to-≅ k~l = ≅-univ (~-to-≅ₜ k~l)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Agda.Builtin.FromNeg where

open import Agda.Primitive
open import Agda.Builtin.Nat

record Negative {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : Nat → Set a
    fromNeg : ∀ n → {{_ : Constraint n}} → A

open Negative {{...}} public using (fromNeg)

{-# BUILTIN FROMNEG fromNeg #-}
{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-}


text:
module Sets.PredicateSet.Listable where

import      Lvl
open import Data.List as List using (List)
open import Data.List.Functions renaming (_++_ to _∪ₗ_) using (singleton)
open import Data.List.Relation.Membership renaming (_∈_ to _∈ₗ_ ; _∈!_ to _∈!ₗ_) using (use ; skip)
open import Data.List.Relation.Permutation
open import Data.List.Relation.Quantification using (∀ₗᵢₛₜ ; module AllElements ; ExistsElement ; ExistsElementEquivalence ; module ExistsElementEquivalence)
open import Functional
open import Lang.Instance
open import Logic.Propositional
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet ; _∈_ ; ∅ ; _∪_ ; •_)
open        Sets.PredicateSet.BoundedQuantifiers
open import Type.Properties.Singleton
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T : Type{ℓ}
private variable S S₁ S₂ : PredSet{ℓ}(T)
private variable x : T

module _ (S : PredSet{ℓ}(T)) where
  record Listable : Type{Lvl.of(T) Lvl.⊔ ℓ} where
    field
      list : List(T)
      unique : ∀ₛ(S) (_∈!ₗ list)
      restrict : ∀ₗᵢₛₜ(list)  (_∈ S)

    proof : ∀ₛ(S) (_∈ₗ list)
    proof = IsUnit.unit ∘ unique
  list = inst-fn Listable.list

private variable l l₁ l₂ l₁₂ : Listable(S)

∅-listable : Listable{ℓ = ℓ}{T = T}(∅)
Listable.list     ∅-listable = List.∅
Listable.unique   ∅-listable ()
Listable.restrict ∅-listable = AllElements.∅

singleton-listable : Listable(•_ ⦃ [≡]-equiv ⦄ x)
Listable.list     singleton-listable           = singleton _
Listable.unique   singleton-listable [≡]-intro = intro (use [≡]-intro) (\{ {ExistsElement.• x} → ExistsElementEquivalence.use})
Listable.restrict singleton-listable           = [≡]-intro AllElements.⊰ AllElements.∅

{- TODO: Will not satisfy Listable because (_++_) may yield multiples which Listable does not allow, and therefore list-[∪] below is also incorrect.
∪-listable : ⦃ Listable(S₁) ⦄ → ⦃ Listable(S₂) ⦄ → Listable(S₁ ∪ S₂)
Listable.list (∪-listable {S₁ = S₁} {S₂ = S₂}) = list(S₁) ∪ₗ list(S₂)
Listable.unique   ∪-listable = {!!}
Listable.restrict ∪-listable = {!!}-}

-- list-[∪] : ∀{Γ₁ : PredSet{ℓ₁}(Formula(P))}{Γ₂ : PredSet{ℓ₂}(Formula(P))}{l₁₂ : Listable(Γ₁ PredSet.∪ Γ₂)} → Logic.∃{Obj = Listable(Γ₁) ⨯ Listable(Γ₂)}(\(l₁ , l₂) → (list(Γ₁ PredSet.∪ Γ₂) ⦃ l₁₂ ⦄ ≡ (list Γ₁ ⦃ l₁ ⦄) ∪ (list Γ₂ ⦃ l₂ ⦄)))
postulate list-[∪] : (list(S₁ ∪ S₂) ⦃ l₁₂ ⦄ permutes (list S₁ ⦃ l₁ ⦄) ∪ₗ (list S₂ ⦃ l₂ ⦄))
postulate list-[∪·] : (list(S ∪ (•_ ⦃ [≡]-equiv ⦄ x)) ⦃ l₁₂ ⦄ permutes (list S ⦃ l ⦄) ∪ₗ singleton(x))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module SAcc where

data Size : Set where
  s : Size -> Size

data Acc ( A : Set ) ( Lt : A -> A -> Set) : Size -> A -> Set where
  acc :   (i : Size) ->  ( b : A )
        -> ( ( a : A ) -> Lt a b  ->  Acc A Lt i a )
        -> ( Acc A Lt (s i) b )

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

data Lt : Nat -> Nat -> Set where
  ltzero : ( x : Nat ) -> Lt zero (succ x)
  ltsucc : ( x : Nat ) -> (y : Nat) -> Lt x y -> Lt (succ x) (succ y)

notLt0 : ( x : Nat ) -> Lt x zero -> (C : Set) -> C
notLt0 x ()

accLt : (i : Size ) -> ( x : Nat ) -> Acc Nat Lt i x
accLt (s i) zero = acc i zero (\a -> \p -> notLt0 a p (Acc Nat Lt i a) )
accLt (s i) (succ x) = acc i (succ x) (\a -> \p -> (accLt i a))

max_stars_repo_name: andreasabel/miniagda

max_issues_repo_name: andreasabel/miniagda

max_forks_repo_name: andreasabel/miniagda


text:
module _ where

open import Agda.Primitive

postulate
  Equiv : ∀ {a b} → (A : Set a) (B : Set b) → Set (a ⊔ b)

{-# BUILTIN EQUIV Equiv #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Oscar.Relation where

open import Oscar.Level

_⟨_⟩→_ : ∀ {a} {A : Set a} {b} → A → (A → Set b) → A → Set b
m ⟨ B ⟩→ n = B m → B n

Transitive : ∀ {a} {A : Set a} {b} (B : A → A → Set b) → Set (a ⊔ b)
Transitive B = ∀ {y z} → B y z → ∀ {x} → B x y → B x z

module _ {𝔬} {⋆ : Set 𝔬} {𝔪} {_↦_ : ⋆ → ⋆ → Set 𝔪} (_∙_ : Transitive _↦_) {𝔮} (_≞_ : ∀ {x} {y} → x ↦ y → x ↦ y → Set 𝔮) where

  Extensional : Set (𝔬 ⊔ 𝔪 ⊔ 𝔮)
  Extensional =
    ∀ {x y} {f₁ f₂ : x ↦ y}
    → f₁ ≞ f₂ → ∀ {z} {g₁ g₂ : y ↦ z}
    → g₁ ≞ g₂
    → (g₁ ∙ f₁) ≞ (g₂ ∙ f₂)

  Associative : Set (𝔬 ⊔ 𝔪 ⊔ 𝔮)
  Associative =
    ∀ {w x}
      (f : w ↦ x)
    {y}
      (g : x ↦ y)
    {z}
      (h : y ↦ z)
    → ((h ∙ g) ∙ f) ≞ (h ∙ (g ∙ f))


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

module Data.Bits.Equatable where

open import Data.Bits
open import Prelude

_≡ᴮ_ : Bits → Bits → Bool
[]      ≡ᴮ []      = true
(0∷ xs) ≡ᴮ (0∷ ys) = xs ≡ᴮ ys
(1∷ xs) ≡ᴮ (1∷ ys) = xs ≡ᴮ ys
_       ≡ᴮ _       = false

open import Relation.Nullary.Discrete.FromBoolean

sound-== : ∀ n m →  T (n ≡ᴮ m) → n ≡ m
sound-== [] [] p i = []
sound-== (0∷ n) (0∷ m) p i = 0∷ sound-== n m p i
sound-== (1∷ n) (1∷ m) p i = 1∷ sound-== n m p i

complete-== : ∀ n → T (n ≡ᴮ n)
complete-== [] = tt
complete-== (0∷ n) = complete-== n
complete-== (1∷ n) = complete-== n

_≟_ : Discrete Bits
_≟_ = from-bool-eq _≡ᴮ_ sound-== complete-==

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import lib.Basics
open import lib.types.Bool
open import lib.types.Empty
open import lib.types.Lift
open import lib.types.Pointed

module lib.types.Coproduct where

module _ {i j} {A : Type i} {B : Type j} where

  ⊔-code : Coprod A B → Coprod A B → Type (lmax i j)
  ⊔-code (inl a₁) (inl a₂) = Lift {j = (lmax i j)} $ a₁ == a₂
  ⊔-code (inl a₁) (inr b₂) = Lift Empty
  ⊔-code (inr b₁) (inl a₂) = Lift Empty
  ⊔-code (inr b₁) (inr b₂) = Lift {j = (lmax i j)} $ b₁ == b₂

  ⊔-encode : {x y : Coprod A B} → (x == y) → ⊔-code x y
  ⊔-encode {inl a₁} {y} p = transport (⊔-code $ inl a₁) p (lift $ idp {a = a₁})
  ⊔-encode {inr b₁} {y} p = transport (⊔-code $ inr b₁) p (lift $ idp {a = b₁})

  ⊔-decode : {x y : Coprod A B} → ⊔-code x y → (x == y)
  ⊔-decode {inl _} {inl _} c = ap inl $ lower c
  ⊔-decode {inl _} {inr _} c = Empty-rec $ lower c
  ⊔-decode {inr _} {inl _} c = Empty-rec $ lower c
  ⊔-decode {inr _} {inr _} c = ap inr (lower c)

  ⊔-code-equiv : (x y : Coprod A B) → (x == y) ≃ ⊔-code x y
  ⊔-code-equiv x y = equiv ⊔-encode ⊔-decode (f-g x y) (g-f x y)
    where f-g : ∀ x' y' → ∀ c → ⊔-encode (⊔-decode {x'} {y'} c) == c
          f-g (inl a₁) (inl .a₁) (lift idp) = idp
          f-g (inl a₁) (inr b₂) b = Empty-rec $ lower b
          f-g (inr b₁) (inl a₂) b = Empty-rec $ lower b
          f-g (inr b₁) (inr .b₁) (lift idp) = idp

          g-f : ∀ x' y' → ∀ p → ⊔-decode (⊔-encode {x'} {y'} p) == p
          g-f (inl _) .(inl _) idp = idp
          g-f (inr _) .(inr _) idp = idp

  inl=inl-equiv : (a₁ a₂ : A) → (inl a₁ == inl a₂) ≃ (a₁ == a₂)
  inl=inl-equiv a₁ a₂ = lower-equiv ∘e ⊔-code-equiv (inl a₁) (inl a₂)

  inr=inr-equiv : (b₁ b₂ : B) → (inr b₁ == inr b₂) ≃ (b₁ == b₂)
  inr=inr-equiv b₁ b₂ = lower-equiv ∘e ⊔-code-equiv (inr b₁) (inr b₂)

  inl≠inr : (a₁ : A) (b₂ : B) → (inl a₁ ≠ inr b₂)
  inl≠inr a₁ b₂ p = lower $ ⊔-encode p

  inr≠inl : (b₁ : B) (a₂ : A) → (inr b₁ ≠ inl a₂)
  inr≠inl a₁ b₂ p = lower $ ⊔-encode p

  ⊔-level : ∀ {n} → has-level (S (S n)) A → has-level (S (S n)) B
            → has-level (S (S n)) (Coprod A B)
  ⊔-level pA _ (inl a₁) (inl a₂) =
    equiv-preserves-level ((inl=inl-equiv a₁ a₂)⁻¹) (pA a₁ a₂)
  ⊔-level _ _ (inl a₁) (inr b₂) = λ p → Empty-rec (inl≠inr a₁ b₂ p)
  ⊔-level _ _ (inr b₁) (inl a₂) = λ p → Empty-rec (inr≠inl b₁ a₂ p)
  ⊔-level _ pB (inr b₁) (inr b₂) =
    equiv-preserves-level ((inr=inr-equiv b₁ b₂)⁻¹) (pB b₁ b₂)

infix 80 _⊙⊔_
_⊙⊔_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
X ⊙⊔ Y = ⊙[ Coprod (fst X) (fst Y) , inl (snd X) ]

_⊔⊙_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
X ⊔⊙ Y = ⊙[ Coprod (fst X) (fst Y) , inr (snd Y) ]

codiag : ∀ {i} {A : Type i} → A ⊔ A → A
codiag (inl a) = a
codiag (inr a) = a

⊙codiag : ∀ {i} {X : Ptd i} → fst (X ⊙⊔ X ⊙→ X)
⊙codiag = (codiag , idp)

-- A binary sigma is a coproduct
ΣBool-equiv-⊔ : ∀ {i} (Pick : Bool → Type i)
  → Σ _ Pick ≃ (Pick true ⊔ Pick false)
ΣBool-equiv-⊔ Pick = equiv into out into-out out-into
  where
  into : Σ _ Pick → Pick true ⊔ Pick false
  into (true , a) = inl a
  into (false , b) = inr b

  out : (Pick true ⊔ Pick false) → Σ _ Pick
  out (inl a) = (true , a)
  out (inr b) = (false , b)

  into-out : ∀ c → into (out c) == c
  into-out (inl a) = idp
  into-out (inr b) = idp

  out-into : ∀ s → out (into s) == s
  out-into (true , a) = idp
  out-into (false , b) = idp

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

module Agda.Builtin.Equality.Rewrite where

open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a non-strict order to incorporate a new supremum
------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Supremum

open import Relation.Binary

module Relation.Binary.Construct.Add.Supremum.NonStrict
  {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where

open import Level using (_⊔_)
open import Data.Sum as Sum
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
import Relation.Binary.PropositionalEquality as P
open import Relation.Nullary.Construct.Add.Supremum
import Relation.Binary.Construct.Add.Supremum.Equality as Equality

------------------------------------------------------------------------
-- Definition

data _≤⁺_ : Rel (A ⁺) (a ⊔ ℓ) where
  [_]  : {k l : A} → k ≤ l → [ k ] ≤⁺ [ l ]
  _≤⊤⁺ : (k : A ⁺)         → k     ≤⁺ ⊤⁺

------------------------------------------------------------------------
-- Properties

[≤]-injective : ∀ {k l} → [ k ] ≤⁺ [ l ] → k ≤ l
[≤]-injective [ p ] = p

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  ≤⁺-reflexive : (_≈_ ⇒ _≤_) → (_≈⁺_ ⇒ _≤⁺_)
  ≤⁺-reflexive ≤-reflexive [ p ] = [ ≤-reflexive p ]
  ≤⁺-reflexive ≤-reflexive ⊤⁺≈⊤⁺ = ⊤⁺ ≤⊤⁺

  ≤⁺-antisym : Antisymmetric _≈_ _≤_ → Antisymmetric _≈⁺_ _≤⁺_
  ≤⁺-antisym ≤-antisym [ p ]    [ q ]    = [ ≤-antisym p q ]
  ≤⁺-antisym ≤-antisym (⊤⁺ ≤⊤⁺) (⊤⁺ ≤⊤⁺) = ⊤⁺≈⊤⁺

≤⁺-trans : Transitive _≤_ → Transitive _≤⁺_
≤⁺-trans ≤-trans [ p ] [ q ]   = [ ≤-trans p q ]
≤⁺-trans ≤-trans p     (l ≤⊤⁺) = _ ≤⊤⁺

≤⁺-maximum : Maximum _≤⁺_ ⊤⁺
≤⁺-maximum = _≤⊤⁺

≤⁺-dec : Decidable _≤_ → Decidable _≤⁺_
≤⁺-dec _≤?_ k     ⊤⁺    = yes (k ≤⊤⁺)
≤⁺-dec _≤?_ ⊤⁺    [ l ] = no (λ ())
≤⁺-dec _≤?_ [ k ] [ l ] = Dec.map′ [_] [≤]-injective (k ≤? l)

≤⁺-total : Total _≤_ → Total _≤⁺_
≤⁺-total ≤-total k     ⊤⁺    = inj₁ (k ≤⊤⁺)
≤⁺-total ≤-total ⊤⁺    l     = inj₂ (l ≤⊤⁺)
≤⁺-total ≤-total [ k ] [ l ] = Sum.map [_] [_] (≤-total k l)

≤⁺-irrelevant : Irrelevant _≤_ → Irrelevant _≤⁺_
≤⁺-irrelevant ≤-irr [ p ]   [ q ]    = P.cong _ (≤-irr p q)
≤⁺-irrelevant ≤-irr (k ≤⊤⁺) (k ≤⊤⁺) = P.refl

------------------------------------------------------------------------
-- Structures

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  ≤⁺-isPreorder : IsPreorder _≈_ _≤_ → IsPreorder _≈⁺_ _≤⁺_
  ≤⁺-isPreorder ≤-isPreorder = record
    { isEquivalence = ≈⁺-isEquivalence isEquivalence
    ; reflexive     = ≤⁺-reflexive reflexive
    ; trans         = ≤⁺-trans trans
    } where open IsPreorder ≤-isPreorder

  ≤⁺-isPartialOrder : IsPartialOrder _≈_ _≤_ → IsPartialOrder _≈⁺_ _≤⁺_
  ≤⁺-isPartialOrder ≤-isPartialOrder = record
    { isPreorder = ≤⁺-isPreorder isPreorder
    ; antisym    = ≤⁺-antisym antisym
    } where open IsPartialOrder ≤-isPartialOrder

  ≤⁺-isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecPartialOrder _≈⁺_ _≤⁺_
  ≤⁺-isDecPartialOrder ≤-isDecPartialOrder = record
    { isPartialOrder = ≤⁺-isPartialOrder isPartialOrder
    ; _≟_            = ≈⁺-dec _≟_
    ; _≤?_           = ≤⁺-dec _≤?_
    } where open IsDecPartialOrder ≤-isDecPartialOrder

  ≤⁺-isTotalOrder : IsTotalOrder _≈_ _≤_ → IsTotalOrder _≈⁺_ _≤⁺_
  ≤⁺-isTotalOrder ≤-isTotalOrder = record
    { isPartialOrder = ≤⁺-isPartialOrder isPartialOrder
    ; total          = ≤⁺-total total
    } where open IsTotalOrder ≤-isTotalOrder

  ≤⁺-isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ → IsDecTotalOrder _≈⁺_ _≤⁺_
  ≤⁺-isDecTotalOrder ≤-isDecTotalOrder = record
    { isTotalOrder = ≤⁺-isTotalOrder isTotalOrder
    ; _≟_          = ≈⁺-dec _≟_
    ; _≤?_         = ≤⁺-dec _≤?_
    } where open IsDecTotalOrder ≤-isDecTotalOrder


text:
-- (Γ ⇒ Δ ∪ · A) → (Γ ⇒ Δ ∪ · (A ∨ B))
-- The conclusion (A ∨ B) is the principal/major formula of the rule.
-- The premiss A is the active/minor formula of the rule
-- Γ, Δ is the side formulas of the rule.

-- Γ ⇒ Δ
-- LHS Γ is the antecedent of the sequent.
-- RHS Γ is the consequent of the sequent.


text:
{-# OPTIONS  --sized-types --show-implicit #-}

module SizedNatAnnotated where

open import Size

data Nat : {i : Size} -> Set where
  zero : {i : Size} -> Nat {↑ i}
  suc  : {i : Size} -> Nat {i} -> Nat {↑ i}

-- subtraction is non size increasing
sub : {i : Size} -> Nat {i} -> Nat {∞} -> Nat {i}
sub .{↑ i} (zero {i})  n       = zero {i}
sub .{↑ i} (suc {i} m) zero    = suc {i} m
sub .{↑ i} (suc {i} m) (suc n) = sub {i} m n

-- div' m n  computes  ceiling(m/(n+1))
div' : {i : Size} -> Nat {i} -> Nat -> Nat {i}
div' .{↑ i} (zero {i})  n = zero {i}
div' .{↑ i} (suc {i} m) n = suc  {i} (div' {i} (sub {i} m n) n)


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

module univ where

open import Base
open import Nat

import Logic.ChainReasoning
module Chain
  {A : Set}( _==_ : A -> A -> Set)
  (refl : {x : A} -> x == x)
  (trans : {x y z : A} -> x == y -> y == z -> x == z) =
  Logic.ChainReasoning.Mono.Homogenous _==_ (\x -> refl) (\x y z -> trans)

-- mutual inductive recursive definition of S and the functions _=S_, El, eq,
-- and all the proofs on these functions

mutual

  infix 40 _==_ _=S_ _=Fam_
  infixr 80 _<<_
  infixl 80 _>>_
  infixl 150 _!_

  data S : Set where
    nat   : S
    pi    : (A : S)(F : Fam A) -> S
    sigma : (A : S)(F : Fam A) -> S

  data Fam (A : S) : Set where
    fam : (F : El A -> S) -> Map _==_ _=S_ F -> Fam A

  _=S'_ : rel S
  nat       =S' pi _ _    = False
  nat       =S' sigma _ _ = False
  pi _ _    =S' nat       = False
  pi _ _    =S' sigma _ _ = False
  sigma _ _ =S' nat       = False
  sigma _ _ =S' pi _ _    = False
  nat       =S' nat       = True
  pi A F =S' pi B G =
      (B =S A) * \ B=A -> F =Fam G >> B=A
  sigma A F =S' sigma B G =
      (A =S B) * \A=B -> F >> A=B =Fam G

  data _=S_ (A B : S) : Set where
    eqS : A =S' B -> A =S B

  El' : S -> Set
  El' nat = Nat
  El' (pi A F) =
    ((x : El A) -> El (F ! x)) * \f ->
    {x y : El A}(x=y : x == y) -> f x == pFam F x=y << f y
  El' (sigma A F) =
    El A * \x -> El (F ! x)

  data El (A : S) : Set where
    el : El' A -> El A

  _=='_ : {A : S} -> rel (El A)
  _=='_ {nat} (el x) (el y) = x =N y
  _=='_ {pi A F} (el < f , pf >) (el < g , pg >) =
        (x : El A) -> f x == g x
  _=='_ {sigma A F} (el < x , Fx >) (el < y , Fy >) =
        x == y * \x=y -> Fx == pFam F x=y << Fy

  data _==_ {A : S}(x y : El A) : Set where
    eq : x ==' y -> x == y

  _=Fam_ : {A : S} -> rel (Fam A)
  F =Fam G = (x : El _) -> F ! x =S G ! x

  _!_ : {A : S} -> Fam A -> El A -> S
  fam F _ ! x = F x

  pFam : {A : S}(F : Fam A) -> Map _==_ _=S_ (_!_ F)
  pFam (fam F pF) = pF

  -- Families are contravariant so they cast in the other direction.
  _>>_ : {A B : S} -> Fam A -> A =S B -> Fam B
  _>>_ {A}{B} F A=B = fam G pG
    where
      G : El B -> S
      G x = F ! (A=B << x)

      pG : Map _==_ _=S_ G
      pG x=y = pFam F (p<< A=B x=y)

  pfiFam : {A B : S}(p q : A =S B)(F : Fam A) -> F >> p =Fam F >> q
  pfiFam p q F x = pFam F (pfi p q x)

  _<<_ : {A B : S} -> A =S B -> El B -> El A
  _<<_ {nat       }{pi _ _    } (eqS ()) _
  _<<_ {nat       }{sigma _ _ } (eqS ()) _
  _<<_ {pi _ _    }{nat       } (eqS ()) _
  _<<_ {pi _ _    }{sigma _ _ } (eqS ()) _
  _<<_ {sigma _ _ }{nat       } (eqS ()) _
  _<<_ {sigma _ _ }{pi _ _    } (eqS ()) _
  _<<_ {nat       }{nat       } p x = x
  _<<_ {pi A F    }{pi B G    } (eqS < B=A , F=G >) (el < g , pg >) =
    el < f , (\{x}{y} -> pf x y) >
    where
      f : (x : El A) -> El (F ! x)
      f x = F=G x << g (B=A << x)

      pf : (x y : El A)(x=y : x == y) -> f x == pFam F x=y << f y
      pf x y x=y =
        chain> F=G x << g (B=A << x)
           === F=G x << _      << g (B=A << y)     by p<< _ (pg (p<< B=A x=y))
           === pFam F x=y << F=G y << g (B=A << y) by pfi2 _ _ _ _ _
        where
          open module C = Chain _==_ (ref {_}) (trans {_})
  _<<_ {sigma A F}{sigma B G} (eqS < A=B , F=G >) (el < y , Gy >) =
    el < A=B << y , F=G y << Gy >

  p<< : {A B : S}(A=B : A =S B) -> Map _==_ _==_ (_<<_ A=B)
  p<< {nat}{nat} _ x=y = x=y
  p<< {pi A F} {pi B G} (eqS < B=A , F=G >)
        {el < f , pf >} {el < g , pg >} (eq f=g) = eq cf=cg
    where
      cf=cg : (x : El A) -> F=G x << f (B=A << x) == F=G x << g (B=A << x)
      cf=cg x = p<< (F=G x) (f=g (B=A << x))

  p<< {sigma A F}{sigma B G}(eqS < A=B , F=G >)
      {el < x , Gx >}{el < y , Gy >} (eq < x=y , Gx=Gy >) =
      eq < cx=cy , cGx=cGy >
    where
      cx=cy : A=B << x == A=B << y
      cx=cy = p<< A=B x=y

      cGx=cGy : F=G x << Gx == pFam F cx=cy << F=G y << Gy
      cGx=cGy =
        chain> F=G x        << Gx
           === F=G x        << pFam G x=y << Gy  by p<< (F=G x) Gx=Gy
           === pFam F cx=cy << F=G y      << Gy  by pfi2 _ _ _ _ Gy
        where
          open module C = Chain _==_ (ref {_}) (trans {_})

  p<< {nat        }{pi _ _   } (eqS ()) _
  p<< {nat        }{sigma _ _} (eqS ()) _
  p<< {pi _ _   }{nat        } (eqS ()) _
  p<< {pi _ _   }{sigma _ _} (eqS ()) _
  p<< {sigma _ _}{nat        } (eqS ()) _
  p<< {sigma _ _}{pi _ _   } (eqS ()) _

  refS : Refl _=S_
  refS {nat}       = eqS T
  refS {pi A F}    = eqS < refS , (\x -> symS (pFam F (ref<< x))) >
  refS {sigma A F} = eqS < refS , (\x -> pFam F (ref<< x)) >

  transS : Trans _=S_
  transS {nat       }{nat       }{pi _ _    } _ (eqS ())
  transS {nat       }{nat       }{sigma _ _ } _ (eqS ())
  transS {nat       }{pi _ _    }               (eqS ()) _
  transS {nat       }{sigma _ _ }               (eqS ()) _
  transS {pi _ _    }{nat       }               (eqS ()) _
  transS {pi _ _    }{pi _ _    }{nat       } _ (eqS ())
  transS {pi _ _    }{pi _ _    }{sigma _ _ } _ (eqS ())
  transS {pi _ _    }{sigma _ _ }               (eqS ()) _
  transS {sigma _ _ }{nat       }               (eqS ()) _
  transS {sigma _ _ }{pi _ _    }               (eqS ()) _
  transS {sigma _ _ }{sigma _ _ }{nat       } _ (eqS ())
  transS {sigma _ _ }{sigma _ _ }{pi _ _    } _ (eqS ())
  transS {nat}{nat}{nat} p q = p
  transS {pi A F}{pi B G}{pi C H}
         (eqS < B=A , F=G >) (eqS < C=B , G=H >) = eqS < C=A , F=H >
    where
      open module C = Chain _=S_ refS transS
      C=A = transS C=B B=A
      F=H : F =Fam H >> C=A
      F=H x =
        chain> F ! x
           === G ! (B=A << x)           by F=G x
           === H ! (C=B << B=A << x)    by G=H (B=A << x)
           === H ! (C=A << x)           by pFam H (sym (trans<< C=B B=A x))
  transS {sigma A F}{sigma B G}{sigma C H}
         (eqS < A=B , F=G >)(eqS < B=C , G=H >) = eqS < A=C , F=H >
    where
      open module C = Chain _=S_ refS transS
      A=C = transS A=B B=C
      F=H : F >> A=C =Fam H
      F=H x =
        chain> F ! (A=C << x)
           === F ! (A=B << B=C << x) by pFam F (trans<< A=B B=C x)
           === G ! (B=C << x)        by F=G (B=C << x)
           === H ! x                 by G=H x

  symS : Sym _=S_
  symS {nat       }{pi _ _    } (eqS ())
  symS {nat       }{sigma _ _ } (eqS ())
  symS {pi _ _    }{nat       } (eqS ())
  symS {pi _ _    }{sigma _ _ } (eqS ())
  symS {sigma _ _ }{nat       } (eqS ())
  symS {sigma _ _ }{pi _ _    } (eqS ())
  symS {nat}{nat} p                 = p
  symS {pi A F}{pi B G} (eqS < B=A , F=G >) = eqS < A=B , G=F >
    where
      open module C = Chain _=S_ refS transS
      A=B = symS B=A
      G=F : G =Fam F >> A=B
      G=F x = symS (
        chain> F ! (A=B << x)
           === G ! (B=A << A=B << x) by F=G (A=B << x)
           === G ! (refS << x)       by pFam G (casttrans B=A A=B refS x)
           === G ! x                 by pFam G (ref<< x)
        )
  symS {sigma A F}{sigma B G}(eqS < A=B , F=G >) = eqS < B=A , G=F >
    where
      open module C = Chain _=S_ refS transS
      B=A = symS A=B
      G=F : G >> B=A =Fam F
      G=F x =
        chain> G ! (B=A << x)
           === F ! (A=B << B=A << x) by symS (F=G _)
           === F ! (refS << x)       by pFam F (casttrans _ _ _ x)
           === F ! x                 by pFam F (castref _ x)

  pfi : {A B : S}(p q : A =S B)(x : El B) -> p << x == q << x
  pfi {nat       }{pi _ _    } (eqS ()) _ _
  pfi {nat       }{sigma _ _ } (eqS ()) _ _
  pfi {pi _ _    }{nat       } (eqS ()) _ _
  pfi {pi _ _    }{sigma _ _ } (eqS ()) _ _
  pfi {sigma _ _ }{nat       } (eqS ()) _ _
  pfi {sigma _ _ }{pi _ _    } (eqS ()) _ _
  pfi {nat}{nat} _ _ x = ref
  pfi {pi A F}{pi B G} (eqS < B=A1 , F=G1 >) (eqS < B=A2 , F=G2 >)
      (el < g , pg >) = eq g1=g2
    where
      g1=g2 : (x : El A) -> F=G1 x << g (B=A1 << x)
                         == F=G2 x << g (B=A2 << x)
      g1=g2 x =
        chain> F=G1 x      << g (B=A1 << x)
           === F=G1 x << _ << g (B=A2 << x) by p<< _ (pg (pfi B=A1 B=A2 x))
           === F=G2 x      << g (B=A2 << x) by casttrans _ _ _ _
        where
          open module C = Chain _==_ (ref {_}) (trans {_})
  pfi {sigma A F}{sigma B G} (eqS < A=B1 , F=G1 >) (eqS < A=B2 , F=G2 >)
      (el < y , Gy >) = eq < x1=x2 , Fx1=Fx2 >
    where
      x1=x2 : A=B1 << y == A=B2 << y
      x1=x2 = pfi A=B1 A=B2 y

      Fx1=Fx2 : F=G1 y << Gy == pFam F x1=x2 << F=G2 y << Gy
      Fx1=Fx2 = sym (casttrans _ _ _ _)

  ref<< : {A : S}(x : El A) -> refS << x == x
  ref<< {nat}       x = ref
  ref<< {sigma A F} (el < x , Fx >) = eq < ref<< x , pfi _ _ Fx >
  ref<< {pi A F   } (el < f , pf >) = eq rf=f
    where
      rf=f : (x : El A) -> _ << f (refS << x) == f x
      rf=f x =
        chain> _ << f (refS << x)
           === _ << pFam F (ref<< x) << f x by p<< _ (pf (ref<< x))
           === _ << f x                     by sym (trans<< _ _ (f x))
           === f x                          by castref _ _
        where open module C = Chain _==_ (ref {_}) (trans {_})

  trans<< : {A B C : S}(A=B : A =S B)(B=C : B =S C)(x : El C) ->
            transS A=B B=C << x == A=B << B=C << x
  trans<< {nat       }{nat       }{pi _ _    } _ (eqS ()) _
  trans<< {nat       }{nat       }{sigma _ _ } _ (eqS ()) _
  trans<< {nat       }{pi _ _    }               (eqS ()) _ _
  trans<< {nat       }{sigma _ _ }               (eqS ()) _ _
  trans<< {pi _ _    }{nat       }               (eqS ()) _ _
  trans<< {pi _ _    }{pi _ _    }{nat       } _ (eqS ()) _
  trans<< {pi _ _    }{pi _ _    }{sigma _ _ } _ (eqS ()) _
  trans<< {pi _ _    }{sigma _ _ }               (eqS ()) _ _
  trans<< {sigma _ _ }{nat       }               (eqS ()) _ _
  trans<< {sigma _ _ }{pi _ _    }               (eqS ()) _ _
  trans<< {sigma _ _ }{sigma _ _ }{nat       } _ (eqS ()) _
  trans<< {sigma _ _ }{sigma _ _ }{pi _ _    } _ (eqS ()) _
  trans<< {nat}{nat}{nat} _ _ _ = ref
  trans<< {pi A F}{pi B G}{pi C H}
          (eqS < B=A , F=G >)(eqS < C=B , G=H >)
          (el < h , ph >) = eq prf
    where
      C=A = transS C=B B=A
      prf : (x : El A) -> _
      prf x =
        chain> _ << h (C=A << x)
           === _ << _ << h (C=B << B=A << x)     by p<< _ (ph (trans<< _ _ x))
           === F=G x << G=H _ << h (_ << _ << x) by pfi2 _ _ _ _ _
        where open module C' = Chain _==_ (ref {_}) (trans {_})
  trans<< {sigma A F}{sigma B G}{sigma C H}
          (eqS < A=B , F=G >)(eqS < B=C , G=H >)
          (el < z , Hz >) = eq < trans<< A=B B=C z , prf >
    where
      prf =
        chain> _ << Hz
           === _ << Hz                   by pfi _ _ _
           === _ << _ << Hz              by trans<< _ _ _
           === _ << F=G _ << G=H z << Hz by trans<< _ _ _
        where open module C' = Chain _==_ (ref {_}) (trans {_})

  -- we never need this one, but it feels like it should be here...
  sym<< : {A B : S}(A=B : A =S B)(x : El B) ->
          symS A=B << A=B << x == x
  sym<< A=B x =
    chain> symS A=B << A=B << x
       === refS << x       by casttrans _ _ _ x
       === x               by ref<< x
    where open module C' = Chain _==_ (ref {_}) (trans {_})

  castref : {A : S}(p : A =S A)(x : El A) -> p << x == x
  castref A=A x =
    chain> A=A << x
       === refS << x  by pfi A=A refS x
       === x          by ref<< x
    where open module C = Chain _==_ (ref {_}) (trans {_})

  casttrans : {A B C : S}(A=B : A =S B)(B=C : B =S C)(A=C : A =S C)(x : El C) ->
               A=B << B=C << x == A=C << x
  casttrans A=B B=C A=C x =
    chain> A=B << B=C << x
       === _ << x     by sym (trans<< _ _ _)
       === A=C << x   by pfi _ _ _
    where open module C' = Chain _==_ (ref {_}) (trans {_})

  pfi2 : {A B1 B2 C : S}
         (A=B1 : A =S B1)(A=B2 : A =S B2)(B1=C : B1 =S C)(B2=C : B2 =S C)
         (x : El C) -> A=B1 << B1=C << x == A=B2 << B2=C << x
  pfi2 A=B1 A=B2 B1=C B2=C x =
    chain> A=B1 << B1=C << x
       === _ << x             by casttrans _ _ _ x
       === A=B2 << B2=C << x  by trans<< _ _ x
    where
      open module C = Chain _==_ (ref {_}) (trans {_})

  ref : {A : S} -> Refl {El A} _==_
  ref {nat}       {el n}          = eq (refN {n})
  ref {pi A F}    {el < f , pf >} = eq \x -> ref
  ref {sigma A F} {el < x , Fx >} = eq < ref , sym (castref _ _) >

  trans : {A : S} -> Trans {El A} _==_
  trans {nat}{el x}{el y}{el z} (eq p) (eq q) = eq (transN {x}{y}{z} p q)
  trans {pi A F}{el < f , pf >}{el < g , pg >}{el < h , ph >}
        (eq f=g)(eq g=h) = eq \x -> trans (f=g x) (g=h x)
  trans {sigma A F}{el < x , Fx >}{el < y , Fy >}{el < z , Fz >}
        (eq < x=y , Fx=Fy >)(eq < y=z , Fy=Fz >) =
        eq < x=z , Fx=Fz >
    where
      x=z   = trans x=y y=z
      Fx=Fz =
        chain> Fx
           === pFam F x=y << Fy               by Fx=Fy
           === pFam F x=y << pFam F y=z << Fz by p<< _ Fy=Fz
           === pFam F x=z << Fz               by casttrans _ _ _ _
        where open module C = Chain _==_ (ref {_}) (trans {_})

  sym : {A : S} -> Sym {El A} _==_
  sym {nat}{el x}{el y} (eq p)  = eq (symN {x}{y} p)
  sym {pi A F}{el < f , pf >}{el < g , pg >}
      (eq f=g) = eq \x -> sym (f=g x)
  sym {sigma A F}{el < x , Fx >}{el < y , Fy >}
      (eq < x=y , Fx=Fy >) = eq < y=x , Fy=Fx >
    where
      y=x = sym x=y
      Fy=Fx = sym (
        chain> pFam F y=x << Fx
           === pFam F y=x << pFam F x=y << Fy by p<< (pFam F y=x) Fx=Fy
           === refS << Fy                     by casttrans _ _ _ _
           === Fy                             by castref _ _
        )
        where open module C = Chain _==_ (ref {_}) (trans {_})

refFam : {A : S} -> Refl (_=Fam_ {A})
refFam x = refS

transFam : {A : S} -> Trans (_=Fam_ {A})
transFam F=G G=H x = transS (F=G x) (G=H x)

symFam : {A : S} -> Sym (_=Fam_ {A})
symFam F=G x = symS (F=G x)

castref2 : {A B : S}(A=B : A =S B)(B=A : B =S A)(x : El A) ->
           A=B << B=A << x == x
castref2 A=B B=A x = trans (casttrans A=B B=A refS x) (ref<< x)


text:
{-# OPTIONS --rewriting #-}
module Examples where

import Examples.Syntax
import Examples.OpSem
import Examples.Run
import Examples.Type

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
------------------------------------------------------------------------
-- Untyped hereditary substitution in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Syntax.HereditarySubstitution where

open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (zero; suc)
open import Data.List using ([]; _∷_; _++_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε)
open import Relation.Binary.PropositionalEquality as P hiding ([_])

open import FOmegaInt.Reduction.Full
open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution

open Syntax

----------------------------------------------------------------------
-- Untyped hereditary substitution.

infixl 9 _?∙∙⟨_⟩_ _∙∙⟨_⟩_ _⌜·⌝⟨_⟩_ _↓⌜·⌝_
infixl 8 _/⟨_⟩_ _//⟨_⟩_ _Kind/⟨_⟩_ _Asc/⟨_⟩_

-- TODO: explain why there are degenerate cases.
mutual

  -- Apply a herediary substition to an elimination, kind or spine.

  _/⟨_⟩_ : ∀ {m n} → Elim m → SKind → SVSub m n → Elim n
  var x   ∙ as /⟨ k ⟩ σ = lookupSV σ x ?∙∙⟨ k ⟩ (as //⟨ k ⟩ σ)
  ⊥       ∙ as /⟨ k ⟩ σ = ⊥ ∙ (as //⟨ k ⟩ σ)
  ⊤       ∙ as /⟨ k ⟩ σ = ⊤ ∙ (as //⟨ k ⟩ σ)
  Π j a   ∙ as /⟨ k ⟩ σ = Π (j Kind/⟨ k ⟩ σ) (a /⟨ k ⟩ σ ↑) ∙ (as //⟨ k ⟩ σ)
  (a ⇒ b) ∙ as /⟨ k ⟩ σ = ((a /⟨ k ⟩ σ) ⇒ (b /⟨ k ⟩ σ))  ∙ (as //⟨ k ⟩ σ)
  Λ j a   ∙ as /⟨ k ⟩ σ = Λ (j Kind/⟨ k ⟩ σ) (a /⟨ k ⟩ σ ↑) ∙ (as //⟨ k ⟩ σ)
  ƛ a b   ∙ as /⟨ k ⟩ σ = ƛ (a /⟨ k ⟩ σ) (b /⟨ k ⟩ σ ↑) ∙ (as //⟨ k ⟩ σ)
  a ⊡ b   ∙ as /⟨ k ⟩ σ = (a /⟨ k ⟩ σ) ⊡ (b /⟨ k ⟩ σ)    ∙ (as //⟨ k ⟩ σ)

  _Kind/⟨_⟩_ : ∀ {m n} → Kind Elim m → SKind → SVSub m n → Kind Elim n
  (a ⋯ b) Kind/⟨ k ⟩ σ = (a /⟨ k ⟩ σ) ⋯ (b /⟨ k ⟩ σ)
  Π j₁ j₂   Kind/⟨ k ⟩ σ = Π (j₁ Kind/⟨ k ⟩ σ) (j₂ Kind/⟨ k ⟩ σ ↑)

  _//⟨_⟩_ : ∀ {m n} → Spine m → SKind → SVSub m n → Spine n
  []       //⟨ k ⟩ σ = []
  (a ∷ as) //⟨ k ⟩ σ = a /⟨ k ⟩ σ ∷ as //⟨ k ⟩ σ

  -- Apply a lookup-result to a spine, performing β-reduction if possible.

  _?∙∙⟨_⟩_ : ∀ {n} → SVRes n → SKind → Spine n → Elim n
  hit a  ?∙∙⟨ k ⟩ as = a  ∙∙⟨ k ⟩ as
  miss y ?∙∙⟨ k ⟩ as = var y ∙ as

  -- Apply an elimination to a spine, performing β-reduction if possible.
  --
  -- NOTE.  Degenerate cases are marked "!".

  _∙∙⟨_⟩_ : ∀ {n} → Elim n → SKind → Spine n → Elim n
  a ∙∙⟨ k ⟩     []       = a
  a ∙∙⟨ ★ ⟩     (b ∷ bs) = a ∙∙ (b ∷ bs)               -- ! a ill-kinded
  a ∙∙⟨ j ⇒ k ⟩ (b ∷ bs) = a ⌜·⌝⟨ j ⇒ k ⟩ b ∙∙⟨ k ⟩ bs

  -- Apply one elimination to another, performing β-reduction if possible.
  --
  -- NOTE.  Degenerate cases are marked "!".

  _⌜·⌝⟨_⟩_ : ∀ {n} → Elim n → SKind → Elim n → Elim n
  a              ⌜·⌝⟨ ★ ⟩     b = a ⌜·⌝ b              -- ! a ill-kinded
  (a ∙ (c ∷ cs)) ⌜·⌝⟨ j ⇒ k ⟩ b = a ∙ (c ∷ cs) ⌜·⌝ b   -- ! unless a = var x
  (Λ l a ∙ [])   ⌜·⌝⟨ j ⇒ k ⟩ b = a /⟨ j ⟩ (sub b)
  {-# CATCHALL #-}
  (a ∙ [])       ⌜·⌝⟨ j ⇒ k ⟩ b = a ∙ (b ∷ [])         -- ! unless a = var x

-- Apply a herediary substition to a kind or type ascription.

_Asc/⟨_⟩_ : ∀ {m n} → ElimAsc m → SKind → SVSub m n → ElimAsc n
kd j Asc/⟨ k ⟩ σ = kd (j Kind/⟨ k ⟩ σ)
tp a Asc/⟨ k ⟩ σ = tp (a /⟨ k ⟩ σ)

-- Some shorthands.

_[_∈_] : ∀ {n} → Elim (suc n) → Elim n → SKind → Elim n
a [ b ∈ k ] = a /⟨ k ⟩ sub b

_Kind[_∈_] : ∀ {n} → Kind Elim (suc n) → Elim n → SKind → Kind Elim n
j Kind[ a ∈ k ] = j Kind/⟨ k ⟩ sub a

-- A variant of application that is reducing (only) if the first
-- argument is a type abstraction.

_↓⌜·⌝_ : ∀ {n} → Elim n → Elim n → Elim n
(a ∙ (b ∷ bs)) ↓⌜·⌝ c = (a ∙ (b ∷ bs)) ⌜·⌝ c
(Λ k a ∙ [])   ↓⌜·⌝ b = a [ b ∈ ⌊ k ⌋ ]
{-# CATCHALL #-}
(a ∙ [])       ↓⌜·⌝ b = a ∙ (b ∷ [])

----------------------------------------------------------------------
-- Properties of (untyped) hereditary substitution.

-- Some exact lemmas about hereditary substitutions (up to
-- α-equality).

module _ where
  open SimpleCtx using (⌊_⌋Asc; kd; tp)

  -- Simplified kinds are stable under application of hereditary
  -- substitutions.

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

  ⌊⌋-Asc/⟨⟩ : ∀ {m n} (a : ElimAsc m) {k} {σ : SVSub m n} →
             ⌊ a Asc/⟨ k ⟩ σ ⌋Asc ≡ ⌊ a ⌋Asc
  ⌊⌋-Asc/⟨⟩ (kd k) = cong kd (⌊⌋-Kind/⟨⟩ k)
  ⌊⌋-Asc/⟨⟩ (tp a) = refl

  -- Hereditary substitutions in spines commute with concatenation.

  ++-//⟨⟩ : ∀ {k m n} (as bs : Spine m) {σ : SVSub m n} →
            (as ++ bs) //⟨ k ⟩ σ ≡ as //⟨ k ⟩ σ ++ bs //⟨ k ⟩ σ
  ++-//⟨⟩ []       bs     = refl
  ++-//⟨⟩ (a ∷ as) bs {σ} = cong (a /⟨ _ ⟩ σ ∷_) (++-//⟨⟩ as bs)

  open Substitution using (_Elim/_; _Kind′/_; _//_)

  -- Hereditary substitutions and reducing applications at ★
  -- degenerate to ordinary substitutions and applications.

  mutual

    /⟨★⟩-/ : ∀ {m n} (a : Elim m) {σ : SVSub m n} →
             a /⟨ ★ ⟩ σ ≡ a Elim/ toSub σ
    /⟨★⟩-/ (var x   ∙ as) {σ} = begin
        lookupSV σ x ?∙∙⟨ ★ ⟩ (as //⟨ ★ ⟩ σ)
      ≡⟨ ?∙∙⟨★⟩-∙∙ (lookupSV σ x) ⟩
        toElim (lookupSV σ x) ∙∙ (as //⟨ ★ ⟩ σ)
      ≡⟨ cong₂ _∙∙_ (sym (⌜⌝∘⌞⌟-id _)) (//⟨★⟩-// as) ⟩
        ⌜ ⌞ toElim (lookupSV σ x) ⌟ ⌝ ∙∙ (as // toSub σ)
      ≡˘⟨ cong (_∙∙ _) (cong ⌜_⌝ (lookup-toSub σ x)) ⟩
        var x ∙ as Elim/ toSub σ
      ∎
      where open ≡-Reasoning
    /⟨★⟩-/ (⊥       ∙ as) = cong (⊥ ∙_) (//⟨★⟩-// as)
    /⟨★⟩-/ (⊤       ∙ as) = cong (⊤ ∙_) (//⟨★⟩-// as)
    /⟨★⟩-/ (Π k b   ∙ as) =
      cong₂ _∙_ (cong₂ Π (Kind/⟨★⟩-/ k) (/⟨★⟩-/ b)) (//⟨★⟩-// as)
    /⟨★⟩-/ ((b ⇒ c) ∙ as) =
      cong₂ _∙_ (cong₂ _⇒_ (/⟨★⟩-/ b) (/⟨★⟩-/ c)) (//⟨★⟩-// as)
    /⟨★⟩-/ (Λ k b   ∙ as) =
      cong₂ _∙_ (cong₂ Λ (Kind/⟨★⟩-/ k) (/⟨★⟩-/ b)) (//⟨★⟩-// as)
    /⟨★⟩-/ (ƛ b c   ∙ as) =
      cong₂ _∙_ (cong₂ ƛ (/⟨★⟩-/ b) (/⟨★⟩-/ c)) (//⟨★⟩-// as)
    /⟨★⟩-/ (b ⊡ c   ∙ as) =
      cong₂ _∙_ (cong₂ _⊡_ (/⟨★⟩-/ b) (/⟨★⟩-/ c)) (//⟨★⟩-// as)

    //⟨★⟩-// : ∀ {m n} (as : Spine m) {σ : SVSub m n} →
               as //⟨ ★ ⟩ σ ≡ as // toSub σ
    //⟨★⟩-// []       = refl
    //⟨★⟩-// (a ∷ as) = cong₂ _∷_ (/⟨★⟩-/ a) (//⟨★⟩-// as)

    Kind/⟨★⟩-/ : ∀ {m n} (k : Kind Elim m) {σ : SVSub m n} →
                 k Kind/⟨ ★ ⟩ σ ≡ k Kind′/ toSub σ
    Kind/⟨★⟩-/ (a ⋯ b) = cong₂ _⋯_ (/⟨★⟩-/ a) (/⟨★⟩-/ b)
    Kind/⟨★⟩-/ (Π j k) = cong₂ Π (Kind/⟨★⟩-/ j) (Kind/⟨★⟩-/ k)

    ?∙∙⟨★⟩-∙∙ : ∀ {n} (r : SVRes n) {as} → r ?∙∙⟨ ★ ⟩ as ≡ toElim r ∙∙ as
    ?∙∙⟨★⟩-∙∙ (hit a)  = ∙∙⟨★⟩-∙∙ a
    ?∙∙⟨★⟩-∙∙ (miss y) = refl

    ∙∙⟨★⟩-∙∙ : ∀ {n} (a : Elim n) {bs} → a ∙∙⟨ ★ ⟩ bs ≡ a ∙∙ bs
    ∙∙⟨★⟩-∙∙ a {[]}     = sym (∙∙-[] a)
    ∙∙⟨★⟩-∙∙ a {b ∷ bs} = refl

module RenamingCommutes where
  open Substitution
    hiding (_↑; _↑⋆_; sub; _/Var_) renaming (_Elim/Var_ to _/Var_)
  open P.≡-Reasoning
  private
    module S = Substitution
    module V = VarSubst

  mutual

    -- Hereditary substitution commutes with renaming.
    --
    -- NOTE: this is a variant of the `sub-commutes' lemma from
    -- Data.Fin.Substitution.Lemmas adapted to hereditary
    -- substitutions and renaming.

    /⟨⟩-/Var-↑⋆ : ∀ i {m n} a k b {ρ : Sub Fin m n} →
                  b /⟨ k ⟩ sub a ↑⋆ i /Var ρ V.↑⋆ i ≡
                    b /Var (ρ V.↑) V.↑⋆ i /⟨ k ⟩ sub (a /Var ρ) ↑⋆ i
    /⟨⟩-/Var-↑⋆ i a k (var x ∙ bs) {ρ} = begin
        var x ∙ bs /⟨ k ⟩ sub a ↑⋆ i /Var ρ V.↑⋆ i
      ≡⟨⟩
        lookupSV (sub a ↑⋆ i) x ?∙∙⟨ k ⟩ (bs //⟨ k ⟩ sub a ↑⋆ i) /Var ρ V.↑⋆ i
      ≡⟨ ?∙∙⟨⟩-/Var (lookupSV (sub a ↑⋆ i) x) k (bs //⟨ k ⟩ sub a ↑⋆ i) ⟩
        (lookupSV (sub a ↑⋆ i) x ?/Var ρ V.↑⋆ i) ?∙∙⟨ k ⟩
          (bs //⟨ k ⟩ sub a ↑⋆ i //Var ρ V.↑⋆ i)
      ≡⟨ cong₂ _?∙∙⟨ k ⟩_ (lookup-sub-/Var-↑⋆ a i x) (//⟨⟩-/Var-↑⋆ i a k bs) ⟩
        lookupSV (sub (a /Var ρ) ↑⋆ i) (x V./ (ρ V.↑) V.↑⋆ i) ?∙∙⟨ k ⟩
          (bs //Var (ρ V.↑) V.↑⋆ i //⟨ k ⟩ sub (a /Var ρ) ↑⋆ i)
      ≡⟨⟩
        var x ∙ bs /Var (ρ V.↑) V.↑⋆ i /⟨ k ⟩ sub (a /Var ρ) ↑⋆ i
      ∎
    /⟨⟩-/Var-↑⋆ i a k (⊥     ∙ bs)   = cong (⊥ ∙_) (//⟨⟩-/Var-↑⋆ i a k bs)
    /⟨⟩-/Var-↑⋆ i a k (⊤     ∙ bs)   = cong (⊤ ∙_) (//⟨⟩-/Var-↑⋆ i a k bs)
    /⟨⟩-/Var-↑⋆ i a k (Π j b ∙ bs)   =
      cong₂ _∙_ (cong₂ Π (Kind/⟨⟩-/Var-↑⋆ i a k j) (/⟨⟩-/Var-↑⋆ (suc i) a k b))
                (//⟨⟩-/Var-↑⋆ i a k bs)
    /⟨⟩-/Var-↑⋆ i a k ((b ⇒ c) ∙ bs) =
      cong₂ _∙_ (cong₂ _⇒_ (/⟨⟩-/Var-↑⋆ i a k b) (/⟨⟩-/Var-↑⋆ i a k c))
                (//⟨⟩-/Var-↑⋆ i a k bs)
    /⟨⟩-/Var-↑⋆ i a k (Λ j b ∙ bs)   =
      cong₂ _∙_ (cong₂ Λ (Kind/⟨⟩-/Var-↑⋆ i a k j) (/⟨⟩-/Var-↑⋆ (suc i) a k b))
                (//⟨⟩-/Var-↑⋆ i a k bs)
    /⟨⟩-/Var-↑⋆ i a k (ƛ b c ∙ bs)   =
      cong₂ _∙_ (cong₂ ƛ (/⟨⟩-/Var-↑⋆ i a k b) (/⟨⟩-/Var-↑⋆ (suc i) a k c))
                (//⟨⟩-/Var-↑⋆ i a k bs)
    /⟨⟩-/Var-↑⋆ i a k (b ⊡ c ∙ bs)   =
      cong₂ _∙_ (cong₂ _⊡_ (/⟨⟩-/Var-↑⋆ i a k b) (/⟨⟩-/Var-↑⋆ i a k c))
                (//⟨⟩-/Var-↑⋆ i a k bs)

    Kind/⟨⟩-/Var-↑⋆ : ∀ i {m n} a k j {ρ : Sub Fin m n} →
                      j Kind/⟨ k ⟩ sub a ↑⋆ i Kind′/Var ρ V.↑⋆ i ≡
                        j Kind′/Var (ρ V.↑) V.↑⋆ i Kind/⟨ k ⟩ sub (a /Var ρ) ↑⋆ i
    Kind/⟨⟩-/Var-↑⋆ i a k (b ⋯ c) =
      cong₂ _⋯_ (/⟨⟩-/Var-↑⋆ i a k b) (/⟨⟩-/Var-↑⋆ i a k c)
    Kind/⟨⟩-/Var-↑⋆ i a k (Π j l) =
      cong₂ Π (Kind/⟨⟩-/Var-↑⋆ i a k j) (Kind/⟨⟩-/Var-↑⋆ (suc i) a k l)

    //⟨⟩-/Var-↑⋆ : ∀ i {n m} a k bs {ρ : Sub Fin m n} →
                   bs //⟨ k ⟩ sub a ↑⋆ i //Var ρ V.↑⋆ i ≡
                     (bs //Var (ρ V.↑) V.↑⋆ i) //⟨ k ⟩ sub (a /Var ρ) ↑⋆ i
    //⟨⟩-/Var-↑⋆ i a k []       = refl
    //⟨⟩-/Var-↑⋆ i a k (b ∷ bs) =
      cong₂ _∷_ (/⟨⟩-/Var-↑⋆ i a k b) (//⟨⟩-/Var-↑⋆ i a k bs)

    -- Reducing applications commute with renaming.

    ?∙∙⟨⟩-/Var : ∀ {m n} r k bs {ρ : Sub Fin m n} →
                 r ?∙∙⟨ k ⟩ bs /Var ρ ≡ (r ?/Var ρ) ?∙∙⟨ k ⟩ (bs //Var ρ)
    ?∙∙⟨⟩-/Var (hit a)  k as = ∙∙⟨⟩-/Var a k as
    ?∙∙⟨⟩-/Var (miss y) k as = refl

    ∙∙⟨⟩-/Var : ∀ {m n} a k bs {ρ : Sub Fin m n} →
                a ∙∙⟨ k ⟩ bs /Var ρ ≡ (a /Var ρ) ∙∙⟨ k ⟩ (bs //Var ρ)
    ∙∙⟨⟩-/Var a k       []           = refl
    ∙∙⟨⟩-/Var a ★       (b ∷ bs)     = S.∙∙-/Var a (b ∷ bs)
    ∙∙⟨⟩-/Var a (j ⇒ k) (b ∷ bs) {ρ} = begin
        a ⌜·⌝⟨ j ⇒ k ⟩ b ∙∙⟨ k ⟩ bs /Var ρ
      ≡⟨ ∙∙⟨⟩-/Var (a ⌜·⌝⟨ j ⇒ k ⟩ b) k bs ⟩
        (a ⌜·⌝⟨ j ⇒ k ⟩ b /Var ρ) ∙∙⟨ k ⟩ (bs //Var ρ)
      ≡⟨ cong (_∙∙⟨ k ⟩ (bs //Var ρ)) (⌜·⌝⟨⟩-/Var a (j ⇒ k) b) ⟩
        (a /Var ρ) ⌜·⌝⟨ j ⇒ k ⟩ (b /Var ρ) ∙∙⟨ k ⟩ (bs //Var ρ)
      ∎

    ⌜·⌝⟨⟩-/Var : ∀ {m n} a k b {ρ : Sub Fin m n} →
                 a ⌜·⌝⟨ k ⟩ b /Var ρ ≡ (a /Var ρ) ⌜·⌝⟨ k ⟩ (b /Var ρ)
    ⌜·⌝⟨⟩-/Var a ★                    b     = S.⌜·⌝-/Var a b
    ⌜·⌝⟨⟩-/Var (a ∙ (c ∷ cs)) (j ⇒ k) b {ρ} = begin
        a ∙ (c ∷ cs) ⌜·⌝ b /Var ρ
      ≡⟨ S.⌜·⌝-/Var (a ∙ (c ∷ cs)) b ⟩
        (a ∙ (c ∷ cs) /Var ρ) ⌜·⌝ (b /Var ρ)
      ≡˘⟨ cong (λ a → a ∙∙ _ ⌜·⌝ (b /Var ρ)) (S.Head/Var-∙ a) ⟩
        (a Head/Var ρ) ∙ ((c ∷ cs) //Var ρ) ⌜·⌝⟨ j ⇒ k ⟩ (b /Var ρ)
      ≡⟨ cong (λ a → a ∙∙ _ ⌜·⌝⟨ j ⇒ k ⟩ (b /Var ρ)) (S.Head/Var-∙ a) ⟩
        (a ∙ (c ∷ cs) /Var ρ) ⌜·⌝⟨ j ⇒ k ⟩ (b /Var ρ)
      ∎
    ⌜·⌝⟨⟩-/Var (var x   ∙ []) (j ⇒ k) b = refl
    ⌜·⌝⟨⟩-/Var (⊥       ∙ []) (j ⇒ k) b = refl
    ⌜·⌝⟨⟩-/Var (⊤       ∙ []) (j ⇒ k) b = refl
    ⌜·⌝⟨⟩-/Var (Π l a   ∙ []) (j ⇒ k) b = refl
    ⌜·⌝⟨⟩-/Var ((a ⇒ b) ∙ []) (j ⇒ k) c = refl
    ⌜·⌝⟨⟩-/Var (Λ l a   ∙ []) (j ⇒ k) b = /⟨⟩-/Var-↑⋆ 0 b j a
    ⌜·⌝⟨⟩-/Var (ƛ a b   ∙ []) (j ⇒ k) c = refl
    ⌜·⌝⟨⟩-/Var (a ⊡ b   ∙ []) (j ⇒ k) c = refl

  -- Some corollaries of the above.

  Asc/⟨⟩-/Var-↑⋆ : ∀ i {m n} a k b {ρ : Sub Fin m n} →
                   b Asc/⟨ k ⟩ sub a ↑⋆ i ElimAsc/Var ρ V.↑⋆ i ≡
                     b ElimAsc/Var (ρ V.↑) V.↑⋆ i Asc/⟨ k ⟩ sub (a /Var ρ) ↑⋆ i
  Asc/⟨⟩-/Var-↑⋆ i a k (kd j) = cong kd (Kind/⟨⟩-/Var-↑⋆ i a k j)
  Asc/⟨⟩-/Var-↑⋆ i a k (tp b) = cong tp (/⟨⟩-/Var-↑⋆ i a k b)

  [∈⌊⌋]-/Var : ∀ {m n} a b k {ρ : Sub Fin m n} →
               a [ b ∈ ⌊ k ⌋ ] /Var ρ ≡
                 (a /Var ρ V.↑) [ b /Var ρ ∈ ⌊ k Kind′/Var ρ ⌋ ]
  [∈⌊⌋]-/Var a b k {ρ} = begin
      (a [ b ∈ ⌊ k ⌋ ] /Var ρ)
    ≡⟨ /⟨⟩-/Var-↑⋆ 0 b ⌊ k ⌋ a ⟩
      ((a /Var ρ V.↑) [ b /Var ρ ∈ ⌊ k ⌋ ])
    ≡˘⟨ cong (a /Var ρ V.↑ /⟨_⟩ sub (b /Var ρ)) (S.⌊⌋-Kind′/Var k) ⟩
      ((a /Var ρ V.↑) [ b /Var ρ ∈ ⌊ k Kind′/Var ρ ⌋ ])
    ∎

  Kind[∈⌊⌋]-/Var : ∀ {m n} j a k {ρ : Sub Fin m n} →
                   j Kind[ a ∈ ⌊ k ⌋ ] Kind′/Var ρ ≡
                     (j Kind′/Var ρ V.↑) Kind[ a /Var ρ ∈ ⌊ k Kind′/Var ρ ⌋ ]
  Kind[∈⌊⌋]-/Var j a k {ρ} = begin
      j Kind[ a ∈ ⌊ k ⌋ ] Kind′/Var ρ
    ≡⟨ Kind/⟨⟩-/Var-↑⋆ 0 a ⌊ k ⌋ j ⟩
      (j Kind′/Var ρ V.↑) Kind[ a /Var ρ ∈ ⌊ k ⌋ ]
    ≡˘⟨ cong (j Kind′/Var ρ V.↑ Kind/⟨_⟩ sub (a /Var ρ)) (S.⌊⌋-Kind′/Var k) ⟩
      (j Kind′/Var ρ V.↑) Kind[ a /Var ρ ∈ ⌊ k Kind′/Var ρ ⌋ ]
    ∎

  -- Potentially reducing applications commute with renaming.

  ↓⌜·⌝-/Var : ∀ {m n} a b {ρ : Sub Fin m n} →
              a ↓⌜·⌝ b /Var ρ ≡ (a /Var ρ) ↓⌜·⌝ (b /Var ρ)
  ↓⌜·⌝-/Var (a ∙ (c ∷ cs)) b {ρ} = begin
      a ∙ (c ∷ cs) ⌜·⌝ b /Var ρ
    ≡⟨ S.⌜·⌝-/Var (a ∙ (c ∷ cs)) b ⟩
      (a ∙ (c ∷ cs) /Var ρ) ⌜·⌝ (b /Var ρ)
    ≡˘⟨ cong (λ a → a ∙∙ _ ⌜·⌝ (b /Var ρ)) (S.Head/Var-∙ a) ⟩
      (a Head/Var ρ) ∙ ((c ∷ cs) //Var ρ) ↓⌜·⌝ (b /Var ρ)
    ≡⟨ cong (λ a → a ∙∙ _ ↓⌜·⌝ (b /Var ρ)) (S.Head/Var-∙ a) ⟩
      (a ∙ (c ∷ cs) /Var ρ) ↓⌜·⌝ (b /Var ρ)
    ∎
  ↓⌜·⌝-/Var (var x   ∙ []) b = refl
  ↓⌜·⌝-/Var (⊥       ∙ []) b = refl
  ↓⌜·⌝-/Var (⊤       ∙ []) b = refl
  ↓⌜·⌝-/Var (Π l a   ∙ []) b = refl
  ↓⌜·⌝-/Var ((a ⇒ b) ∙ []) c = refl
  ↓⌜·⌝-/Var (Λ l a   ∙ []) b = [∈⌊⌋]-/Var a b l
  ↓⌜·⌝-/Var (ƛ a b   ∙ []) c = refl
  ↓⌜·⌝-/Var (a ⊡ b   ∙ []) c = refl

  mutual

    -- Weakening commutes with application of lifted hereditary
    -- substitutions.
    --
    -- NOTE: this is a variant of the `wk-commutes' lemma from
    -- Data.Fin.Substitution.Lemmas adapted to hereditary
    -- substitutions.

    wk-/⟨⟩-↑⋆ : ∀ i {k m n} a {σ : SVSub m n} →
                a /Var V.wk V.↑⋆ i /⟨ k ⟩ (σ ↑) ↑⋆ i ≡
                  a /⟨ k ⟩ σ ↑⋆ i /Var V.wk V.↑⋆ i
    wk-/⟨⟩-↑⋆ i {k} (var x ∙ as) {σ} = begin
        var x ∙ as /Var V.wk V.↑⋆ i /⟨ k ⟩ (σ ↑) ↑⋆ i
      ≡⟨⟩
        lookupSV ((σ ↑) ↑⋆ i) (x V./ V.wk V.↑⋆ i) ?∙∙⟨ k ⟩
          (as //Var V.wk V.↑⋆ i //⟨ k ⟩ ((σ ↑) ↑⋆ i))
      ≡⟨ (cong₂ (_?∙∙⟨ k ⟩_)) (sym (lookup-/Var-wk-↑⋆ i x)) (wk-//⟨⟩-↑⋆ i as) ⟩
        (lookupSV (σ ↑⋆ i) x ?/Var V.wk V.↑⋆ i) ?∙∙⟨ k ⟩
          (as //⟨ k ⟩ (σ ↑⋆ i) //Var V.wk V.↑⋆ i)
      ≡˘⟨ ?∙∙⟨⟩-/Var (lookupSV (σ ↑⋆ i) x) k (as //⟨ k ⟩ (σ ↑⋆ i)) ⟩
        lookupSV (σ ↑⋆ i) x ?∙∙⟨ k ⟩ (as //⟨ k ⟩ (σ ↑⋆ i)) /Var V.wk V.↑⋆ i
      ≡⟨⟩
        var x ∙ as /⟨ k ⟩ σ ↑⋆ i /Var V.wk V.↑⋆ i
      ∎
    wk-/⟨⟩-↑⋆ i (⊥ ∙ as)       = cong (⊥ ∙_) (wk-//⟨⟩-↑⋆ i as)
    wk-/⟨⟩-↑⋆ i (⊤ ∙ as)       = cong (⊤ ∙_) (wk-//⟨⟩-↑⋆ i as)
    wk-/⟨⟩-↑⋆ i (Π k a ∙ as)   =
      cong₂ _∙_ (cong₂ Π (wk-Kind/⟨⟩-↑⋆ i k) (wk-/⟨⟩-↑⋆ (suc i) a))
                (wk-//⟨⟩-↑⋆ i as)
    wk-/⟨⟩-↑⋆ i ((a ⇒ b) ∙ as) =
      cong₂ _∙_ (cong₂ _⇒_ (wk-/⟨⟩-↑⋆ i a) (wk-/⟨⟩-↑⋆ i b)) (wk-//⟨⟩-↑⋆ i as)
    wk-/⟨⟩-↑⋆ i (Λ k a ∙ as)   =
      cong₂ _∙_ (cong₂ Λ (wk-Kind/⟨⟩-↑⋆ i k) (wk-/⟨⟩-↑⋆ (suc i) a))
                (wk-//⟨⟩-↑⋆ i as)
    wk-/⟨⟩-↑⋆ i (ƛ a b ∙ as)   =
      cong₂ _∙_ (cong₂ ƛ (wk-/⟨⟩-↑⋆ i a) (wk-/⟨⟩-↑⋆ (suc i) b)) (wk-//⟨⟩-↑⋆ i as)
    wk-/⟨⟩-↑⋆ i (a ⊡ b ∙ as)   =
      cong₂ _∙_ (cong₂ _⊡_ (wk-/⟨⟩-↑⋆ i a) (wk-/⟨⟩-↑⋆ i b)) (wk-//⟨⟩-↑⋆ i as)

    wk-Kind/⟨⟩-↑⋆ : ∀ i {k m n} j {σ : SVSub m n} →
                    j Kind′/Var V.wk V.↑⋆ i Kind/⟨ k ⟩ (σ ↑) ↑⋆ i ≡
                      j Kind/⟨ k ⟩ σ ↑⋆ i Kind′/Var V.wk V.↑⋆ i
    wk-Kind/⟨⟩-↑⋆ i (a ⋯ b) = cong₂ _⋯_ (wk-/⟨⟩-↑⋆ i a) (wk-/⟨⟩-↑⋆ i b)
    wk-Kind/⟨⟩-↑⋆ i (Π j k) =
      cong₂ Π (wk-Kind/⟨⟩-↑⋆ i j) (wk-Kind/⟨⟩-↑⋆ (suc i) k)

    wk-//⟨⟩-↑⋆ : ∀ i {k m n} as {σ : SVSub m n} →
                 as //Var V.wk V.↑⋆ i //⟨ k ⟩ (σ ↑) ↑⋆ i ≡
                   as //⟨ k ⟩ σ ↑⋆ i //Var V.wk V.↑⋆ i
    wk-//⟨⟩-↑⋆ i []       = refl
    wk-//⟨⟩-↑⋆ i (a ∷ as) = cong₂ _∷_ (wk-/⟨⟩-↑⋆ i a) (wk-//⟨⟩-↑⋆ i as)

  -- A corollary of the above.

  wk-Asc/⟨⟩-↑⋆ : ∀ i {k m n} a {σ : SVSub m n} →
                a ElimAsc/Var V.wk V.↑⋆ i Asc/⟨ k ⟩ (σ ↑) ↑⋆ i ≡
                  a Asc/⟨ k ⟩ σ ↑⋆ i ElimAsc/Var V.wk V.↑⋆ i
  wk-Asc/⟨⟩-↑⋆ i (kd a) = cong kd (wk-Kind/⟨⟩-↑⋆ i a)
  wk-Asc/⟨⟩-↑⋆ i (tp a) = cong tp (wk-/⟨⟩-↑⋆ i a)

  mutual

    -- Weakening of a term followed by hereditary substitution of the
    -- newly introduced extra variable leaves the term unchanged.
    --
    -- NOTE: this is a variant of the `wk-sub-vanishes' lemma from
    -- Data.Fin.Substitution.Lemmas adapted to hereditary
    -- substitutions.

    /Var-wk-↑⋆-hsub-vanishes : ∀ i {k m} a {b : Elim m} →
                               a /Var V.wk V.↑⋆ i /⟨ k ⟩ sub b ↑⋆ i ≡ a
    /Var-wk-↑⋆-hsub-vanishes i {k} (var x ∙ as) {b} = begin
        var x ∙ as /Var V.wk V.↑⋆ i /⟨ k ⟩ sub b ↑⋆ i
      ≡⟨ cong₂ _?∙∙⟨ k ⟩_ (lookup-sub-wk-↑⋆ i x)
                          (//Var-wk-↑⋆-hsub-vanishes i as) ⟩
        var x ∙ as
      ∎
    /Var-wk-↑⋆-hsub-vanishes i (⊥ ∙ as)       =
      cong (⊥ ∙_) (//Var-wk-↑⋆-hsub-vanishes i as)
    /Var-wk-↑⋆-hsub-vanishes i (⊤ ∙ as)       =
      cong (⊤ ∙_) (//Var-wk-↑⋆-hsub-vanishes i as)
    /Var-wk-↑⋆-hsub-vanishes i (Π k a ∙ as)   =
      cong₂ _∙_ (cong₂ Π (Kind/Var-wk-↑⋆-hsub-vanishes i k)
                         (/Var-wk-↑⋆-hsub-vanishes (suc i) a))
                (//Var-wk-↑⋆-hsub-vanishes i as)
    /Var-wk-↑⋆-hsub-vanishes i ((a ⇒ b) ∙ as) =
      cong₂ _∙_ (cong₂ _⇒_ (/Var-wk-↑⋆-hsub-vanishes i a)
                           (/Var-wk-↑⋆-hsub-vanishes i b))
                (//Var-wk-↑⋆-hsub-vanishes i as)
    /Var-wk-↑⋆-hsub-vanishes i (Λ k a ∙ as)   =
      cong₂ _∙_ (cong₂ Λ (Kind/Var-wk-↑⋆-hsub-vanishes i k)
                         (/Var-wk-↑⋆-hsub-vanishes (suc i) a))
                (//Var-wk-↑⋆-hsub-vanishes i as)
    /Var-wk-↑⋆-hsub-vanishes i (ƛ a b ∙ as)   =
      cong₂ _∙_ (cong₂ ƛ (/Var-wk-↑⋆-hsub-vanishes i a)
                           (/Var-wk-↑⋆-hsub-vanishes (suc i) b))
                (//Var-wk-↑⋆-hsub-vanishes i as)
    /Var-wk-↑⋆-hsub-vanishes i (a ⊡ b ∙ as)   =
      cong₂ _∙_ (cong₂ _⊡_ (/Var-wk-↑⋆-hsub-vanishes i a)
                           (/Var-wk-↑⋆-hsub-vanishes i b))
                (//Var-wk-↑⋆-hsub-vanishes i as)

    Kind/Var-wk-↑⋆-hsub-vanishes
      : ∀ i {k m} j {b : Elim m} →
        j Kind′/Var V.wk V.↑⋆ i Kind/⟨ k ⟩ sub b ↑⋆ i ≡ j
    Kind/Var-wk-↑⋆-hsub-vanishes i (a ⋯ b) =
      cong₂ _⋯_ (/Var-wk-↑⋆-hsub-vanishes i a) (/Var-wk-↑⋆-hsub-vanishes i b)
    Kind/Var-wk-↑⋆-hsub-vanishes i (Π j k) =
      cong₂ Π (Kind/Var-wk-↑⋆-hsub-vanishes i j)
              (Kind/Var-wk-↑⋆-hsub-vanishes (suc i) k)

    //Var-wk-↑⋆-hsub-vanishes : ∀ i {k m} as {b : Elim m} →
                                as //Var V.wk V.↑⋆ i //⟨ k ⟩ sub b ↑⋆ i ≡ as
    //Var-wk-↑⋆-hsub-vanishes i []       = refl
    //Var-wk-↑⋆-hsub-vanishes i (a ∷ as) =
      cong₂ _∷_ (/Var-wk-↑⋆-hsub-vanishes i a) (//Var-wk-↑⋆-hsub-vanishes i as)

  -- A corollary of the above.
  Asc/Var-wk-↑⋆-hsub-vanishes
    : ∀ i {k m} a {b : Elim m} →
      a S.ElimAsc/Var V.wk V.↑⋆ i Asc/⟨ k ⟩ sub b ↑⋆ i ≡ a
  Asc/Var-wk-↑⋆-hsub-vanishes i (kd a) =
    cong kd (Kind/Var-wk-↑⋆-hsub-vanishes i a)
  Asc/Var-wk-↑⋆-hsub-vanishes i (tp a) =
    cong tp (/Var-wk-↑⋆-hsub-vanishes i a)

open RenamingCommutes

module _ where
  private
    module EL = TermLikeLemmas Substitution.termLikeLemmasElim
    module KL = TermLikeLemmas Substitution.termLikeLemmasKind′
  open Substitution hiding (_↑; _↑⋆_; sub)
  open ≡-Reasoning

  -- Repeated weakening commutes with application of lifted hereditary
  -- substitutions.

  wk⋆-/⟨⟩-↑⋆ : ∀ i {k m n} a {σ : SVSub m n} →
               a Elim/ wk⋆ i /⟨ k ⟩ σ ↑⋆ i ≡ a /⟨ k ⟩ σ Elim/ wk⋆ i
  wk⋆-/⟨⟩-↑⋆ zero {k} a {σ} = begin
    a Elim/ id /⟨ k ⟩ σ   ≡⟨ cong (_/⟨ k ⟩ σ) (EL.id-vanishes a) ⟩
    a /⟨ k ⟩ σ            ≡˘⟨ EL.id-vanishes (a /⟨ k ⟩ σ) ⟩
    a /⟨ k ⟩ σ Elim/ id   ∎
  wk⋆-/⟨⟩-↑⋆ (suc i) {k} a {σ} = begin
      a Elim/ wk⋆ (suc i) /⟨ k ⟩ (σ ↑⋆ i) ↑
    ≡⟨ cong (_/⟨ k ⟩ (σ ↑⋆ i) ↑) (EL./-weaken a) ⟩
      a Elim/ wk⋆ i Elim/ wk /⟨ k ⟩ (σ ↑⋆ i) ↑
    ≡⟨ cong (_/⟨ k ⟩ (σ ↑⋆ i) ↑) (EL./-wk {t = a Elim/ wk⋆ i}) ⟩
      weakenElim (a Elim/ wk⋆ i) /⟨ k ⟩ (σ ↑⋆ i) ↑
    ≡⟨ wk-/⟨⟩-↑⋆ zero (a Elim/ wk⋆ i) ⟩
      weakenElim (a Elim/ wk⋆ i /⟨ k ⟩ σ ↑⋆ i)
    ≡⟨ cong weakenElim (wk⋆-/⟨⟩-↑⋆ i a) ⟩
      weakenElim (a /⟨ k ⟩ σ Elim/ wk⋆ i)
    ≡˘⟨ (EL./-wk {t = a /⟨ k ⟩ σ Elim/ wk⋆ i}) ⟩
      a /⟨ k ⟩ σ Elim/ wk⋆ i Elim/ wk
    ≡˘⟨ EL./-weaken (a /⟨ k ⟩ σ)  ⟩
      a /⟨ k ⟩ σ Elim/ wk⋆ (suc i)
    ∎

  wk⋆-Kind/⟨⟩-↑⋆ : ∀ i {k m n} j {σ : SVSub m n} →
                   j Kind′/ wk⋆ i Kind/⟨ k ⟩ σ ↑⋆ i ≡
                     j Kind/⟨ k ⟩ σ Kind′/ wk⋆ i
  wk⋆-Kind/⟨⟩-↑⋆ zero {k} j {σ} = begin
    j Kind′/ id Kind/⟨ k ⟩ σ   ≡⟨ cong (_Kind/⟨ k ⟩ σ) (KL.id-vanishes j) ⟩
    j Kind/⟨ k ⟩ σ             ≡˘⟨ KL.id-vanishes (j Kind/⟨ k ⟩ σ) ⟩
    j Kind/⟨ k ⟩ σ Kind′/ id   ∎
  wk⋆-Kind/⟨⟩-↑⋆ (suc i) {k} j {σ} = begin
      j Kind′/ wk⋆ (suc i) Kind/⟨ k ⟩ (σ ↑⋆ i) ↑
    ≡⟨ cong (_Kind/⟨ k ⟩ (σ ↑⋆ i) ↑) (KL./-weaken j) ⟩
      j Kind′/ wk⋆ i Kind′/ wk Kind/⟨ k ⟩ (σ ↑⋆ i) ↑
    ≡⟨ cong (_Kind/⟨ k ⟩ (σ ↑⋆ i) ↑) (KL./-wk {t = j Kind′/ wk⋆ i}) ⟩
      weakenKind′ (j Kind′/ wk⋆ i) Kind/⟨ k ⟩ (σ ↑⋆ i) ↑
    ≡⟨ wk-Kind/⟨⟩-↑⋆ zero (j Kind′/ wk⋆ i) ⟩
      weakenKind′ (j Kind′/ wk⋆ i Kind/⟨ k ⟩ σ ↑⋆ i)
    ≡⟨ cong weakenKind′ (wk⋆-Kind/⟨⟩-↑⋆ i j) ⟩
      weakenKind′ (j Kind/⟨ k ⟩ σ Kind′/ wk⋆ i)
    ≡˘⟨ (KL./-wk {t = j Kind/⟨ k ⟩ σ Kind′/ wk⋆ i}) ⟩
      j Kind/⟨ k ⟩ σ Kind′/ wk⋆ i Kind′/ wk
    ≡˘⟨ KL./-weaken (j Kind/⟨ k ⟩ σ)  ⟩
      j Kind/⟨ k ⟩ σ Kind′/ wk⋆ (suc i)
    ∎

  -- A corollary of the above.
  weaken⋆-/⟨⟩-↑⋆ : ∀ i {k m n} a {σ : SVSub m n} →
                   weakenElim⋆ i (a /⟨ k ⟩ σ) ≡ weakenElim⋆ i a /⟨ k ⟩ σ ↑⋆ i
  weaken⋆-/⟨⟩-↑⋆ i {k} a {σ} = begin
    weakenElim⋆ i (a /⟨ k ⟩ σ)     ≡˘⟨ EL./-wk⋆ i ⟩
    a /⟨ k ⟩ σ Elim/ wk⋆ i         ≡˘⟨ wk⋆-/⟨⟩-↑⋆ i a ⟩
    a Elim/ wk⋆ i /⟨ k ⟩ σ ↑⋆ i    ≡⟨ cong (_/⟨ k ⟩ σ ↑⋆ i) (EL./-wk⋆ i) ⟩
    weakenElim⋆ i a /⟨ k ⟩ σ ↑⋆ i  ∎

  -- NOTE. Unfortunately, we cannot prove that arbitrary untyped
  -- hereditary substitutions commute, because *untyped* hereditary
  -- substitutions need not commute with reducting applications in
  -- general.  We will prove a weaker result, namely that well-kinded
  -- hereditary substitutions in well-kinded types commute, later.
  -- See e.g. `Nf∈-[]-/⟨⟩-↑⋆` etc. in module Kinding.Simple.

-- Some commutation lemmas up to βη-equality.

module _ where
  open →β*-Reasoning
  open Substitution hiding (_↑; _↑⋆_; sub)
  private module Kd = Kd→β*-Reasoning

  mutual

    -- Hereditary substitution commutes with ⌞_⌟ up to β-reduction.

    ⌞⌟-/⟨⟩-β : ∀ {m n} a {k} {σ : SVSub m n} →
               ⌞ a ⌟ / toSub σ  →β*  ⌞ a /⟨ k ⟩ σ ⌟
    ⌞⌟-/⟨⟩-β (var x ∙ bs) {k} {σ} = begin
        ⌞ var x ∙ bs ⌟ / toSub σ
      ⟶⋆⟨ ⌞∙⌟-/⟨⟩-β (var x / toSub σ) (var x) bs ε ⟩
        (var x / toSub σ) ⌞∙⌟ ⌞ bs //⟨ k ⟩ σ ⌟Sp
      ≡⟨ cong (_⌞∙⌟ ⌞ bs //⟨ k ⟩ σ ⌟Sp) (lookup-toSub σ x) ⟩
        ⌞ toElim (lookupSV σ x) ⌟ ⌞∙⌟ ⌞ bs //⟨ k ⟩ σ ⌟Sp
      ⟶⋆⟨ ⌞⌟-?∙∙-β (lookupSV σ x) k (bs //⟨ k ⟩ σ) ⟩
        ⌞ lookupSV σ x ?∙∙⟨ k ⟩ (bs //⟨ k ⟩ σ) ⌟
      ∎
    ⌞⌟-/⟨⟩-β (⊥ ∙ bs) = ⌞∙⌟-/⟨⟩-β ⊥ ⊥ bs ε
    ⌞⌟-/⟨⟩-β (⊤ ∙ bs) = ⌞∙⌟-/⟨⟩-β ⊤ ⊤ bs ε
    ⌞⌟-/⟨⟩-β (Π j b ∙ bs) {k} {σ} = ⌞∙⌟-/⟨⟩-β _ _ bs (begin
        ⌞ Π j b ⌟Hd / toSub σ
      ⟶⋆⟨ →β*-Π (⌞⌟Kd-/⟨⟩-β j) (⌞⌟-/⟨⟩-β b) ⟩
        Π ⌞ j Kind/⟨ k ⟩ σ ⌟Kd ⌞ b /⟨ k ⟩ σ ↑ ⌟
      ∎)
    ⌞⌟-/⟨⟩-β ((a ⇒ b) ∙ bs) {k} {σ} = ⌞∙⌟-/⟨⟩-β _ _ bs (begin
        ⌞ a ⇒ b ⌟Hd / toSub σ
      ⟶⋆⟨ →β*-⇒ (⌞⌟-/⟨⟩-β a) (⌞⌟-/⟨⟩-β b) ⟩
        ⌞ a /⟨ k ⟩ σ ⌟ ⇒ ⌞ b /⟨ k ⟩ σ ⌟
      ∎)
    ⌞⌟-/⟨⟩-β (Λ j b ∙ bs) {k} {σ}  = ⌞∙⌟-/⟨⟩-β _ _ bs (begin
        ⌞ Λ j b ⌟Hd / toSub σ
      ⟶⋆⟨ →β*-Λ (⌞⌟Kd-/⟨⟩-β j) (⌞⌟-/⟨⟩-β b) ⟩
        Λ ⌞ j Kind/⟨ k ⟩ σ ⌟Kd ⌞ b /⟨ k ⟩ σ ↑ ⌟
      ∎)
    ⌞⌟-/⟨⟩-β (ƛ a b ∙ bs) {k} {σ}  = ⌞∙⌟-/⟨⟩-β _ _ bs (begin
        ⌞ ƛ a b ⌟Hd / toSub σ
      ⟶⋆⟨ →β*-ƛ (⌞⌟-/⟨⟩-β a) (⌞⌟-/⟨⟩-β b) ⟩
        ƛ ⌞ a /⟨ k ⟩ σ ⌟ ⌞ b /⟨ k ⟩ σ ↑ ⌟
      ∎)
    ⌞⌟-/⟨⟩-β (a ⊡ b ∙ bs) {k} {σ}  = ⌞∙⌟-/⟨⟩-β _ _ bs (begin
        ⌞ a ⊡ b ⌟Hd / toSub σ
      ⟶⋆⟨ →β*-⊡ (⌞⌟-/⟨⟩-β a) (⌞⌟-/⟨⟩-β b) ⟩
        ⌞ a /⟨ k ⟩ σ ⌟ ⊡ ⌞ b /⟨ k ⟩ σ ⌟
      ∎)

    ⌞⌟Kd-/⟨⟩-β : ∀ {m n} j {k} {σ : SVSub m n} →
                 ⌞ j ⌟Kd Kind/ toSub σ  Kd→β*  ⌞ j Kind/⟨ k ⟩ σ ⌟Kd
    ⌞⌟Kd-/⟨⟩-β (a ⋯ b) {k} {σ} = Kd.begin
        (⌞ a ⋯ b ⌟Kd Kind/ toSub σ)
      Kd.⟶⋆⟨ Kd→β*-⋯ (⌞⌟-/⟨⟩-β a) (⌞⌟-/⟨⟩-β b) ⟩
        ⌞ a /⟨ k ⟩ σ ⌟ ⋯ ⌞ b /⟨ k ⟩ σ ⌟
      Kd.∎
    ⌞⌟Kd-/⟨⟩-β (Π j l) {k} {σ} = Kd.begin
        (⌞ Π j l ⌟Kd Kind/ toSub σ)
      Kd.⟶⋆⟨ Kd→β*-Π (⌞⌟Kd-/⟨⟩-β j) (⌞⌟Kd-/⟨⟩-β l) ⟩
        Π ⌞ j Kind/⟨ k ⟩ σ ⌟Kd ⌞ l Kind/⟨ k ⟩ σ ↑ ⌟Kd
      Kd.∎

    ⌞∙⌟-/⟨⟩-β : ∀ {m n} a b bs {k} {σ : SVSub m n} →
                b / toSub σ →β* a →
                (b ⌞∙⌟ ⌞ bs ⌟Sp) / toSub σ  →β*  a ⌞∙⌟ ⌞ bs //⟨ k ⟩ σ ⌟Sp
    ⌞∙⌟-/⟨⟩-β a b []               hyp = hyp
    ⌞∙⌟-/⟨⟩-β a b (c ∷ cs) {k} {σ} hyp =
      ⌞∙⌟-/⟨⟩-β (a · ⌞ c /⟨ k ⟩ σ ⌟) (b · ⌞ c ⌟) cs
               (→β*-· hyp (⌞⌟-/⟨⟩-β c))

    -- Reducing applications commute with ⌞_⌟ up to β-reduction.

    ⌞⌟-?∙∙-β : ∀ {n} (r : SVRes n) k bs →
               ⌞ toElim r ⌟ ⌞∙⌟ ⌞ bs ⌟Sp →β* ⌞ r ?∙∙⟨ k ⟩ bs ⌟
    ⌞⌟-?∙∙-β (hit a)  k bs = ⌞⌟-∙∙-β a k bs
    ⌞⌟-?∙∙-β (miss y) k bs = ε

    ⌞⌟-∙∙-β : ∀ {n} (a : Elim n) k bs → ⌞ a ⌟ ⌞∙⌟ ⌞ bs ⌟Sp →β* ⌞ a ∙∙⟨ k ⟩ bs ⌟
    ⌞⌟-∙∙-β a k       []       = ε
    ⌞⌟-∙∙-β a ★       (b ∷ bs) = begin
      ⌞ a ⌟ ⌞∙⌟ (⌞ b ⌟ ∷ ⌞ bs ⌟Sp) ≡˘⟨ ⌞⌟-∙∙ a (b ∷ bs) ⟩
      ⌞ a ∙∙ (b ∷ bs) ⌟            ∎
    ⌞⌟-∙∙-β a (j ⇒ k) (b ∷ bs) = begin
        ⌞ a ⌟ ⌞∙⌟ (⌞ b ⌟ ∷ ⌞ bs ⌟Sp)
      ⟶⋆⟨ →β*-⌞∙⌟₁ (⌞⌟-⌜·⌝-β a (j ⇒ k) b) ⌞ bs ⌟Sp  ⟩
        ⌞ a ⌜·⌝⟨ j ⇒ k ⟩ b ⌟ ⌞∙⌟ ⌞ bs ⌟Sp
      ⟶⋆⟨ ⌞⌟-∙∙-β (a ⌜·⌝⟨ j ⇒ k ⟩ b) k bs ⟩
        ⌞ a ⌜·⌝⟨ j ⇒ k ⟩ b ∙∙⟨ k ⟩ bs ⌟
      ∎

    ⌞⌟-⌜·⌝-β : ∀ {n} (a : Elim n) k b → ⌞ a ⌟ · ⌞ b ⌟ →β* ⌞ a ⌜·⌝⟨ k ⟩ b ⌟
    ⌞⌟-⌜·⌝-β a ★ b = begin
      ⌞ a ⌟ · ⌞ b ⌟              ≡˘⟨ ⌞⌟-· a b ⟩
      ⌞ a ⌜·⌝ b ⌟                ∎
    ⌞⌟-⌜·⌝-β (a ∙ (c ∷ cs)) (j ⇒ k) b = begin
      ⌞ a ∙ (c ∷ cs) ⌟ · ⌞ b ⌟   ≡˘⟨ ⌞⌟-· (a ∙ (c ∷ cs)) b ⟩
      ⌞ a ∙ (c ∷ cs) ⌜·⌝ b ⌟     ∎
    ⌞⌟-⌜·⌝-β (var x   ∙ []) (j ⇒ k) b = ε
    ⌞⌟-⌜·⌝-β (⊥       ∙ []) (j ⇒ k) b = ε
    ⌞⌟-⌜·⌝-β (⊤       ∙ []) (j ⇒ k) b = ε
    ⌞⌟-⌜·⌝-β (Π l a   ∙ []) (j ⇒ k) b = ε
    ⌞⌟-⌜·⌝-β ((a ⇒ b) ∙ []) (j ⇒ k) c = ε
    ⌞⌟-⌜·⌝-β (Λ l a ∙ []) (j ⇒ k) b = begin
      Λ ⌞ l ⌟Kd ⌞ a ⌟ · ⌞ b ⌟    ⟶⟨ ⌈ cont-Tp· ⌞ l ⌟Kd ⌞ a ⌟ ⌞ b ⌟ ⌉ ⟩
      ⌞ a ⌟ [ ⌞ b ⌟ ]            ⟶⋆⟨ ⌞⌟-/⟨⟩-β a {j} {sub b} ⟩
      ⌞ a [ b ∈ j ] ⌟            ∎
    ⌞⌟-⌜·⌝-β (ƛ a b   ∙ []) (j ⇒ k) c = ε
    ⌞⌟-⌜·⌝-β (a ⊡ b   ∙ []) (j ⇒ k) c = ε

  -- Potentially reducing applications commute with ⌞_⌟ up to β-reduction.

  ⌞⌟-↓⌜·⌝-β : ∀ {n} (a : Elim n) b → ⌞ a ⌟ · ⌞ b ⌟ →β* ⌞ a ↓⌜·⌝ b ⌟
  ⌞⌟-↓⌜·⌝-β (a ∙ (c ∷ cs)) b = begin
    ⌞ a ∙ (c ∷ cs) ⌟ · ⌞ b ⌟   ≡˘⟨ ⌞⌟-· (a ∙ (c ∷ cs)) b ⟩
    ⌞ a ∙ (c ∷ cs) ⌜·⌝ b ⌟     ∎
  ⌞⌟-↓⌜·⌝-β (var x   ∙ []) b = ε
  ⌞⌟-↓⌜·⌝-β (⊥       ∙ []) b = ε
  ⌞⌟-↓⌜·⌝-β (⊤       ∙ []) b = ε
  ⌞⌟-↓⌜·⌝-β (Π l a   ∙ []) b = ε
  ⌞⌟-↓⌜·⌝-β ((a ⇒ b) ∙ []) c = ε
  ⌞⌟-↓⌜·⌝-β (Λ l a ∙ []) b = begin
    Λ ⌞ l ⌟Kd ⌞ a ⌟ · ⌞ b ⌟    ⟶⟨ ⌈ cont-Tp· ⌞ l ⌟Kd ⌞ a ⌟ ⌞ b ⌟ ⌉ ⟩
    ⌞ a ⌟ [ ⌞ b ⌟ ]            ⟶⋆⟨ ⌞⌟-/⟨⟩-β a {⌊ l ⌋} {sub b} ⟩
    ⌞ a [ b ∈ ⌊ l ⌋ ] ⌟        ∎
  ⌞⌟-↓⌜·⌝-β (ƛ a b   ∙ []) c = ε
  ⌞⌟-↓⌜·⌝-β (a ⊡ b   ∙ []) c = ε

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:
postulate A : Set
postulate B : A → Set
variable a : A

foo : B a → Set
foo x = {!a!} -- WAS: C-c C-c here reports "Not a variable: a"

-- SHOULD instead introduce the hidden argument {a}

{- C-c C-e reports
a : A  (not in scope)
x : B a
-}


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

open import LogicalFormulae
open import Numbers.Naturals.Definition

module Numbers.Integers.Definition where

data ℤ : Set where
  nonneg : ℕ → ℤ
  negSucc : ℕ → ℤ
{-# BUILTIN INTEGER       ℤ       #-}
{-# BUILTIN INTEGERPOS    nonneg  #-}
{-# BUILTIN INTEGERNEGSUC negSucc #-}

nonnegInjective : {a b : ℕ} → nonneg a ≡ nonneg b → a ≡ b
nonnegInjective refl = refl

negSuccInjective : {a b : ℕ} → negSucc a ≡ negSucc b → a ≡ b
negSuccInjective refl = refl

ℤDecideEquality : (a b : ℤ) → ((a ≡ b) || ((a ≡ b) → False))
ℤDecideEquality (nonneg x) (nonneg y) with ℕDecideEquality x y
ℤDecideEquality (nonneg x) (nonneg y) | inl eq = inl (applyEquality nonneg eq)
ℤDecideEquality (nonneg x) (nonneg y) | inr non = inr λ i → non (nonnegInjective i)
ℤDecideEquality (nonneg x) (negSucc y) = inr λ ()
ℤDecideEquality (negSucc x) (nonneg x₁) = inr λ ()
ℤDecideEquality (negSucc x) (negSucc y) with ℕDecideEquality x y
ℤDecideEquality (negSucc x) (negSucc y) | inl eq = inl (applyEquality negSucc eq)
ℤDecideEquality (negSucc x) (negSucc y) | inr non = inr λ i → non (negSuccInjective i)


text:
-- This error never occurs.
module ShouldBeASort where

err = ShouldBeASort-Never-Occurs


text:
------------------------------------------------------------------------
-- Some theory of Erased, developed using the K rule and propositional
-- equality
------------------------------------------------------------------------

-- This module instantiates and reexports code from Erased.

{-# OPTIONS --with-K --safe #-}

module Erased.With-K where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Embedding equality-with-J as Emb using (Is-embedding)
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
import Erased.Basics as EB
import Erased.Level-1 equality-with-J as E
open import H-level equality-with-J
open import Injection equality-with-J using (Injective)

private
  variable
    a b p : Level
    A     : Type a

------------------------------------------------------------------------
-- Code related to the module Erased

-- Given an erased proof of equality of x and y one can show that
-- [ x ] is equal to [ y ].

[]-cong : {@0 A : Type a} {@0 x y : A} →
          EB.Erased (x ≡ y) → EB.[ x ] ≡ EB.[ y ]
[]-cong EB.[ refl ] = refl

-- []-cong is an equivalence.

[]-cong-equivalence :
  {@0 A : Type a} {@0 x y : A} →
  Is-equivalence ([]-cong {x = x} {y = y})
[]-cong-equivalence {x = x} {y = y} = _≃_.is-equivalence (Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = []-cong
      ; from = λ eq → EB.[ cong EB.erased eq ]
      }
    ; right-inverse-of = λ { refl → refl }
    }
  ; left-inverse-of = λ { EB.[ refl ] → refl }
  }))

-- []-cong maps [ refl ] to refl (by definition).

[]-cong-[refl] :
  {@0 A : Type a} {@0 x : A} →
  []-cong EB.[ refl {x = x} ] ≡ refl {x = EB.[ x ]}
[]-cong-[refl] = refl

-- The []-cong axioms can be instantiated.

instance-of-[]-cong-axiomatisation : E.[]-cong-axiomatisation a
instance-of-[]-cong-axiomatisation = λ where
  .E.[]-cong-axiomatisation.[]-cong             → []-cong
  .E.[]-cong-axiomatisation.[]-cong-equivalence → []-cong-equivalence
  .E.[]-cong-axiomatisation.[]-cong-[refl]      → []-cong-[refl]

-- Some reexported definitions.

open import Erased equality-with-J instance-of-[]-cong-axiomatisation
  public
  hiding ([]-cong; []-cong-equivalence; []-cong-[refl]; Injective-[];
          Π-Erased≃Π0[]; Π-Erased≃Π0)

------------------------------------------------------------------------
-- Other code

-- [_]→ is injective.

Injective-[] : {@0 A : Type a} → Injective [ A ∣_]→
Injective-[] refl = refl

-- [_]→ is an embedding.

Is-embedding-[] : {@0 A : Type a} → Is-embedding [ A ∣_]→
Is-embedding-[] _ _ =
    (λ { refl → refl })
  , (λ { refl → refl })
  , (λ { refl → refl })
  , (λ { refl → refl })

-- If Erased A is a proposition, then A is a proposition.

Is-proposition-Erased→Is-proposition :
  {@0 A : Type a} →
  Is-proposition (Erased A) → Is-proposition A
Is-proposition-Erased→Is-proposition prop x y =
  Injective-[] (prop [ x ] [ y ])

-- A variant of the previous result.

H-level′-1-Erased→H-level′-1 :
  {@0 A : Type a} →
  H-level′ 1 (Erased A) → H-level′ 1 A
H-level′-1-Erased→H-level′-1 prop x y
  with proj₁ (prop [ x ] [ y ])
... | refl = refl , λ { refl → refl }

-- Equality is always very stable.

Very-stable-≡-trivial : Very-stable-≡ A
Very-stable-≡-trivial =
  _⇔_.from (Very-stable-≡↔Is-embedding-[] _)
           Is-embedding-[]

-- The following four results are inspired by a result in
-- Mishra-Linger's PhD thesis (see Section 5.4.1).

-- There is a bijection between (x : Erased A) → P x and
-- (@0 x : A) → P [ x ].

Π-Erased↔Π0[] :
  {@0 A : Type a} {@0 P : Erased A → Type p} →
  ((x : Erased A) → P x) ↔ ((@0 x : A) → P [ x ])
Π-Erased↔Π0[] = record
  { surjection = record
    { logical-equivalence = Π-Erased⇔Π0
    ; right-inverse-of = λ _ → refl
    }
  ; left-inverse-of = λ _ → refl
  }

-- There is an equivalence between (x : Erased A) → P x and
-- (@0 x : A) → P [ x ].
--
-- This is not proved by converting Π-Erased↔Π0[] to an equivalence,
-- because the type arguments of the conversion function in
-- Equivalence are not erased, and P can only be used in erased
-- contexts.
--
-- This is a strengthening of E.Π-Erased≃Π0[].

Π-Erased≃Π0[] :
  {@0 A : Type a} {@0 P : Erased A → Type p} →
  ((x : Erased A) → P x) ≃ ((@0 x : A) → P [ x ])
Π-Erased≃Π0[] = record
  { to             = λ f x → f [ x ]
  ; is-equivalence =
        (λ f ([ x ]) → f x)
      , (λ _ → refl)
      , (λ _ → refl)
      , (λ _ → refl)
  }

-- There is a bijection between (x : Erased A) → P (erased x) and
-- (@0 x : A) → P x.

Π-Erased↔Π0 :
  {@0 A : Type a} {@0 P : A → Type p} →
  ((x : Erased A) → P (erased x)) ↔ ((@0 x : A) → P x)
Π-Erased↔Π0 = Π-Erased↔Π0[]

-- There is an equivalence between (x : Erased A) → P (erased x) and
-- (@0 x : A) → P x.
--
-- This is a strengthening of E.Π-Erased≃Π0.

Π-Erased≃Π0 :
  {@0 A : Type a} {@0 P : A → Type p} →
  ((x : Erased A) → P (erased x)) ≃ ((@0 x : A) → P x)
Π-Erased≃Π0 = Π-Erased≃Π0[]

private

  -- As an aside it is possible to prove the four previous results
  -- without relying on eta-equality for Erased. However, the code
  -- makes use of extensionality, and it also makes use of
  -- eta-equality for Π. (The use of η-equality for Π could perhaps be
  -- avoided, but Agda does not, at the time of writing, provide a
  -- simple way to turn off this kind of η-equality.)

  data Erased-no-η (@0 A : Type a) : Type a where
    [_] : @0 A → Erased-no-η A

  @0 erased-no-η : Erased-no-η A → A
  erased-no-η [ x ] = x

  -- Some lemmas.

  Π-Erased-no-η→Π0[] :
    {@0 A : Type a} {@0 P : Erased-no-η A → Type p} →
    ((x : Erased-no-η A) → P x) → (@0 x : A) → P [ x ]
  Π-Erased-no-η→Π0[] f x = f [ x ]

  Π0[]→Π-Erased-no-η :
    {@0 A : Type a} (@0 P : Erased-no-η A → Type p) →
    ((@0 x : A) → P [ x ]) → (x : Erased-no-η A) → P x
  Π0[]→Π-Erased-no-η _ f [ x ] = f x

  Π0[]→Π-Erased-no-η-Π-Erased-no-η→Π0[] :
    {@0 A : Type a} {@0 P : Erased-no-η A → Type p}
    (f : (x : Erased-no-η A) → P x) (x : Erased-no-η A) →
    Π0[]→Π-Erased-no-η P (Π-Erased-no-η→Π0[] f) x ≡ f x
  Π0[]→Π-Erased-no-η-Π-Erased-no-η→Π0[] f [ x ] = refl

  -- There is a bijection between (x : Erased-no-η A) → P x and
  -- (@0 x : A) → P [ x ] (assuming extensionality).

  Π-Erased-no-η↔Π0[] :
    {@0 A : Type a} {@0 P : Erased-no-η A → Type p} →
    Extensionality′ (Erased-no-η A) P →
    ((x : Erased-no-η A) → P x) ↔ ((@0 x : A) → P [ x ])
  Π-Erased-no-η↔Π0[] {P = P} ext = record
    { surjection = record
      { logical-equivalence = record
        { to   = Π-Erased-no-η→Π0[]
        ; from = Π0[]→Π-Erased-no-η _
        }
      ; right-inverse-of    = λ _ → refl
      }
    ; left-inverse-of = λ f →
        ext (Π0[]→Π-Erased-no-η-Π-Erased-no-η→Π0[] f)
    }

  -- There is an equivalence between (x : Erased-no-η A) → P x and
  -- (@0 x : A) → P [ x ] (assuming extensionality).
  --
  -- This is not proved by converting Π-Erased-no-η↔Π0[] to an
  -- equivalence, because the type arguments of the conversion
  -- function in Equivalence are not erased, and A and P can only be
  -- used in erased contexts.

  Π-Erased-no-η≃Π0[] :
    {@0 A : Type a} {@0 P : Erased-no-η A → Type p} →
    Extensionality′ (Erased-no-η A) P →
    ((x : Erased-no-η A) → P x) ≃ ((@0 x : A) → P [ x ])
  Π-Erased-no-η≃Π0[] {A = A} {P = P} ext = record
    { to             = λ f x → f [ x ]
    ; is-equivalence =
          Π0[]→Π-Erased-no-η _
        , (λ _ → refl)
        , (λ f → ext (Π0[]→Π-Erased-no-η-Π-Erased-no-η→Π0[] f))
        , (λ _ → uip _ _)
    }
    where
    uip : {@0 B : Type b} {@0 x y : B} (@0 p q : x ≡ y) → p ≡ q
    uip refl refl = refl

  -- There is a bijection between
  -- (x : Erased-no-η A) → P (erased-no-η x) and (@0 x : A) → P x
  -- (assuming extensionality).

  Π-Erased-no-η↔Π0 :
    {@0 A : Type a} {@0 P : A → Type p} →
    Extensionality′ (Erased-no-η A) (P ∘ erased-no-η) →
    ((x : Erased-no-η A) → P (erased-no-η x)) ↔ ((@0 x : A) → P x)
  Π-Erased-no-η↔Π0 = Π-Erased-no-η↔Π0[]

  -- There is an equivalence between
  -- (x : Erased-no-η A) → P (erased-no-η x) and (@0 x : A) → P x
  -- (assuming extensionality).

  Π-Erased-no-η≃Π0 :
    {@0 A : Type a} {@0 P : A → Type p} →
    Extensionality′ (Erased-no-η A) (P ∘ erased-no-η) →
    ((x : Erased-no-η A) → P (erased-no-η x)) ≃ ((@0 x : A) → P x)
  Π-Erased-no-η≃Π0 = Π-Erased-no-η≃Π0[]

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2015-02-07

-- {-# OPTIONS -v tc.with:40 #-}

open import Common.Prelude hiding (not)

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

T : Bool → Set → Set
T true  A = A → A
T false A = Bool

test : (b : Bool) → (A : Set) → T (not b) A
test b with not b
test b | true   = λ A a → a
test b | false  = λ A → false

-- should be able to abstract (not b) under Binder (A : Set)
-- and succeed


text:
import      Lvl
open import Type

module Data.List.Relation.Sublist {ℓ} {T : Type{ℓ}} where

open import Data.List using (List ; ∅ ; _⊰_)
open import Logic

-- Whether a list's elements are contained in another list in order.
-- Examples:
--   [1,2,3] ⊑ [1,2,3]
--   [1,2,3] ⊑ [1,2,3,4]
--   [1,2,3] ⊑ [0,1,2,3]
--   [1,2,3] ⊑ [0,1,10,2,20,3,30]
--   [0,10,20,30] ⊑ [0,1,10,2,20,3,30]
data _⊑_ : List(T) → List(T) → Stmt{ℓ} where
  empty : (∅ ⊑ ∅)
  use   : ∀{x}{l₁ l₂} → (l₁ ⊑ l₂) → ((x ⊰ l₁) ⊑ (x ⊰ l₂))
  skip  : ∀{x}{l₁ l₂} → (l₁ ⊑ l₂) → (l₁       ⊑ (x ⊰ l₂))

-- Whether a list's elements are contained in another list in order while not containing the same sublist.
-- Examples:
--   [1,2,3] ⊏ [1,2,3,4]
--   [1,2,3] ⊏ [0,1,2,3]
--   [1,2,3] ⊏ [0,1,10,2,20,3,30]
data _⊏_ : List(T) → List(T) → Stmt{ℓ} where
  use   : ∀{x}{l₁ l₂} → (l₁ ⊏ l₂) → ((x ⊰ l₁) ⊏ (x ⊰ l₂))
  skip  : ∀{x}{l₁ l₂} → (l₁ ⊑ l₂) → (l₁       ⊏ (x ⊰ l₂))