text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Restriction.Instance.PartialFunctions where

-- The Category of partial functions is a restriction category

-- The proof is straightforward in the sense that it's all unwinding definitions,
-- but also no-trivial in that they need to be unwound with care (a lot of
-- case analyses with 'with' and inspect is used a lot).

open import Data.Maybe using (Maybe; map; just; nothing; _>>=_)
open import Data.Maybe.Properties
open import Function using (const)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; inspect; [_])

open import Categories.Category.Core using (Category)
open import Categories.Category.Instance.PartialFunctions using (PartialFunctions)
open import Categories.Category.Restriction using (Restriction)

private
  variable
    o : Level
    A B C : Set o

Restriction-PF : ∀ {o} → Restriction (PartialFunctions o)
Restriction-PF {o} = record
  { _↓ = λ f x → map (const x) (f x)
  ; pidʳ = pidʳ
  ; ↓-comm = λ {_} {_} {_} {g} {f} → ↓-comm {g = g} {f}
  ; ↓-denestʳ = λ {_} {_} {_} {f} {g} → ↓-denestʳ {f = f} {g}
  ; ↓-skew-comm = λ {_} {_} {_} {g} {f} → ↓-skew-comm {g = g} {f}
  ; ↓-cong = ↓-cong
  }
  where
    open Category (PartialFunctions o)
    _↓ : (A → Maybe B) → (A → Maybe A)
    _↓ = λ f x → map (const x) (f x)

    pidʳ : {f : A → Maybe B} → f ∘ f ↓ ≈ f
    pidʳ {f = f} x with f x | inspect f x
    ... | just z | [ eq ] = eq
    ... | nothing | _ = refl

    ↓-comm : {g : A → Maybe C} {f : A → Maybe B} → g ↓ ∘ f ↓ ≈ f ↓ ∘ g ↓
    ↓-comm {g = g} {f} x with f x | g x | inspect f x | inspect g x
    ... | just b | just b′  | [ fx=jb ] | [ gx=jb′ ] rewrite fx=jb | gx=jb′ = refl
    ... | just b | nothing  | _         | [ eq ]     rewrite eq = refl
    ... | nothing | just b′ | [ eq ]    | _          rewrite eq = refl
    ... | nothing | nothing | _         | _                     = refl

    ↓-denestʳ : {A B C : Obj} {f : A ⇒ B} {g : A ⇒ C} → (g ∘ f ↓) ↓ ≈ g ↓ ∘ f ↓
    ↓-denestʳ {f = f} a with f a
    ... | just b  = refl
    ... | nothing = refl

    ↓-skew-comm : {A B C : Obj} {g : A ⇒ B} {f : C ⇒ A} → g ↓ ∘ f ≈ f ∘ (g ∘ f) ↓
    ↓-skew-comm {g = g} {f = f} a with f a | inspect f a
    ... | just b | [ eq ] with g b
    ... | just c = sym eq
    ... | nothing = refl
    ↓-skew-comm _ | nothing | _ = refl

    ↓-cong : {A B : Obj} {f g : A ⇒ B} → f ≈ g → f ↓ ≈ g ↓
    ↓-cong eq a rewrite eq a = refl

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Data.Maybe.Sugar where

open import Prelude
open import Data.Maybe

infixl 4 _<*>_
_>>=_ : 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)

_>>_ : Maybe A → Maybe B → Maybe B
nothing >> _ = nothing
just _  >> y = y

guard : Bool → Maybe ⊤
guard false = nothing
guard true  = just tt

_<|>_ : Maybe A → Maybe A → Maybe A
nothing     <|> ys = ys
xs@(just _) <|> _ = xs

ext: agda

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Universe where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓ≅A ℓB ℓ≅B ℓ≅ᴰ : Level

-- Universes and equivalences form a URGStr
𝒮-universe : URGStr (Type ℓ) ℓ
𝒮-universe
  = make-𝒮 {_≅_ = _≃_}
            idEquiv
            λ A → isContrRespectEquiv (Σ-cong-equiv-snd (λ A' → isoToEquiv (equivInv A' A)))
                                       (equivContr' A)
  where
    module _ (A : Type ℓ) where
      equivInv : (A' : Type ℓ) → Iso (A ≃ A') (A' ≃ A)
      Iso.fun (equivInv A') = invEquiv
      Iso.inv (equivInv A') = invEquiv
      Iso.leftInv (equivInv A') = λ e → equivEq (invEquiv (invEquiv e)) e (funExt (λ x → refl))
      Iso.rightInv (equivInv A') = λ e → equivEq (invEquiv (invEquiv e)) e (funExt (λ x → refl))
      equivContr' : isContr (Σ[ A' ∈ Type ℓ ] A' ≃ A)
      equivContr' = EquivContr A

𝒮ᴰ-pointed : {ℓ : Level} → URGStrᴰ (𝒮-universe {ℓ}) (λ A → A) ℓ
𝒮ᴰ-pointed {ℓ} =
  make-𝒮ᴰ (λ a e b → equivFun e a ≡ b)
          (λ _ → refl)
          p
          where
            p : (A : Type ℓ) (a : A) → isContr (Σ[ b ∈ A ] a ≡ b)
            p _ a = isContrSingl a

𝒮-pointed : {ℓ : Level} → URGStr (Σ[ A ∈ Type ℓ ] A) ℓ
𝒮-pointed = ∫⟨ 𝒮-universe ⟩ 𝒮ᴰ-pointed

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Property related to Grouped
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Grouped.Properties where

open import Data.Bool using (true; false)
open import Data.List
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.All.Properties as All
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.Grouped
open import Function using (_∘_; _⇔_; Equivalence)
open import Function.Equality using (_⟨$⟩_)
open import Relation.Binary as B using (REL; Rel)
open import Relation.Unary as U using (Pred)
open import Relation.Nullary using (¬_; does; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Level

private
  variable
    a b c p q : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- map

module _ (P : Rel A p) (Q : Rel B q) where

  map⁺ : ∀ {f xs} → (∀ {x y} → P x y ⇔ Q (f x) (f y)) → Grouped P xs → Grouped Q (map f xs)
  map⁺ {f} {[]} P⇔Q [] = []
  map⁺ {f} {x ∷ xs} P⇔Q (all[¬Px,xs] ∷≉ g) = aux all[¬Px,xs] ∷≉ map⁺ P⇔Q g where
    aux : ∀ {ys} → All (λ y → ¬ P x y) ys → All (λ y → ¬ Q (f x) y) (map f ys)
    aux [] = []
    aux (py ∷ pys) = py ∘ Equivalence.g P⇔Q ∷ aux pys
  map⁺ {f} {x₁ ∷ x₂ ∷ xs} P⇔Q (Px₁x₂ ∷≈ g) = Equivalence.f P⇔Q Px₁x₂ ∷≈ map⁺ P⇔Q g

  map⁻ : ∀ {f xs} → (∀ {x y} → P x y ⇔ Q (f x) (f y)) → Grouped Q (map f xs) → Grouped P xs
  map⁻ {f} {[]} P⇔Q [] = []
  map⁻ {f} {x ∷ []} P⇔Q ([] ∷≉ []) = [] ∷≉ []
  map⁻ {f} {x₁ ∷ x₂ ∷ xs} P⇔Q (all[¬Qx,xs] ∷≉ g) = aux all[¬Qx,xs] ∷≉ map⁻ P⇔Q g where
    aux : ∀ {ys} → All (λ y → ¬ Q (f x₁) y) (map f ys) → All (λ y → ¬ P x₁ y) ys
    aux {[]} [] = []
    aux {y ∷ ys} (py ∷ pys) = py ∘ Equivalence.f P⇔Q ∷ aux pys
  map⁻ {f} {x₁ ∷ x₂ ∷ xs} P⇔Q (Qx₁x₂ ∷≈ g) = Equivalence.g P⇔Q Qx₁x₂ ∷≈ map⁻ P⇔Q g

------------------------------------------------------------------------
-- [_]

module _ (P : Rel A p) where

  [_]⁺ : ∀ x → Grouped P [ x ]
  [_]⁺ x = [] ∷≉ []

------------------------------------------------------------------------
-- derun

module _ {P : Rel A p} (P? : B.Decidable P) where

  grouped[xs]⇒unique[derun[xs]] : ∀ xs → Grouped P xs → AllPairs (λ x y → ¬ P x y) (derun P? xs)
  grouped[xs]⇒unique[derun[xs]] [] [] = []
  grouped[xs]⇒unique[derun[xs]] (x ∷ []) ([] ∷≉ []) = [] ∷ []
  grouped[xs]⇒unique[derun[xs]] (x ∷ y ∷ xs) (all[¬Px,y∷xs]@(¬Pxy ∷ _) ∷≉ grouped[y∷xs]) with P? x y
  ... | yes Pxy  = contradiction Pxy ¬Pxy
  ... | no  _    = All.derun⁺ P? all[¬Px,y∷xs] ∷ grouped[xs]⇒unique[derun[xs]] (y ∷ xs) grouped[y∷xs]
  grouped[xs]⇒unique[derun[xs]] (x ∷ y ∷ xs) (Pxy ∷≈ grouped[xs]) with P? x y
  ... | yes _    = grouped[xs]⇒unique[derun[xs]] (y ∷ xs) grouped[xs]
  ... | no  ¬Pxy = contradiction Pxy ¬Pxy


text:
------------------------------------------------------------------------------
-- Properties related with the forest type
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Forest.PropertiesATP where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesATP using ( ∷-rightCong )
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesATP
  using ( ++-leftIdentity
        ; mapCong₂
        ; ++-leftCong
        ; reverse-[x]≡[x]
        )
open import FOTC.Program.Mirror.Forest.TotalityATP
open import FOTC.Program.Mirror.Type

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

++-rightIdentity : ∀ {xs} → Forest xs → xs ++ [] ≡ xs
++-rightIdentity fnil = ++-leftIdentity []
++-rightIdentity (fcons {x} {xs} Tx Fxs) =
  prf (++-rightIdentity Fxs)
  where postulate prf : xs ++ [] ≡ xs → (x ∷ xs) ++ [] ≡ x ∷ xs
        {-# ATP prove prf #-}

++-assoc : ∀ {xs} → Forest xs → ∀ ys zs → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc fnil ys zs = prf
  where postulate prf : ([] ++ ys) ++ zs ≡ [] ++ ys ++ zs
        {-# ATP prove prf #-}

++-assoc (fcons {x} {xs} Tx Fxs) ys zs = prf (++-assoc Fxs ys zs)
  where postulate prf : (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs →
                        ((x ∷ xs) ++ ys) ++ zs ≡ (x ∷ xs) ++ ys ++ zs
        {-# ATP prove prf #-}

-- We don't use an automatic proof, because it is necessary to erase a
-- proof term which we don't know how to erase.
map-++ : ∀ f {xs} → (∀ {x} → Tree x → Tree (f · x)) →
         Forest xs →
         ∀ ys → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f h fnil ys =
  map f ([] ++ ys)
    ≡⟨ mapCong₂ (++-leftIdentity ys) ⟩
  map f ys
    ≡⟨ sym (++-leftIdentity (map f ys)) ⟩
  [] ++ map f ys
     ≡⟨ ++-leftCong (sym (map-[] f)) ⟩
  map f [] ++ map f ys ∎

map-++ f h (fcons {x} {xs} Tx Fxs) ys =
  map f ((x ∷ xs) ++ ys)
    ≡⟨ mapCong₂ (++-∷ x xs ys) ⟩
  map f (x ∷ xs ++ ys)
    ≡⟨ map-∷ f x (xs ++ ys) ⟩
  f · x ∷ map f (xs ++ ys)
    ≡⟨ ∷-rightCong (map-++ f h Fxs ys) ⟩
  f · x ∷ (map f xs ++ map f ys)
    ≡⟨ sym (++-∷ (f · x) (map f xs) (map f ys)) ⟩
  (f · x ∷ map f xs) ++ map f ys
     ≡⟨ ++-leftCong (sym (map-∷ f x xs)) ⟩
  map f (x ∷ xs) ++ map f ys ∎

rev-++ : ∀ {xs} → Forest xs → ∀ ys → rev xs ys ≡ rev xs [] ++ ys
rev-++ fnil ys = prf
  where postulate prf : rev [] ys ≡ rev [] [] ++ ys
        {-# ATP prove prf #-}

rev-++ (fcons {x} {xs} Tx Fxs) ys =
  prf (rev-++ Fxs (x ∷ ys))
      (rev-++ Fxs (x ∷ []))
  where postulate prf : rev xs (x ∷ ys) ≡ rev xs [] ++ x ∷ ys →
                        rev xs (x ∷ []) ≡ rev xs [] ++ x ∷ [] →
                        rev (x ∷ xs) ys ≡ rev (x ∷ xs) [] ++ ys
        {-# ATP prove prf ++-assoc rev-Forest #-}

reverse-++ : ∀ {xs ys} → Forest xs → Forest ys →
             reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ {ys = ys} fnil Fys = prf
  where postulate prf : reverse ([] ++ ys) ≡ reverse ys ++ reverse []
        {-# ATP prove prf ++-rightIdentity reverse-Forest #-}

reverse-++ (fcons {x} {xs} Tx Fxs) fnil = prf
  where
  postulate prf : reverse ((x ∷ xs) ++ []) ≡ reverse [] ++ reverse (x ∷ xs)
  {-# ATP prove prf ++-rightIdentity #-}

reverse-++ (fcons {x} {xs} Tx Fxs) (fcons {y} {ys} Ty Fys) =
  prf (reverse-++ Fxs (fcons Ty Fys))
  where
  postulate prf : reverse (xs ++ y ∷ ys) ≡ reverse (y ∷ ys) ++
                                           reverse xs →
                  reverse ((x ∷ xs) ++ y ∷ ys) ≡ reverse (y ∷ ys) ++
                                                 reverse (x ∷ xs)
  {-# ATP prove prf reverse-Forest ++-Forest rev-++ ++-assoc #-}

reverse-∷ : ∀ {x ys} → Tree x → Forest ys →
            reverse (x ∷ ys) ≡ reverse ys ++ (x ∷ [])
reverse-∷ {x} Tx fnil = prf
  where postulate prf : reverse (x ∷ []) ≡ reverse [] ++ x ∷ []
        {-# ATP prove prf #-}

reverse-∷ {x} Tx (fcons {y} {ys} Ty Fys) = prf
  where postulate prf : reverse (x ∷ y ∷ ys) ≡ reverse (y ∷ ys) ++ x ∷ []
        {-# ATP prove prf reverse-[x]≡[x] reverse-++ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some theory for commutative semigroup
------------------------------------------------------------------------

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

open import Algebra using (CommutativeSemigroup)

module Algebra.Properties.CommutativeSemigroup
  {a ℓ} (CS : CommutativeSemigroup a ℓ)
  where

open CommutativeSemigroup CS

open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------------
-- Re-export the contents of semigroup

open import Algebra.Properties.Semigroup semigroup public

------------------------------------------------------------------------------
-- Permutation laws for _∙_ for three factors.

------------------------------------------------------------------------------
-- Partitions (1,1).
-- There are five nontrivial permutations.
------------------------------------------------------------------------------

x∙yz≈y∙xz :  ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (x ∙ z)
x∙yz≈y∙xz x y z = begin
  x ∙ (y ∙ z)    ≈⟨ sym (assoc x y z) ⟩
  (x ∙ y) ∙ z    ≈⟨ ∙-congʳ (comm x y) ⟩
  (y ∙ x) ∙ z    ≈⟨ assoc y x z ⟩
  y ∙ (x ∙ z)    ∎

x∙yz≈z∙yx :  ∀ x y z → x ∙ (y ∙ z) ≈ z ∙ (y ∙ x)
x∙yz≈z∙yx x y z = begin
  x ∙ (y ∙ z)    ≈⟨ ∙-congˡ (comm y z) ⟩
  x ∙ (z ∙ y)    ≈⟨ x∙yz≈y∙xz x z y ⟩
  z ∙ (x ∙ y)    ≈⟨ ∙-congˡ (comm x y) ⟩
  z ∙ (y ∙ x)    ∎

x∙yz≈x∙zy :  ∀ x y z → x ∙ (y ∙ z) ≈ x ∙ (z ∙ y)
x∙yz≈x∙zy _ y z =  ∙-congˡ (comm y z)

x∙yz≈y∙zx :  ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (z ∙ x)
x∙yz≈y∙zx x y z = begin
  x ∙ (y ∙ z)   ≈⟨ comm x _ ⟩
  (y ∙ z) ∙ x   ≈⟨ assoc y z x ⟩
  y ∙ (z ∙ x)   ∎

x∙yz≈z∙xy :  ∀ x y z → x ∙ (y ∙ z) ≈ z ∙ (x ∙ y)
x∙yz≈z∙xy x y z = begin
  x ∙ (y ∙ z)   ≈⟨ sym (assoc x y z) ⟩
  (x ∙ y) ∙ z   ≈⟨ comm _ z ⟩
  z ∙ (x ∙ y)   ∎

------------------------------------------------------------------------------
-- Partitions (1,2).
-- These permutation laws are proved by composing the proofs for
-- partitions (1,1) with  \p → trans p (sym (assoc _ _ _)).
------------------------------------------------------------------------------

x∙yz≈yx∙z :  ∀ x y z → x ∙ (y ∙ z) ≈ (y ∙ x) ∙ z
x∙yz≈yx∙z x y z =  trans (x∙yz≈y∙xz x y z) (sym (assoc y x z))

x∙yz≈zy∙x :  ∀ x y z → x ∙ (y ∙ z) ≈ (z ∙ y) ∙ x
x∙yz≈zy∙x x y z =  trans (x∙yz≈z∙yx x y z) (sym (assoc z y x))

x∙yz≈xz∙y :  ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ z) ∙ y
x∙yz≈xz∙y x y z =  trans (x∙yz≈x∙zy x y z) (sym (assoc x z y))

x∙yz≈yz∙x :  ∀ x y z → x ∙ (y ∙ z) ≈ (y ∙ z) ∙ x
x∙yz≈yz∙x x y z =  trans (x∙yz≈y∙zx _ _ _) (sym (assoc y z x))

x∙yz≈zx∙y :  ∀ x y z → x ∙ (y ∙ z) ≈ (z ∙ x) ∙ y
x∙yz≈zx∙y x y z =  trans (x∙yz≈z∙xy x y z) (sym (assoc z x y))

------------------------------------------------------------------------------
-- Partitions (2,1).
-- Their laws are proved by composing proofs for partitions (1,1) with
-- trans (assoc x y z).
------------------------------------------------------------------------------

xy∙z≈y∙xz :  ∀ x y z → (x ∙ y) ∙ z ≈ y ∙ (x ∙ z)
xy∙z≈y∙xz x y z =  trans (assoc x y z) (x∙yz≈y∙xz x y z)

xy∙z≈z∙yx :  ∀ x y z → (x ∙ y) ∙ z ≈ z ∙ (y ∙ x)
xy∙z≈z∙yx x y z =  trans (assoc x y z) (x∙yz≈z∙yx x y z)

xy∙z≈x∙zy :  ∀ x y z → (x ∙ y) ∙ z ≈ x ∙ (z ∙ y)
xy∙z≈x∙zy x y z =  trans (assoc x y z) (x∙yz≈x∙zy x y z)

xy∙z≈y∙zx :  ∀ x y z → (x ∙ y) ∙ z ≈ y ∙ (z ∙ x)
xy∙z≈y∙zx x y z =  trans (assoc x y z) (x∙yz≈y∙zx x y z)

xy∙z≈z∙xy :  ∀ x y z → (x ∙ y) ∙ z ≈ z ∙ (x ∙ y)
xy∙z≈z∙xy x y z =  trans (assoc x y z) (x∙yz≈z∙xy x y z)

------------------------------------------------------------------------------
-- Partitions (2,2).
-- These proofs are by composing with the proofs for (2,1).
------------------------------------------------------------------------------

xy∙z≈yx∙z :  ∀ x y z → (x ∙ y) ∙ z ≈ (y ∙ x) ∙ z
xy∙z≈yx∙z x y z =  trans (xy∙z≈y∙xz _ _ _) (sym (assoc y x z))

xy∙z≈zy∙x :  ∀ x y z → (x ∙ y) ∙ z ≈ (z ∙ y) ∙ x
xy∙z≈zy∙x x y z =  trans (xy∙z≈z∙yx x y z) (sym (assoc z y x))

xy∙z≈xz∙y :  ∀ x y z → (x ∙ y) ∙ z ≈ (x ∙ z) ∙ y
xy∙z≈xz∙y x y z =  trans (xy∙z≈x∙zy x y z) (sym (assoc x z y))

xy∙z≈yz∙x :  ∀ x y z → (x ∙ y) ∙ z ≈ (y ∙ z) ∙ x
xy∙z≈yz∙x x y z =  trans (xy∙z≈y∙zx x y z) (sym (assoc y z x))

xy∙z≈zx∙y :  ∀ x y z → (x ∙ y) ∙ z ≈ (z ∙ x) ∙ y
xy∙z≈zx∙y x y z =  trans (xy∙z≈z∙xy x y z) (sym (assoc z x y))


text:
open import Relation.Binary.Core

module TreeSort.Impl2  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import BBSTree _≤_
open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List
open import Data.Sum

insert : {x : A}{b t : Bound} → LeB b (val x) → LeB (val x) t → BBSTree b t → BBSTree b t
insert b≤x x≤t (bslf _) = bsnd b≤x x≤t (bslf b≤x) (bslf x≤t)
insert {x = x} b≤x x≤t (bsnd {x = y} b≤y y≤t l r)
    with tot≤ x y
... | inj₁ x≤y = bsnd b≤y y≤t (insert b≤x (lexy x≤y) l) r
... | inj₂ y≤x = bsnd b≤y y≤t l (insert (lexy y≤x) x≤t r)

treeSort : List A → BBSTree bot top
treeSort [] = bslf lebx
treeSort (x ∷ xs) = insert {x = x} lebx lext (treeSort xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import Oscar.Prelude
open import Oscar.Class.Successor₀
open import Oscar.Class.Successor₁
open import Oscar.Class.Injectivity
open import Oscar.Class.Pure

module Oscar.Class.Thickandthin where

module _
  {x} {X : Ø x} {a} (A : X → Ø a) {b} (B : X → Ø b)
  where
  record [𝓣hin] : Ø₀ where
    no-eta-equality
    constructor ∁
  module _
    ⦃ _ : 𝓢uccessor₀ X ⦄
    where
    𝔱hin : ∀ (m : X) → A (⇑₀ m) → B m → Ø b
    𝔱hin m = λ _ _ → B (⇑₀ m)
    𝓽hin = ∀ {m : X} → A (⇑₀ m) → B m → B (⇑₀ m)
    record 𝓣hin ⦃ _ : [𝓣hin] ⦄ : Ø x ∙̂ a ∙̂ b where
      field
        thin : 𝓽hin
      instance `𝓘njection₂ : ∀ {m} → 𝓘njection₂ (𝔱hin m)
      `𝓘njection₂ = ∁ thin
open 𝓣hin ⦃ … ⦄ public

module _
  {x} {X : Ø x} {a} (A : X → Ø a) {b} (B : X → Ø b)
  where
  record [𝓣hick] : Ø₀ where
    no-eta-equality
    constructor ∁
  module _
    ⦃ _ : 𝓢uccessor₀ X ⦄
    where
    𝓽hick = ∀ {m} → A m → B (⇑₀ m) → B m
    record 𝓣hick ⦃ _ : [𝓣hick] ⦄ : Ø x ∙̂ a ∙̂ b where field thick : 𝓽hick
open 𝓣hick ⦃ … ⦄ public

module _
  {x} {X : Ø x}
  {a} (A : X → Ø a)
  {b} (B : X → Ø b)
  {ℓ} (_≈_ : ∀ {x} → B x → B x → Ø ℓ)
  where
  record [𝓣hick/thin=1] : Ø₀ where
    no-eta-equality
    constructor ∁
  module _
    ⦃ _ : 𝓢uccessor₀ X ⦄
    ⦃ _ : [𝓢uccessor₁] A ⦄
    ⦃ _ : 𝓢uccessor₁ A ⦄
    ⦃ _ : [𝓣hin] A B ⦄
    ⦃ _ : 𝓣hin A B ⦄
    ⦃ _ : [𝓣hick] A B ⦄
    ⦃ _ : 𝓣hick A B ⦄
    where
    𝓽hick/thin=1 = ∀ {m} (x : A m) (y : B m) → thick x (thin (⇑₁ x) y) ≈ y
    record 𝓣hick/thin=1 : Ø x ∙̂ a ∙̂ b ∙̂ ℓ where field thick/thin=1 : 𝓽hick/thin=1
open 𝓣hick/thin=1 ⦃ … ⦄ public

module _
  {x} {X : Ø x}
  {a} (A : X → Ø a)
  {b} (B : X → Ø b)
  {c} (C : Ø b → Ø c)
  where
  record [𝓒heck] : Ø₀ where
    no-eta-equality
    constructor ∁
  module _
    ⦃ _ : 𝓢uccessor₀ X ⦄
    where
    𝓬heck = ∀ {m} → A (⇑₀ m) → B (⇑₀ m) → C (B m)
    record 𝓒heck ⦃ _ : [𝓒heck] ⦄ : Ø x ∙̂ a ∙̂ b ∙̂ c where field check : 𝓬heck
open 𝓒heck ⦃ … ⦄ public

check[_] : ∀
  {x} {X : Ø x}
  {a} {A : X → Ø a}
  {b} {B : X → Ø b}
  {c} (C : Ø b → Ø c)
  ⦃ _ : [𝓒heck] A B C ⦄
  ⦃ _ : 𝓢uccessor₀ X ⦄
  ⦃ _ : 𝓒heck A B C ⦄
  → 𝓬heck A B C
check[ _ ] = check

module _
  {x} {X : Ø x}
  {a} (A : X → Ø a)
  {b} (B : X → Ø b)
  {c} (C : Ø b → Ø c)
  {ℓ} (_≈_ : ∀ {x} → C (B x) → C (B x) → Ø ℓ)
  where
  record [𝓒heck/thin=1] : Ø₀ where
    no-eta-equality
    constructor ∁
  module _
    ⦃ _ : 𝓢uccessor₀ X ⦄
    ⦃ _ : [𝓣hin] A B ⦄
    ⦃ _ : 𝓣hin A B ⦄
    ⦃ _ : [𝓒heck] A B C ⦄
    ⦃ _ : 𝓒heck A B C ⦄
    ⦃ _ : 𝓟ure C ⦄
    where
    𝓬heck/thin=1 = ∀ {n} (x : A (⇑₀ n)) (y : B n) → check x (thin x y) ≈ pure y
    record 𝓒heck/thin=1 ⦃ _ : [𝓒heck/thin=1] ⦄ : Ø x ∙̂ a ∙̂ b ∙̂ c ∙̂ ℓ where field check/thin=1 : 𝓬heck/thin=1
open 𝓒heck/thin=1 ⦃ … ⦄ public

check/thin=1[_] : ∀
  {x} {X : Ø x}
  {a} {A : X → Ø a}
  {b} {B : X → Ø b}
  {c} {C : Ø b → Ø c}
  {ℓ} (_≈_ : ∀ {x} → C (B x) → C (B x) → Ø ℓ)
  ⦃ _ : 𝓢uccessor₀ X ⦄
  ⦃ _ : [𝓣hin] A B ⦄
  ⦃ _ : 𝓣hin A B ⦄
  ⦃ _ : [𝓒heck] A B C ⦄
  ⦃ _ : 𝓒heck A B C ⦄
  ⦃ _ : 𝓟ure C ⦄
  ⦃ _ : [𝓒heck/thin=1] A B C _≈_ ⦄
  ⦃ _ : 𝓒heck/thin=1 A B C _≈_ ⦄
  → 𝓬heck/thin=1 A B C _≈_
check/thin=1[ _ ] = check/thin=1

record IsThickandthin
  {x a b c ℓb ℓc}
  {X : Ø x}
  (A : X → Ø a)
  (B : X → Ø b)
  (_≈B_ : ∀ {x} → B x → B x → Ø ℓb)
  (C : Ø b → Ø c)
  (_≈C_ : ∀ {x} → C (B x) → C (B x) → Ø ℓc)
  : Ø x ∙̂ a ∙̂ ↑̂ b ∙̂ ℓb ∙̂ c ∙̂ ℓc where
  constructor ∁
  field
    overlap ⦃ `𝓢uccessor₀ ⦄ : 𝓢uccessor₀ X
    overlap ⦃ `[𝓢uccessor₁] ⦄ : [𝓢uccessor₁] A
    overlap ⦃ `𝓢uccessor₁ ⦄ : 𝓢uccessor₁ A
    overlap ⦃ `[𝓣hick] ⦄ : [𝓣hick] A B
    overlap ⦃ `𝓣hick ⦄ : 𝓣hick A B
    overlap ⦃ `[𝓣hin] ⦄ : [𝓣hin] A B
    overlap ⦃ `𝓣hin ⦄ : 𝓣hin A B
    overlap ⦃ `[𝓘njectivity₂,₁] ⦄ : ∀ {m} → [𝓘njectivity₂,₁] (𝔱hin A B m) _≈B_ _≈B_
    overlap ⦃ `𝓘njectivity₂,₁ ⦄   : ∀ {m} → 𝓘njectivity₂,₁ (𝔱hin A B m) _≈B_ _≈B_
    overlap ⦃ `[𝓒heck] ⦄ : [𝓒heck] A B C
    overlap ⦃ `𝓒heck ⦄ : 𝓒heck A B C
    overlap ⦃ `[𝓣hick/thin=1] ⦄ : [𝓣hick/thin=1] A B _≈B_
    overlap ⦃ `𝓣hick/thin=1 ⦄ : 𝓣hick/thin=1 A B _≈B_
    overlap ⦃ `[𝓒heck/thin=1] ⦄ : [𝓒heck/thin=1] A B C _≈C_
    overlap ⦃ `𝓟ure ⦄ : 𝓟ure C
    overlap ⦃ `𝓒heck/thin=1 ⦄ : 𝓒heck/thin=1 A B C _≈C_

record Thickandthin x a b ℓb c ℓc : Ø ↑̂ (x ∙̂ a ∙̂ b ∙̂ ℓb ∙̂ c ∙̂ ℓc) where
  constructor ∁
  field
    {X} : Ø x
    A : X → Ø a
    B : X → Ø b
    _≈B_ : ∀ {x} → B x → B x → Ø ℓb
    C : Ø b → Ø c
    _≈C_ : ∀ {x} → C (B x) → C (B x) → Ø ℓc
    ⦃ `IsThickandthin ⦄ : IsThickandthin A B _≈B_ C _≈C_


text:
-- simply-typed λ-calculus w/ DeBruijn indices

module LC where

open import Agda.Primitive
open import Agda.Builtin.Bool
open import Data.Bool.Properties hiding (≤-trans ; <-trans ; ≤-refl ; <-irrefl)
open import Data.Empty
open import Data.Nat renaming (_+_ to _+ᴺ_ ; _≤_ to _≤ᴺ_ ; _≥_ to _≥ᴺ_ ; _<_ to _<ᴺ_ ; _>_ to _>ᴺ_)
open import Data.Nat.Properties renaming (_<?_ to _<ᴺ?_)
open import Data.Integer renaming (_+_ to _+ᶻ_ ; _≤_ to _≤ᶻ_ ; _≥_ to _≥ᶻ_ ; _<_ to _<ᶻ_ ; _>_ to _>ᶻ_)
open import Data.Integer.Properties using (⊖-≥ ; 0≤n⇒+∣n∣≡n ; +-monoˡ-≤)
open import Data.List
open import Data.List.Relation.Unary.All
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation

open import Auxiliary

module defs where
  data Exp : Set where
    Var : ℕ → Exp
    Abs : Exp → Exp
    App : Exp → Exp → Exp

  data Ty : Set where
    Fun : Ty → Ty → Ty

  -- typing

  Env = List Ty

  data _∶_∈_ : ℕ → Ty → Env → Set where
    here : {T : Ty} {Γ : Env} → 0 ∶ T ∈ (T ∷ Γ)
    there : {n : ℕ} {T₁ T₂ : Ty} {Γ : Env} → n ∶ T₁ ∈ Γ → (ℕ.suc n) ∶ T₁ ∈ (T₂ ∷ Γ)

  data _⊢_∶_ : Env → Exp → Ty → Set where
    TVar : {n : ℕ} {Γ : Env} {T : Ty} → n ∶ T ∈ Γ → Γ ⊢ (Var n) ∶ T
    TAbs : {Γ : Env} {T₁ T₂ : Ty} {e : Exp} → (T₁ ∷ Γ) ⊢ e ∶ T₂ → Γ ⊢ (Abs e) ∶ (Fun T₁ T₂)
    TApp : {Γ : Env} {T₁ T₂ : Ty} {e₁ e₂ : Exp} → Γ ⊢ e₁ ∶ (Fun T₁ T₂) → Γ ⊢ e₂ ∶ T₁ → Γ ⊢ (App e₁ e₂) ∶ T₂

-- denotational semantics
module denotational where
  open defs

  Valᵈ : Ty → Set
  Valᵈ (Fun Ty₁ Ty₂) = (Valᵈ Ty₁) → (Valᵈ Ty₂)

  access : {n : ℕ} {Γ : Env} {T : Ty} → n ∶ T ∈ Γ → All Valᵈ Γ → Valᵈ T
  access here (V ∷ Γ) = V
  access (there J) (V ∷ Γ) = access J Γ

  eval : {Γ : Env} {T : Ty} {e : Exp} → Γ ⊢ e ∶ T → All Valᵈ Γ → Valᵈ T
  eval (TVar c) Val-Γ = access c Val-Γ
  eval (TAbs TJ) Val-Γ = λ V → eval TJ (V ∷ Val-Γ)
  eval (TApp TJ TJ₁) Val-Γ = (eval TJ Val-Γ) (eval TJ₁ Val-Γ)

-- operational semantics (call-by-value)
module operational where
  open defs

  -- shifting, required to avoid variable-capturing in substitution
  -- see Pierce 2002, pg. 78/79
  ↑_,_[_] : ℤ → ℕ → Exp → Exp
  ↑ d , c [ Var x ]
    with (x <ᴺ? c)
  ...  | yes p = Var x
  ...  | no ¬p = Var (∣ (ℤ.pos x) +ᶻ d ∣)  -- should always be positive anyway
  ↑ d , c [ Abs t ] = Abs (↑ d , (ℕ.suc c) [ t ])
  ↑ d , c [ App t t₁ ] = App (↑ d , c [ t ]) (↑ d , c [ t₁ ])

  -- shifting in range [n, m]; by def. m < n implies no shift
  ↑[_,_]_[_] : ℕ → ℕ → ℤ → Exp → Exp
  ↑[ n , m ] d [ Var x ]
    with (x <ᴺ? n)
  ...  | yes p = Var x
  ...  | no ¬p
       with (m <ᴺ? x)
  ...     | yes p' = Var x
  ...     | no ¬p' = Var (∣ (ℤ.pos x) +ᶻ d ∣)
  ↑[ n , m ] d [ Abs e ] = Abs (↑[ ℕ.suc n , ℕ.suc m ] d [ e ])
  ↑[ n , m ] d [ App e e₁ ] = App (↑[ n , m ] d [ e ]) (↑[ n , m ] d [ e₁ ])

  -- shorthands
  ↑¹[_] : Exp → Exp
  ↑¹[ e ] = ↑ (ℤ.pos 1) , 0 [ e ]

  ↑⁻¹[_] : Exp → Exp
  ↑⁻¹[ e ] = ↑ (ℤ.negsuc 0) , 0 [ e ]

  -- substitution
  -- see Pierce 2002, pg. 80
  [_↦_]_ : ℕ → Exp → Exp → Exp
  [ k ↦ s ] Var x
    with (Data.Nat._≟_ x k)
  ...  | yes p = s
  ...  | no ¬p = Var x
  [ k ↦ s ] Abs t = Abs ([ ℕ.suc k ↦ ↑¹[ s ] ] t)
  [ k ↦ s ] App t t₁ = App ([ k ↦ s ] t) ([ k ↦ s ] t₁)

  data Val : Exp → Set where
    VFun : {e : Exp} → Val (Abs e)

  -- reduction relation
  data _⇒_ : Exp → Exp → Set where
    ξ-App1 : {e₁ e₁' e₂ : Exp} → e₁ ⇒ e₁' → App e₁ e₂ ⇒ App e₁' e₂
    ξ-App2 : {e e' v : Exp} → Val v → e ⇒ e' → App v e ⇒ App v e'
    β-App : {e v : Exp} → Val v → (App (Abs e) v) ⇒ (↑⁻¹[ ([ 0 ↦ ↑¹[ v ] ] e) ])

  ---- properties & lemmas

  --- properties of shifting

  ↑-var-refl : {d : ℤ} {c : ℕ} {x : ℕ} {le : ℕ.suc x ≤ᴺ c} → ↑ d , c [ Var x ] ≡ Var x
  ↑-var-refl {d} {c} {x} {le}
    with (x <ᴺ? c)
  ...  | no ¬p = contradiction le ¬p
  ...  | yes p = refl

  ↑[]-var-refl-< : {n m x : ℕ} {d : ℤ} {le : x <ᴺ n} → ↑[ n , m ] d [ Var x ] ≡ Var x
  ↑[]-var-refl-< {n} {m} {x} {d} {le}
    with (x <ᴺ? n)
  ...  | yes p = refl
  ...  | no ¬p = contradiction le ¬p

  ↑[]-var-refl-> : {n m x : ℕ} {d : ℤ} {le : m <ᴺ x} → ↑[ n , m ] d [ Var x ] ≡ Var x
  ↑[]-var-refl-> {n} {m} {x} {d} {le}
    with (x <ᴺ? n)
  ...  | yes p = refl
  ...  | no p
      with (m <ᴺ? x)
  ...    | no ¬q = contradiction le ¬q
  ...    | yes q = refl

  ↑[]-var-shift : {n m x : ℕ} {d : ℤ} (le1 : n ≤ᴺ x) (le2 : x ≤ᴺ m) → ↑[ n , m ] d [ Var x ] ≡  Var (∣ (ℤ.pos x) +ᶻ d ∣)
  ↑[]-var-shift {n} {m} {x} {d} le1 le2
    with x <ᴺ? n
  ...  | yes p = contradiction p (<⇒≱ (s≤s le1))
  ...  | no ¬p
      with m <ᴺ? x
  ...    | yes p' = contradiction p' (<⇒≱ (s≤s le2))
  ...    | no ¬p' = refl

  ↑¹-var : {x : ℕ} → ↑¹[ Var x ] ≡ Var (ℕ.suc x)
  ↑¹-var {zero} = refl
  ↑¹-var {ℕ.suc x}
    rewrite (sym (n+1≡sucn{x +ᴺ 1}))
          | (sym (n+1≡sucn{x}))
          = cong ↑¹[_] (↑¹-var{x})

  ↑⁻¹ₖ[↑¹ₖ[s]]≡s : {e : Exp} {k : ℕ} → ↑ -[1+ 0 ] , k [ ↑ + 1 , k [ e ] ] ≡ e
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {Var x} {k}
    with (x <ᴺ? k)
  -- x < k
  --  => ↑⁻¹ₖ(↑¹ₖ(Var n)) = ↑⁻¹ₖ(Var n) = Var n
  ...  | yes p = ↑-var-refl{ -[1+ 0 ]}{k}{x}{p}
  -- x ≥ k
  --  => ↑⁻¹ₖ(↑¹ₖ(Var n)) = ↑⁻¹ₖ(Var |n + 1|) = Var (||n + 1| - 1|) = Var n
  ...  | no ¬p
       with (¬[x≤k]⇒¬[sucx≤k] ¬p)
  ...     | ¬p'
          with (x +ᴺ 1) <ᴺ? k
  ...        | yes pp = contradiction pp ¬p'
  ...        | no ¬pp
             rewrite (∣nℕ+1⊖1∣≡n{x})
                   = refl
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {Abs e} {k} = cong Abs ↑⁻¹ₖ[↑¹ₖ[s]]≡s
  ↑⁻¹ₖ[↑¹ₖ[s]]≡s {App e e₁} = cong₂ App ↑⁻¹ₖ[↑¹ₖ[s]]≡s ↑⁻¹ₖ[↑¹ₖ[s]]≡s

  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] : {k l : ℤ} {c : ℕ} {s : Exp} → l ≥ᶻ +0 → ↑ k , c [ ↑ l , c [ s ] ] ≡ ↑ (l +ᶻ k) , c [ s ]
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {k} {l} {c} {Var x} ge
    with x <ᴺ? c
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {k} {l} {c} {Var x} ge | no ¬p
      with ∣ + x +ᶻ l ∣ <ᴺ? c
  ...    | yes q = contradiction q (<⇒≱ (n≤m⇒n<sucm (≤-trans (≮⇒≥ ¬p) (m≥0⇒∣n+m∣≥n ge))))
  ...    | no ¬q
         rewrite (0≤n⇒+∣n∣≡n{+ x +ᶻ l} (m≥0⇒n+m≥0 ge))
               | (Data.Integer.Properties.+-assoc (+_ x) l k)
               = refl
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {k} {l} {c} {Var x} ge | yes p
      with x <ᴺ? c
  ...    | yes p' = refl
  ...    | no ¬p' = contradiction p ¬p'
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {k} {l} {c} {Abs s} le = cong Abs (↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s]{k}{l}{ℕ.suc c}{s} le)
  ↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s] {k} {l} {c} {App s s₁} le = cong₂ App  (↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s]{k}{l}{c}{s} le)  (↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s]{k}{l}{c}{s₁} le)

  ↑k,q[↑l,c[s]]≡↑l+k,c[s] : {k l : ℤ} {q c : ℕ} {s : Exp} →  + q ≤ᶻ + c +ᶻ l → c ≤ᴺ q → ↑ k , q [ ↑ l , c [ s ] ] ≡ ↑ (l +ᶻ k) , c [ s ]
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {k} {l} {q} {c} {Var x} ge₁ ge₂
    with x <ᴺ? c
  ... | yes p
      with x <ᴺ? q
  ...    | yes p' = refl
  ...    | no ¬p' = contradiction (≤-trans p ge₂) ¬p'
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {k} {l} {q} {c} {Var x} ge₁ ge₂
      | no ¬p
      with ∣ + x +ᶻ l ∣ <ᴺ? q
  ...    | yes p' = contradiction p' (≤⇒≯ (+a≤b⇒a≤∣b∣{q}{+ x +ᶻ l} (Data.Integer.Properties.≤-trans ge₁ ((Data.Integer.Properties.+-monoˡ-≤ l (+≤+ (≮⇒≥ ¬p)))))))
  ...    | no ¬p'
         rewrite (0≤n⇒+∣n∣≡n{+ x +ᶻ l} (Data.Integer.Properties.≤-trans (+≤+ z≤n) ((Data.Integer.Properties.≤-trans ge₁ ((Data.Integer.Properties.+-monoˡ-≤ l (+≤+ (≮⇒≥ ¬p))))))))
               | (Data.Integer.Properties.+-assoc (+_ x) l k)
               = refl
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {k} {l} {q} {c} {Abs s} ge₁ ge₂ = cong Abs (↑k,q[↑l,c[s]]≡↑l+k,c[s] {k} {l} {ℕ.suc q} {ℕ.suc c} {s} (+q≤+c+l⇒+1q≤+1c+l{q}{c}{l} ge₁) (s≤s ge₂))
  ↑k,q[↑l,c[s]]≡↑l+k,c[s] {k} {l} {q} {c} {App s s₁} ge₁ ge₂ = cong₂ App (↑k,q[↑l,c[s]]≡↑l+k,c[s] {k} {l} {q} {c} {s} ge₁ ge₂) (↑k,q[↑l,c[s]]≡↑l+k,c[s] {k} {l} {q} {c} {s₁} ge₁ ge₂)

  --- properties of substitution

  subst-trivial : {x : ℕ} {s : Exp} → [ x ↦ s ] Var x ≡ s
  subst-trivial {x} {s}
    with x Data.Nat.≟ x
  ...  | no ¬p = contradiction refl ¬p
  ...  | yes p = refl

  var-subst-refl : {n m : ℕ} {neq : n ≢ m} {e : Exp} → [ n ↦ e ] (Var m) ≡ (Var m)
  var-subst-refl {n} {m} {neq} {e}
    with Data.Nat._≟_ n m
       | map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (Data.Bool.Properties.T? (m ≡ᵇ n))
  ...  | yes p | _ = contradiction p neq
  ...  | no ¬p | yes q = contradiction q (≢-sym ¬p)
  ...  | no ¬p | no ¬q = refl

  --- properties and manipulation of environments

  var-env-< : {Γ : Env} {T : Ty} {n : ℕ} (j : n ∶ T ∈ Γ) → n <ᴺ (length Γ)
  var-env-< {.(T ∷ _)} {T} {.0} here = s≤s z≤n
  var-env-< {.(_ ∷ _)} {T} {.(ℕ.suc _)} (there j) = s≤s (var-env-< j)

  -- type to determine whether var type judgement in env. (Δ ++ Γ) is in Δ or Γ
  data extract-env-or {Δ Γ : Env} {T : Ty} {x : ℕ} : Set where
    in-Δ : x ∶ T ∈ Δ → extract-env-or
    -- x ≥ length Δ makes sure that x really is in Γ; e.g.
    -- x = 1, Δ = (S ∷ T), Γ = (T ∷ Γ'); here 1 ∶ T ∈ Δ as well as (1 ∸ 2) ≡ 0 ∶ T ∈ Γ
    in-Γ : (x ≥ᴺ length Δ) → (x ∸ length Δ) ∶ T ∈ Γ → extract-env-or

  extract : {Δ Γ : Env} {T : Ty} {x : ℕ} (j : x ∶ T ∈ (Δ ++ Γ)) → extract-env-or{Δ}{Γ}{T}{x}
  extract {[]} {Γ} {T} {x} j = in-Γ z≤n j
  extract {x₁ ∷ Δ} {Γ} {.x₁} {.0} here = in-Δ here
  extract {x₁ ∷ Δ} {Γ} {T} {ℕ.suc x} (there j)
    with extract {Δ} {Γ} {T} {x} j
  ...  | in-Δ j'  = in-Δ (there j')
  ...  | in-Γ ge j'' = in-Γ (s≤s ge) j''

  ext-behind : {Δ Γ : Env} {T : Ty} {x : ℕ} → x ∶ T ∈ Δ → x ∶ T ∈ (Δ ++ Γ)
  ext-behind here = here
  ext-behind (there j) = there (ext-behind j)

  ext-front : {n : ℕ} {Γ Δ : Env} {S : Ty} → n ∶ S ∈ Γ → (n +ᴺ (length Δ)) ∶ S ∈ (Δ ++ Γ)
  ext-front {n} {Γ} {[]} {S} j
    rewrite (n+length[]≡n{A = Ty}{n = n})
          = j
  ext-front {n} {Γ} {T ∷ Δ} {S} j
    rewrite (+-suc n (foldr (λ _ → ℕ.suc) 0 Δ))
          = there (ext-front j)

  swap-env-behind : {Γ Δ : Env} {T : Ty} → 0 ∶ T ∈ (T ∷ Γ) → 0 ∶ T ∈ (T ∷ Δ)
  swap-env-behind {Γ} {Δ} {T} j = here

  swap-type : {Δ ∇ Γ : Env} {T : Ty} → (length Δ) ∶ T ∈ (Δ ++ T ∷ ∇ ++ Γ) → (length Δ +ᴺ length ∇) ∶ T ∈ (Δ ++ ∇ ++ T ∷ Γ)
  swap-type {Δ} {∇} {Γ} {T} j
    with extract{Δ}{T ∷ ∇ ++ Γ} j
  ...  | in-Δ x = contradiction (var-env-< {Δ} {T} x) (<-irrefl refl)
  ...  | in-Γ le j'
       with extract{T ∷ ∇}{Γ} j'
  ...     | in-Δ j''
          rewrite (n∸n≡0 (length Δ))
                | (sym (length[A++B]≡length[A]+length[B]{lzero}{Ty}{Δ}{∇}))
                | (sym (++-assoc{lzero}{Ty}{Δ}{∇}{T ∷ Γ}))
                = ext-front{0}{T ∷ Γ}{Δ ++ ∇}{T} (swap-env-behind{∇}{Γ}{T} j'')
  ...     | in-Γ le' j''
          rewrite (length[A∷B]≡suc[length[B]]{lzero}{Ty}{T}{∇})
                | (n∸n≡0 (length Δ))
                = contradiction le' (<⇒≱ (s≤s z≤n))

  env-pred : {Γ : Env} {S T : Ty} {y : ℕ} {gt : y ≢ 0} → y ∶ T ∈ (S ∷ Γ) → ∣ y ⊖ 1 ∣ ∶ T ∈ Γ
  env-pred {Γ} {S} {.S} {.0} {gt} here = contradiction refl gt
  env-pred {Γ} {S} {T} {.(ℕ.suc _)} {gt} (there j) = j

  env-type-equiv-here : {Γ : Env} {S T : Ty} → 0 ∶ T ∈ (S ∷ Γ) → T ≡ S
  env-type-equiv-here {Γ} {S} {.S} here = refl

  env-type-equiv : {Δ ∇ : Env} {S T : Ty} → length Δ ∶ T ∈ (Δ ++ S ∷ ∇) → T ≡ S
  env-type-equiv {Δ} {∇} {S} {T} j
    with extract{Δ}{S ∷ ∇} j
  ...  | in-Δ x = contradiction (var-env-< x) (≤⇒≯ ≤-refl)
  ...  | in-Γ x j'
       rewrite (n∸n≡0 (length Δ))
             = env-type-equiv-here {∇} {S} {T} j'

  env-type-equiv-j : {Γ : Env} {S T : Ty} {n : ℕ} → T ≡ S → n ∶ T ∈ Γ → n ∶ S ∈ Γ
  env-type-equiv-j {Γ} {S} {T} {n} eq j
    rewrite eq
          = j

  -- extension of environment

  ext : {Γ Δ ∇ : Env} {S : Ty} {s : Exp} → (∇ ++ Γ) ⊢ s ∶ S → (∇ ++ Δ ++ Γ) ⊢ ↑ (ℤ.pos (length Δ)) , length ∇ [ s ] ∶ S
  ext {Γ} {Δ} {∇} (TVar {n} x)
    with extract{∇}{Γ} x
  ... | in-Δ x₁
      with n <ᴺ? length ∇
  ...    | yes p = TVar (ext-behind x₁)
  ...    | no ¬p = contradiction (var-env-< x₁) ¬p
  ext {Γ} {Δ} {∇} (TVar {n} x)
      | in-Γ x₁ x₂
      with n <ᴺ? length ∇
  ...    | yes p = contradiction x₁ (<⇒≱ p)
  ...    | no ¬p
         with (ext-front{n ∸ length ∇}{Γ}{∇ ++ Δ} x₂)
  ...       | w
            rewrite (length[A++B]≡length[A]+length[B]{lzero}{Ty}{∇}{Δ})
                  | (sym (+-assoc (n ∸ length ∇) (length ∇) (length Δ)))
                  | (m∸n+n≡m{n}{length ∇} (≮⇒≥ ¬p))
                  | (++-assoc{lzero}{Ty}{∇}{Δ}{Γ})
                  = TVar w
  ext {Γ} {Δ} {∇} {Fun T₁ T₂} {Abs e} (TAbs j) = TAbs (ext{Γ}{Δ}{T₁ ∷ ∇} j)
  ext {Γ} {Δ} {∇} {S} {App s₁ s₂} (TApp{T₁ = T₁} j₁ j₂) = TApp (ext{Γ}{Δ}{∇}{Fun T₁ S} j₁) (ext{Γ}{Δ}{∇}{T₁} j₂)

  ---- progress and preservation

  -- progress theorem, i.e. a well-typed closed expression is either a value
  -- or can be reduced further
  data Progress (e : Exp) {T : Ty} {j : [] ⊢ e ∶ T}  : Set where
    step : {e' : Exp} → e ⇒ e' → Progress e
    value : Val e → Progress e

  progress : (e : Exp) {T : Ty} {j : [] ⊢ e ∶ T} → Progress e {T} {j}
  progress (Var x) {T} {TVar ()}
  progress (Abs e) = value VFun
  progress (App e e₁) {T} {TApp{T₁ = T₁}{T₂ = .T} j j₁} with progress e {Fun T₁ T} {j}
  ... | step x = step (ξ-App1 x)
  ... | value VFun with progress e₁ {T₁} {j₁}
  ...    | step x₁ = step (ξ-App2 VFun x₁)
  ...    | value x₁ = step (β-App x₁)

  ---

  -- preservation under substitution
  preserve-subst : {T S : Ty} {Γ Δ : Env} {e s : Exp} (j : (Δ ++ (S ∷ Γ)) ⊢ e ∶ T) (j' : Γ ⊢ s ∶ S) → (Δ ++ Γ) ⊢  ↑ -[1+ 0 ] , length Δ [ [ length Δ ↦ ↑ (ℤ.pos (ℕ.suc (length Δ))) , 0 [ s ] ] e ] ∶ T
  preserve-subst {T} {S} {Γ} {Δ} {e} {s} (TVar{n} x) j'
    with extract{Δ}{S ∷ Γ}{T}{n} x
  ...  | in-Δ x₁
       with n Data.Nat.≟ length Δ
  ...     | yes p = contradiction p (<⇒≢ (var-env-< x₁))
  ...     | no ¬p
          with n <ᴺ? length Δ
  ...        | yes q = TVar (ext-behind{Δ}{Γ} x₁)
  ...        | no ¬q = contradiction (var-env-< x₁) ¬q
  preserve-subst {T} {S} {Γ} {Δ} {e} {s} (TVar{n} x) j'
       | in-Γ x₁ x₂
       with n Data.Nat.≟ length Δ
  ...     | yes p
          rewrite (↑k,q[↑l,c[s]]≡↑l+k,c[s]{ -[1+ 0 ]}{+[1+ length Δ ]}{length Δ}{0}{s} (+≤+ n≤sucn) z≤n)
                | p
                | (env-type-equiv x)
                = ext{Γ}{Δ}{[]} j'
  ...     | no ¬p
          with n <ᴺ? length Δ
  ...        | yes q = contradiction x₁ (<⇒≱ q)
  ...        | no ¬q rewrite (sym (minus-1{n}{length Δ}{≤∧≢⇒< x₁ (≢-sym ¬p)}))
                           = TVar (ext-front{Δ = Δ} (env-pred{Γ}{S}{T}{gt = ≢-sym (<⇒≢ (m>n⇒m∸n≥1 (≤∧≢⇒< x₁ (≢-sym ¬p))))} x₂))
  preserve-subst {T} {S} {Γ} {Δ} {Abs e'} {s} (TAbs{T₁ = T₁}{T₂} j) j'
    with preserve-subst{T₂}{S}{Γ}{T₁ ∷ Δ}{e'}{s} j j'
  ...  | w
       rewrite (↑ᵏ[↑ˡ[s]]≡↑ᵏ⁺ˡ[s]{+ 1}{+[1+ length Δ ]}{0}{s} (+≤+ z≤n))
             | (length[A∷B]≡suc[length[B]]{lzero}{Ty}{T₁}{Δ})
             | (n+1≡sucn{length Δ})
             = TAbs w
  preserve-subst (TApp j j₁) j' = TApp (preserve-subst j j') (preserve-subst j₁ j')

  -- preservation theorem, i.e. a well-typed expression reduces to a well-typed expression
  preserve : {T : Ty} {Γ : Env} (e e' : Exp) (j : Γ ⊢ e ∶ T) (r : e ⇒ e') → Γ ⊢ e' ∶ T
  preserve (App s₁ s₂) .(App _ s₂) (TApp j j') (ξ-App1{e₁' = s₁'} r) = TApp (preserve s₁ s₁' j r) j' -- IH on inner reduction
  preserve (App s₁ s₂) .(App s₁ _) (TApp j j') (ξ-App2{e' = s₂'} x r) = TApp j (preserve s₂ s₂' j' r)
  preserve (App (Abs e) s')  .(↑⁻¹[ [ 0 ↦ ↑¹[ s' ] ] e ]) (TApp (TAbs j) j') (β-App x) = preserve-subst{Δ = []} j j'

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

  -- swap-subst lemma: swap the position of a type in an environment (did not need this after all)

  -- aux. calculations
  length-≡ : {Δ ∇ Γ : Env} {S : Ty} → ℕ.suc (length Δ +ᴺ (length Γ +ᴺ length ∇)) ≡ length (Δ ++ S ∷ ∇ ++ Γ)
  length-≡ {Δ} {∇} {Γ} {S}
    rewrite (length[A++B]≡length[A]+length[B]{lzero}{Ty}{Δ}{S ∷ ∇ ++ Γ})
          | (length[A++B]≡length[A]+length[B]{lzero}{Ty}{∇}{Γ})
          | (+-suc (length Δ) (length ∇ +ᴺ length Γ))
          | (+-comm (length ∇) (length Γ))
          = refl

  length-≡' : {Δ ∇ : Env} {S : Ty} → length (Δ ++ ∇ ++ S ∷ []) ≡ length Δ +ᴺ ℕ.suc (length ∇)
  length-≡' {Δ} {∇} {S}
    rewrite (length[A++B]≡length[A]+length[B]{lzero}{Ty}{Δ}{∇ ++ S ∷ []})
          | (length[A++B]≡length[A]+length[B]{lzero}{Ty}{∇}{S ∷ []})
          | (+-suc (length ∇) (0))
          | (+-identityʳ (length ∇))
          = refl

  length-≡'' : {Δ ∇ : Env} {S : Ty} → length (Δ ++ ∇ ++ S ∷ []) ≡ ℕ.suc (length ∇ +ᴺ length Δ)
  length-≡'' {Δ} {∇} {S}
    rewrite (cong (ℕ.suc) (+-comm (length ∇) (length Δ)))
          | (sym (+-suc (length Δ) (length ∇)))
          = length-≡'{Δ}{∇}{S}

  --- why the "r"? we have to "remember" where S was
  --- cannot substitute its position for zero, since ↑ would increase that
  --- cannot do ↑ and then subtitute its position for zero, since (position - 1) would be affected aswell
  --- fix: cache in unreachable variable r
  swap-subst : {T S : Ty} {Γ Δ ∇ : Env} {e : Exp} {r : ℕ} {gt : r >ᴺ ℕ.suc (length Δ +ᴺ (length Γ +ᴺ length ∇))}
               → (Δ ++ (S ∷ ∇) ++ Γ) ⊢ e ∶ T
               → (Δ ++ ∇ ++ (S ∷ Γ)) ⊢ [ r ↦ Var (length Δ +ᴺ length ∇) ] ↑[ ℕ.suc (length Δ) , length Δ +ᴺ length ∇ ] -[1+ 0 ] [ [ length Δ ↦ Var r ] e ] ∶ T
  swap-subst {(Fun T₁ T₂)} {S} {Γ} {Δ} {∇} {(Abs e)} {r} {gt} (TAbs j)
    rewrite (↑¹-var{length Δ +ᴺ length ∇})
          | (n+1≡sucn{r})
          = TAbs (swap-subst{T₂}{S}{Γ}{T₁ ∷ Δ}{∇}{e}{ℕ.suc r}{s≤s gt} j)
  swap-subst {T} {S} {Γ} {Δ} {∇} {(App e e₁)} {r} {gt} (TApp{T₁ = T₁}{T₂} j j₁) = TApp (swap-subst{Fun T₁ T₂}{S}{Γ}{Δ}{∇}{e}{r}{gt} j) (swap-subst{T₁}{S}{Γ}{Δ}{∇}{e₁}{r}{gt} j₁)
  swap-subst {T} {S} {Γ} {Δ} {∇} {Var y} {r} {gt} (TVar j)
    with extract{Δ} {(S ∷ ∇) ++ Γ} {T} {y} j
       | y <ᴺ? (foldr (λ _ → ℕ.suc) 0 Δ)
       | Data.Nat._≟_ y (length Δ)
  -- y ∈ Δ
  ... | in-Δ x | yes p | yes q = contradiction q (<⇒≢ p)
  ... | in-Δ x | yes p | no ¬q
    rewrite (↑[]-var-refl-<{ℕ.suc (length Δ)}{length Δ +ᴺ length ∇}{y}{ -[1+ 0 ] }{[k<x]⇒[k<sucx] p})
          | (var-subst-refl{r}{y}{≢-sym (<⇒≢ (a<b≤c⇒a<c p (≤-trans (n≤m⇒n≤sucm (m≤m+n (length Δ) (length Γ +ᴺ length ∇))) (<-trans (s≤s ≤-refl) gt))) )}
            {Var (foldr (λ _ → ℕ.suc) 0 Δ +ᴺ foldr (λ _ → ℕ.suc) 0 ∇)})
          = TVar (ext-behind x)
  ... | in-Δ x | no ¬p | _ = contradiction (var-env-< x) ¬p
  -- y ∈ (S ∷ ∇ ++ Γ)
  ... | in-Γ ge x | p | q
    with extract{S ∷ ∇} {Γ} {T} {y ∸ length Δ} x
  --- y ∈ (S ∷ ∇)
  ---- y @ S
  swap-subst {T} {S} {Γ} {Δ} {∇} {Var y} {r} {gt} (TVar j) | in-Γ ge x | p | yes q' | in-Δ x'
    rewrite (↑[]-var-refl->{ℕ.suc (length Δ)}{length Δ +ᴺ length ∇}{r}{ -[1+ 0 ] }{<-trans (s≤s (n+m≤n+q+m {length Δ} {length ∇} {length Γ})) gt})
          | (subst-trivial{r} {Var (length Δ +ᴺ length ∇)})
          | q'
          | (env-type-equiv j)
          = TVar (swap-type{Δ}{∇}{Γ}{S} (env-type-equiv-j (env-type-equiv j) j))
  ---- y ∈ ∇
  swap-subst {T} {S} {Γ} {Δ} {∇} {Var y} {r} {gt} (TVar j) | in-Γ ge x | p | no ¬q' | in-Δ x'
    rewrite (↑[]-var-shift{ℕ.suc (length Δ)}{length Δ +ᴺ length ∇}{y}{ -[1+ 0 ]} (≤∧≢⇒< ge (≢-sym ¬q')) (≤-trans (≤-pred (m≤n∧m≡q⇒q≤n (m≤n⇒m+o≤n+o{o = length Δ} (var-env-< x'))
            (cong ℕ.suc (m∸n+n≡m ge)))) (≤-refl-+-comm{length ∇}{length Δ})))
          | length-≡ {Δ} {∇} {Γ} {S}
          | (var-subst-refl {r} {∣ y ⊖ 1 ∣} {≢-sym (<⇒≢ (<-trans (n>0⇒n>∣n⊖1∣ (≤-trans (s≤s z≤n) ((≤∧≢⇒< ge (≢-sym ¬q'))))) (<-trans (var-env-< j) gt)))} {Var (length Δ +ᴺ length ∇)})
          | sym (minus-1{y}{length Δ}{≤∧≢⇒< ge (≢-sym ¬q')} )
          = TVar (ext-front{Δ = Δ}(ext-behind{∇}{S ∷ Γ}{T} (env-pred{gt = ≢-sym (<⇒≢ (m>n⇒m∸n≥1{y}{length Δ} ((≤∧≢⇒< ge (≢-sym ¬q')))))} x')))
  --- y ∈ Γ
  swap-subst {T} {S} {Γ} {Δ} {∇} {Var y} {r} {gt} (TVar j) | in-Γ ge x | no ¬p | yes q | in-Γ ge' x'
          = contradiction q (≢-sym (<⇒≢ (m∸n≢0⇒n<m{y}{length Δ} (≢-sym (<⇒≢ (a<b≤c⇒a<c (s≤s z≤n) (≤-trans (length[A∷B]≥1{lzero}{Ty}{S}{∇}) ge')))))))
  swap-subst {T} {S} {Γ} {Δ} {∇} {Var y} {r} {gt} (TVar j) | in-Γ ge x | yes p | yes q | in-Γ ge' x' = contradiction q (<⇒≢ p)
  swap-subst {T} {S} {Γ} {Δ} {∇} {Var y} {r} {gt} (TVar j) | in-Γ ge x | p | no ¬q' | in-Γ ge' x'
    rewrite (↑[]-var-refl->{ℕ.suc (length Δ)}{length Δ +ᴺ length ∇}{y}{ -[1+ 0 ]}{a<b≤c⇒a<c (s≤s (≤-refl-+-comm{length Δ}{length ∇})) (m≤n∧n≡q⇒m≤q (m≤n⇒m+o≤n+o{o = length Δ} ge') (m∸n+n≡m ge))})
          | (var-subst-refl{r}{y}{≢-sym (<⇒≢ (<-trans (var-env-< j) (m≤n∧m≡q⇒q≤n gt (cong ℕ.suc (length-≡{Δ}{∇}{Γ}{S})))))}{ Var (foldr (λ _ → ℕ.suc) 0 Δ +ᴺ foldr (λ _ → ℕ.suc) 0 ∇)})
      with ext-front{((y ∸ (length Δ)) ∸ ℕ.suc (length ∇))}{Γ}{Δ ++ ∇ ++ (S ∷ [])}{T}
  ...     | w rewrite (∸-+-assoc y (length Δ) (ℕ.suc (length ∇)))
                    | (sym (length-≡'{Δ}{∇}{S}))
                    | (m∸n+n≡m{y}{length (Δ ++ ∇ ++ S ∷ [])}  (m≤n∧m≡q⇒q≤n (m≤n∧n≡q⇒m≤q (m≤n⇒m+o≤n+o{o = length Δ} ge') (m∸n+n≡m ge)) (sym (length-≡''{Δ}{∇}{S}))))
                    | (A++B++D∷[]++C≡A++B++D∷C{lzero}{Ty}{Δ}{∇}{Γ}{S})
                    = TVar (w x')

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
module subst where

open import lib

open import cedille-types
open import ctxt-types
open import is-free
open import rename
open import general-util
open import syntax-util

substh-ret-t : Set → Set
substh-ret-t T = ∀ {ed} → ctxt → renamectxt → trie ⟦ ed ⟧ → T → T

substh : ∀ {ed} → substh-ret-t ⟦ ed ⟧
substh-term : substh-ret-t term
substh-type : substh-ret-t type
substh-kind : substh-ret-t kind
substh-tk : substh-ret-t tk
substh-optClass : substh-ret-t optClass
substh-optGuide : substh-ret-t optGuide
substh-optTerm : substh-ret-t optTerm
substh-optType : substh-ret-t optType
substh-liftingType : substh-ret-t liftingType
substh-arg : substh-ret-t arg
substh-args : substh-ret-t args
substh-params : substh-ret-t params
substh-cases : substh-ret-t cases
substh-varargs : {ed : exprd} → ctxt → renamectxt → trie ⟦ ed ⟧ → varargs → varargs × renamectxt

substh{TERM} = substh-term
substh{TYPE} = substh-type
substh{KIND} = substh-kind
substh{LIFTINGTYPE} = substh-liftingType
substh{TK} = substh-tk
substh{ARG} = substh-arg
substh{QUALIF} = λ Γ ρ σ q → q

subst-rename-var-if : {ed : exprd} → ctxt → renamectxt → var → trie ⟦ ed ⟧ → var
subst-rename-var-if Γ ρ "_" σ = "_"
subst-rename-var-if Γ ρ x σ =
  {- rename bound variable x iff it is one of the vars being substituted for,
     or if x occurs free in one of the terms we are substituting for vars,
     or if it is the renamed version of any variable -}
  if trie-contains σ x || trie-any (is-free-in check-erased x) σ || renamectxt-in-range ρ x || ctxt-binds-var Γ x then
    rename-away-from x (λ s → ctxt-binds-var Γ s || trie-contains σ s) ρ
  else
    x

substh-term Γ ρ σ (App t m t') = App (substh-term Γ ρ σ t) m (substh-term Γ ρ σ t')
substh-term Γ ρ σ (AppTp t tp) = AppTp (substh-term Γ ρ σ t) (substh-type Γ ρ σ tp)
substh-term Γ ρ σ (Hole x₁) = Hole x₁
substh-term Γ ρ σ (Lam _ b _ x oc t) =
  let x' = subst-rename-var-if Γ ρ x σ in
    Lam posinfo-gen b posinfo-gen x' (substh-optClass Γ ρ σ oc)
      (substh-term (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh-term Γ ρ σ (Let _ (DefTerm _ x m t) t') =
  let x' = subst-rename-var-if Γ ρ x σ in
     (Let posinfo-gen (DefTerm posinfo-gen x' (substh-optType Γ ρ σ m) (substh-term Γ ρ σ t))
      (substh-term (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t'))
substh-term Γ ρ σ (Let _ (DefType _ x k t) t') =
  let x' = subst-rename-var-if Γ ρ x σ in
     (Let posinfo-gen (DefType posinfo-gen x' (substh-kind Γ ρ σ k) (substh-type Γ ρ σ t))
      (substh-term (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t'))
substh-term Γ ρ σ (Open _ x t) = Open posinfo-gen x (substh-term Γ ρ σ t)
substh-term Γ ρ σ (Parens _ t _) = substh-term Γ ρ σ t
substh-term{TERM} Γ ρ σ (Var _ x) =
 let x' = renamectxt-rep ρ x in
   trie-lookup-else (Var posinfo-gen x') σ x'
substh-term{ARG} Γ ρ σ (Var _ x) =
 let x' = renamectxt-rep ρ x in
   inst-lookup-term σ x'
substh-term{QUALIF} Γ ρ σ (Var _ x) =
 let x' = renamectxt-rep ρ x in
   qualif-lookup-term σ x'
substh-term Γ ρ σ (Var _ x) = Var posinfo-gen (renamectxt-rep ρ x)
substh-term Γ ρ σ (Beta _ ot ot') = Beta posinfo-gen (substh-optTerm Γ ρ σ ot) (substh-optTerm Γ ρ σ ot')
substh-term Γ ρ σ (IotaPair _ t1 t2 og pi') = IotaPair posinfo-gen (substh-term Γ ρ σ t1) (substh-term Γ ρ σ t2) (substh-optGuide Γ ρ σ og) pi'
substh-term Γ ρ σ (IotaProj t n _) = IotaProj (substh-term Γ ρ σ t) n posinfo-gen
substh-term Γ ρ σ (Epsilon _ lr m t) = Epsilon posinfo-gen lr m (substh-term Γ ρ σ t)
substh-term Γ ρ σ (Sigma _ t) = Sigma posinfo-gen (substh-term Γ ρ σ t)
substh-term Γ ρ σ (Phi _ t t₁ t₂ _) = Phi posinfo-gen (substh-term Γ ρ σ t) (substh-term Γ ρ σ t₁) (substh-term Γ ρ σ t₂) posinfo-gen
substh-term Γ ρ σ (Rho _ op on t og t') = Rho posinfo-gen op on (substh-term Γ ρ σ t) (substh-optGuide Γ ρ σ og) (substh-term Γ ρ σ t')
substh-term Γ ρ σ (Chi _ T t') = Chi posinfo-gen (substh-optType Γ ρ σ T) (substh-term Γ ρ σ t')
substh-term Γ ρ σ (Delta _ T t') = Delta posinfo-gen (substh-optType Γ ρ σ T) (substh-term Γ ρ σ t')
substh-term Γ ρ σ (Theta _ θ t ls) = Theta posinfo-gen (substh-theta θ) (substh-term Γ ρ σ t) (substh-lterms ls)
  where substh-lterms : lterms → lterms
        substh-lterms (LtermsNil pi) = LtermsNil pi
        substh-lterms (LtermsCons m t ls) = LtermsCons m (substh-term Γ ρ σ t) (substh-lterms ls)
        substh-vars : vars → vars
        substh-vars (VarsStart x) = VarsStart (renamectxt-rep ρ x)
        substh-vars (VarsNext x xs) = VarsNext (renamectxt-rep ρ x) (substh-vars xs)
        substh-theta : theta → theta
        substh-theta (AbstractVars xs) = AbstractVars (substh-vars xs)
        substh-theta θ = θ
substh-term Γ ρ σ (Mu _ x t ot _ cs _) =
  let x' = subst-rename-var-if Γ ρ x σ in
  let ρ' = renamectxt-insert ρ x x'    in
    Mu posinfo-gen x' (substh-term (ctxt-var-decl x' Γ) ρ' σ t) (substh-optType Γ ρ σ ot) posinfo-gen (substh-cases Γ ρ' σ cs) posinfo-gen
substh-term Γ ρ σ (Mu' _ t ot _ cs _) = Mu' posinfo-gen (substh-term Γ ρ σ t) (substh-optType Γ ρ σ ot) posinfo-gen (substh-cases Γ ρ σ cs) posinfo-gen

substh-cases Γ ρ σ NoCase = NoCase
substh-cases Γ ρ σ (SomeCase _ x varargs t cs) =
  let res = substh-varargs Γ ρ σ varargs in
  SomeCase posinfo-gen x (fst res) (substh-term Γ (snd res) σ t) (substh-cases Γ ρ σ cs)

substh-varargs Γ ρ σ NoVarargs                = NoVarargs , ρ
substh-varargs Γ ρ σ (NormalVararg x varargs) =
  let x' = subst-rename-var-if Γ ρ x σ in
  let ρ' = renamectxt-insert ρ x x'    in
  let res = substh-varargs Γ ρ' σ varargs in
  NormalVararg x' (fst res) , snd res
substh-varargs Γ ρ σ (ErasedVararg x varargs) =
  let x' = subst-rename-var-if Γ ρ x σ in
  let ρ' = renamectxt-insert ρ x x'    in
  let res = substh-varargs Γ ρ' σ varargs in
  ErasedVararg x' (fst res) , snd res
substh-varargs Γ ρ σ (TypeVararg   x varargs) =
  let x' = subst-rename-var-if Γ ρ x σ in
  let ρ' = renamectxt-insert ρ x x'    in
  let res = substh-varargs Γ ρ' σ varargs in
  TypeVararg x' (fst res) , snd res

substh-type Γ ρ σ (Abs _ b _ x atk t) =
  let x' = subst-rename-var-if Γ ρ x σ in
    Abs posinfo-gen b posinfo-gen x' (substh-tk Γ ρ σ atk)
      (substh-type (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh-type Γ ρ σ (TpLambda _ _ x atk t) =
  let x' = subst-rename-var-if Γ ρ x σ in
    TpLambda posinfo-gen posinfo-gen x' (substh-tk Γ ρ σ atk)
      (substh-type (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh-type Γ ρ σ (Iota _ _ x m t) =
  let x' = subst-rename-var-if Γ ρ x σ in
    Iota posinfo-gen posinfo-gen x' (substh-type Γ ρ σ m)
      (substh-type (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
substh-type Γ ρ σ (Lft _ _ x t l) =
  let x' = subst-rename-var-if Γ ρ x σ in
    Lft posinfo-gen posinfo-gen x' (substh-term (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t)
      (substh-liftingType Γ ρ σ l)
substh-type Γ ρ σ (TpApp tp tp₁) = TpApp (substh-type Γ ρ σ tp) (substh-type Γ ρ σ tp₁)
substh-type Γ ρ σ (TpAppt tp t) = TpAppt (substh-type Γ ρ σ tp) (substh-term Γ ρ σ t)
substh-type Γ ρ σ (TpArrow tp arrowtype tp₁) = TpArrow (substh-type Γ ρ σ tp) arrowtype (substh-type Γ ρ σ tp₁)
substh-type Γ ρ σ (TpEq _ x₁ x₂ _) = TpEq posinfo-gen (substh-term Γ ρ σ x₁) (substh-term Γ ρ σ x₂) posinfo-gen
substh-type Γ ρ σ (TpParens _ tp _) = substh-type Γ ρ σ tp
substh-type Γ ρ σ (NoSpans tp _) = substh-type Γ ρ σ tp
substh-type{TYPE} Γ ρ σ (TpVar _ x) =
 let x' = renamectxt-rep ρ x in
   trie-lookup-else (TpVar posinfo-gen x') σ x'
substh-type{ARG} Γ ρ σ (TpVar _ x) =
 let x' = renamectxt-rep ρ x in
   inst-lookup-type σ x'
substh-type{QUALIF} Γ ρ σ (TpVar _ x) =
 let x' = renamectxt-rep ρ x in
   qualif-lookup-type σ x'
substh-type Γ ρ σ (TpVar _ x) = TpVar posinfo-gen (renamectxt-rep ρ x)
substh-type Γ ρ σ (TpHole _) = TpHole posinfo-gen --ACG
substh-type Γ ρ σ (TpLet _ (DefTerm _ x m t) t') =
  let x' = subst-rename-var-if Γ ρ x σ in
     (TpLet posinfo-gen (DefTerm posinfo-gen x' (substh-optType Γ ρ σ m) (substh-term Γ ρ σ t))
      (substh-type (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t'))
substh-type Γ ρ σ (TpLet _ (DefType _ x k t) t') =
  let x' = subst-rename-var-if Γ ρ x σ in
     (TpLet posinfo-gen (DefType posinfo-gen x' (substh-kind Γ ρ σ k) (substh-type Γ ρ σ t))
      (substh-type (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ t'))
substh-kind Γ ρ σ (KndArrow k k₁) = KndArrow (substh-kind Γ ρ σ k) (substh-kind Γ ρ σ k₁)
substh-kind Γ ρ σ (KndParens x₁ k x₂) = substh-kind Γ ρ σ k
substh-kind Γ ρ σ (KndPi _ _ x atk k) =
  let x' = subst-rename-var-if Γ ρ x σ in
    KndPi posinfo-gen posinfo-gen x' (substh-tk Γ ρ σ atk)
      (substh-kind (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ k)
substh-kind Γ ρ σ (KndTpArrow t k) = KndTpArrow (substh-type Γ ρ σ t) (substh-kind Γ ρ σ k)
substh-kind{QUALIF} Γ ρ σ (KndVar _ x xs) =
   qualif-lookup-kind (substh-args Γ ρ σ xs) σ x
substh-kind Γ ρ σ (KndVar _ x xs) = KndVar posinfo-gen x (substh-args Γ ρ σ xs)
substh-kind Γ ρ σ (Star _) = Star posinfo-gen

substh-arg Γ ρ σ (TermArg me t) = TermArg me (substh-term Γ ρ σ t)
substh-arg Γ ρ σ (TypeArg T) = TypeArg (substh-type Γ ρ σ T)

substh-args Γ ρ σ (ArgsCons a as) = ArgsCons (substh-arg Γ ρ σ a) (substh-args Γ ρ σ as)
substh-args Γ ρ σ ArgsNil = ArgsNil

substh-params{QUALIF} Γ ρ σ (ParamsCons (Decl _ pi me x atk _) ps) =
  ParamsCons (Decl posinfo-gen posinfo-gen me (pi % x) (substh-tk Γ ρ σ atk) posinfo-gen)
    (substh-params Γ (renamectxt-insert ρ x (pi % x)) (trie-remove σ (pi % x)) ps)
substh-params Γ ρ σ (ParamsCons (Decl _ _ me x atk _) ps) =
  ParamsCons (Decl posinfo-gen posinfo-gen me x (substh-tk Γ ρ σ atk) posinfo-gen)
    (substh-params Γ (renamectxt-insert ρ x x) (trie-remove σ x) ps)
substh-params Γ ρ σ ParamsNil = ParamsNil

substh-tk Γ ρ σ (Tkk k) = Tkk (substh-kind Γ ρ σ k)
substh-tk Γ ρ σ (Tkt t) = Tkt (substh-type Γ ρ σ t)

substh-optClass Γ ρ σ NoClass = NoClass
substh-optClass Γ ρ σ (SomeClass atk) = SomeClass (substh-tk Γ ρ σ atk)
substh-liftingType Γ ρ σ (LiftArrow l l₁) = LiftArrow (substh-liftingType Γ ρ σ l) (substh-liftingType Γ ρ σ l₁)
substh-liftingType Γ ρ σ (LiftParens _ l _) = substh-liftingType Γ ρ σ l
substh-liftingType Γ ρ σ (LiftPi _ x tp l) =
  let x' = subst-rename-var-if Γ ρ x σ in
    LiftPi posinfo-gen x' (substh-type Γ ρ σ tp)
       (substh-liftingType (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ l)
substh-liftingType Γ ρ σ (LiftStar _) = LiftStar posinfo-gen
substh-liftingType Γ ρ σ (LiftTpArrow tp l) =
  LiftTpArrow (substh-type Γ ρ σ tp) (substh-liftingType Γ ρ σ l)

substh-optType Γ ρ σ NoType = NoType
substh-optType Γ ρ σ (SomeType T) = SomeType (substh-type Γ ρ σ T)

substh-optTerm Γ ρ σ NoTerm = NoTerm
substh-optTerm Γ ρ σ (SomeTerm t _) = (SomeTerm (substh-term Γ ρ σ t) posinfo-gen)

substh-optGuide Γ ρ σ NoGuide = NoGuide
substh-optGuide Γ ρ σ (Guide _ x T) =
  let x' = subst-rename-var-if Γ ρ x σ in
  Guide posinfo-gen x' (substh-type (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') σ T)

subst-ret-t : Set → Set
subst-ret-t T = {ed : exprd} → ctxt → ⟦ ed ⟧ → var → T → T

subst : ∀ {ed} → subst-ret-t ⟦ ed ⟧
subst Γ t x = substh Γ empty-renamectxt (trie-single x t)

subst-term = subst {TERM}
subst-type = subst {TYPE}
subst-kind = subst {KIND}
subst-liftingType = subst {LIFTINGTYPE}
subst-tk = subst {TK}

subst-renamectxt : ∀ {ed : exprd} → ctxt → renamectxt → ⟦ ed ⟧ → ⟦ ed ⟧
subst-renamectxt {ed} Γ ρ = substh {ed} {ed} Γ ρ empty-trie

rename-var : ∀ {ed} → ctxt → var → var → ⟦ ed ⟧ → ⟦ ed ⟧
rename-var Γ x x' = subst-renamectxt Γ (renamectxt-single x x')

substs-ret-t : Set → Set
substs-ret-t T = ∀ {ed} → ctxt → trie ⟦ ed ⟧ → T → T

substs : ∀ {ed} → substs-ret-t ⟦ ed ⟧
substs Γ = substh Γ empty-renamectxt

substs-term = substs {TERM}
substs-type = substs {TYPE}
substs-kind = substs {KIND}
substs-liftingType = substs {LIFTINGTYPE}
substs-tk = substs {TK}

substs-args : substs-ret-t args
substs-args Γ = substh-args Γ empty-renamectxt

substs-params : substs-ret-t params
substs-params Γ = substh-params Γ empty-renamectxt

subst-params-args : ∀ {ed} → ctxt → params → args → ⟦ ed ⟧ → ⟦ ed ⟧ × params × args
subst-params-args Γ (ParamsCons (Decl _ _ me x atk _) ps) (ArgsCons a as) t =
  subst-params-args Γ (substs-params Γ (trie-single x a) ps) as (subst Γ a x t)
subst-params-args Γ ps as t = t , ps , as

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module Iff where

infix 20 _⇔_
record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A


text:
module Data.BitVector.Peano where

open import Data.BitVector
open import Algebra.FunctionProperties.Core
open import Data.Nat hiding (pred) renaming (suc to Nsuc; zero to Nzero)
open import Data.Vec hiding (fromList)
open import Relation.Binary.PropositionalEquality

open import Data.Digit hiding (Bit)
open import Data.Fin using () renaming (zero to Fzero; suc to Fsuc)
open import Data.List
open import Data.Product

suc : ∀ {n} → Op₁ (BitVector n)
suc [] = []
suc (0# ∷ xs) = 1# ∷ xs
suc (1# ∷ xs) = 0# ∷ suc xs

pred-helper : ∀ {n} → BitVector n → BitVector (Nsuc n)
pred-helper [] = 1# ∷ []
pred-helper (0# ∷ xs) = 1# ∷ pred-helper xs
pred-helper (1# ∷ xs) = 1# ∷ 0# ∷ xs

pred : ∀ {n} → Op₁ (BitVector n)
pred [] = []
pred (1# ∷ xs) = 0# ∷ xs
pred (0# ∷ xs) = pred-helper xs

suc∘pred-helper≡0# : ∀ {n} (x : BitVector n) → suc (pred-helper x) ≡ 0# ∷ x
suc∘pred-helper≡0# [] = refl
suc∘pred-helper≡0# (0# ∷ xs) = cong (_∷_ 0#) (suc∘pred-helper≡0# xs)
suc∘pred-helper≡0# (1# ∷ xs) = refl

pred-helper∘suc≡1# : ∀ {n} (x : BitVector n) → pred-helper (suc x) ≡ 1# ∷ x
pred-helper∘suc≡1# [] = refl
pred-helper∘suc≡1# (0# ∷ xs) = refl
pred-helper∘suc≡1# (1# ∷ xs) = cong (_∷_ 1#) (pred-helper∘suc≡1# xs)

suc∘pred≡id : ∀ {n} (x : BitVector n) → suc (pred x) ≡ x
suc∘pred≡id [] = refl
suc∘pred≡id (0# ∷ xs) = suc∘pred-helper≡0# xs
suc∘pred≡id (1# ∷ xs) = refl

pred∘suc≡id : ∀ {n} (x : BitVector n) → pred (suc x) ≡ x
pred∘suc≡id [] = refl
pred∘suc≡id (0# ∷ xs) = refl
pred∘suc≡id (1# ∷ xs) = pred-helper∘suc≡1# xs

data Peano : ∀ {n} → BitVector n → Set where
  Pzero : ∀ {n} → Peano (zero n)
  Psuc  : ∀ {n} {x : BitVector n} → (p : Peano x) → Peano (suc x)

Pdouble : ∀ {n} {x : BitVector n} → Peano x → Peano (0# ∷ x)
Pdouble Pzero = Pzero
Pdouble (Psuc p) = Psuc (Psuc (Pdouble p))

toPeano : ∀ {n} (x : BitVector n) → Peano x
toPeano [] = Pzero
toPeano (0# ∷ xs) = Pdouble (toPeano xs)
toPeano (1# ∷ xs) = Psuc (Pdouble (toPeano xs))

peanoInduction : ∀ {n} → (P : ∀ {x : BitVector n} → Peano x → Set) → P Pzero
               → (∀ {x : BitVector n} {m : Peano x} → P m → P (Psuc m))
               → ∀ {x : BitVector n} (q : Peano x) → P q
peanoInduction P z s Pzero = z
peanoInduction P z s (Psuc p) = s {_} {p} (peanoInduction P z s p)

induction : ∀ {n} (P : BitVector n → Set) → P (zero n)
          → (∀ {m} → P m → P (suc m)) → ∀ x → P x
induction P z s x = peanoInduction (λ {x} _ → P x) z s (toPeano x)

toℕ : ∀ {n} → BitVector n → ℕ
toℕ = induction _ 0 Nsuc

fromDigit : Digit 2 → Bit
fromDigit Fzero = 0#
fromDigit (Fsuc Fzero) = 1#
fromDigit (Fsuc (Fsuc ()))

fromList : ∀ {n} → List (Digit 2) → BitVector n
fromList [] = zero _
fromList {Nzero} (x ∷ xs) = []
fromList {Nsuc n} (x ∷ xs) = fromDigit x ∷ fromList xs

fromℕ : ∀ {n} → ℕ → BitVector n
fromℕ n with toDigits 2 n
fromℕ .(fromDigits ds) | ds , refl = fromList ds

-- TODO: the terrifying proofs that toℕ and fromℕ are inverses

max_stars_repo_name: copumpkin/bitvector

max_issues_repo_name: copumpkin/bitvector

max_forks_repo_name: copumpkin/bitvector


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle
open        EpochConfig
open import LibraBFT.Yasm.Base ℓ-RoundManager

-- In this module, we instantiate the system model with parameters to
-- model a system using the simple implementation model we have so
-- far, which aims to obey the VotesOnceRule, but not PreferredRoundRule
-- yet.  This will evolve as we build out a model of a real
-- implementation.

module LibraBFT.Concrete.System.Parameters where
 ConcSysParms : SystemParameters
 ConcSysParms = mkSysParms
                 NodeId
                 _≟NodeId_
                 GenesisInfo
                 genInfo
                 RoundManager
                 initRM
                 NetworkMsg
                 Vote
                 sig-Vote
                 _⊂Msg_
                 ∈GenInfo
                 initWrapper
                 peerStep

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --no-unicode #-}

open import Agda.Builtin.Nat

pred : Nat -> Nat
pred = \ { n -> {!!} }

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module SizedPoly.Console where

open import SizedPolyIO.Base
open import SizedPolyIO.Console hiding (main)

open import NativePolyIO

open import Level using () renaming (zero to lzero)

{-# TERMINATING #-}
myProgram  :  ∀{i} → IOConsole i (Unit {lzero})
myProgram  =  exec  getLine          λ line →
              exec  (putStrLn line)  λ _ →
              exec  (putStrLn line)  λ _ →
              myProgram

main  :  NativeIO Unit
main  =  translateIOConsole myProgram

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

open import Definition.Typed.EqualityRelation

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

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

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

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

  -- Transitivty of type equality.
  transEq : ∀ {Γ A B C l l′ l″}
            ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B) ([C] : Γ ⊩⟨ l″ ⟩ C)
          → Γ ⊩⟨ l ⟩  A ≡ B / [A]
          → Γ ⊩⟨ l′ ⟩ B ≡ C / [B]
          → Γ ⊩⟨ l ⟩  A ≡ C / [A]
  transEq [A] [B] [C] A≡B B≡C =
    transEqT (combine (goodCases [A] [B] A≡B) (goodCases [B] [C] B≡C)) A≡B B≡C

  -- Transitivty of type equality with some propositonally equal types.
  transEq′ : ∀ {Γ A B B′ C C′ l l′ l″} → B PE.≡ B′ → C PE.≡ C′
           → ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B) ([C] : Γ ⊩⟨ l″ ⟩ C)
           → Γ ⊩⟨ l ⟩  A ≡ B′ / [A]
           → Γ ⊩⟨ l′ ⟩ B ≡ C′ / [B]
           → Γ ⊩⟨ l ⟩  A ≡ C  / [A]
  transEq′ PE.refl PE.refl [A] [B] [C] A≡B B≡C = transEq [A] [B] [C] A≡B B≡C

transEqTermNe : ∀ {Γ n n′ n″ A}
              → Γ ⊩neNf n  ≡ n′  ∷ A
              → Γ ⊩neNf n′ ≡ n″ ∷ A
              → Γ ⊩neNf n  ≡ n″ ∷ A
transEqTermNe (neNfₜ₌ neK neM k≡m) (neNfₜ₌ neK₁ neM₁ k≡m₁) =
  neNfₜ₌ neK neM₁ (~-trans k≡m k≡m₁)

mutual
  transEqTermℕ : ∀ {Γ n n′ n″}
               → _⊩ℕ_≡_∷ℕ Γ n n′
               → _⊩ℕ_≡_∷ℕ Γ n′ n″
               → _⊩ℕ_≡_∷ℕ Γ n n″
  transEqTermℕ (ℕₜ₌ k k′ d d′ t≡u prop)
               (ℕₜ₌ k₁ k″ d₁ d″ t≡u₁ prop₁) =
    let k₁Whnf = naturalWhnf (proj₁ (split prop₁))
        k′Whnf = naturalWhnf (proj₂ (split prop))
        k₁≡k′ = whrDet*Term (redₜ d₁ , k₁Whnf) (redₜ d′ , k′Whnf)
        prop′ = PE.subst (λ x → [Natural]-prop _ x _) k₁≡k′ prop₁
    in  ℕₜ₌ k k″ d d″ (≅ₜ-trans t≡u (PE.subst (λ x → _ ⊢ x ≅ _ ∷ _) k₁≡k′ t≡u₁))
            (transNatural-prop prop prop′)

  transNatural-prop : ∀ {Γ k k′ k″}
                    → [Natural]-prop Γ k k′
                    → [Natural]-prop Γ k′ k″
                    → [Natural]-prop Γ k k″
  transNatural-prop (sucᵣ x) (sucᵣ x₁) = sucᵣ (transEqTermℕ x x₁)
  transNatural-prop (sucᵣ x) (ne (neNfₜ₌ () neM k≡m))
  transNatural-prop zeroᵣ prop₁ = prop₁
  transNatural-prop prop zeroᵣ = prop
  transNatural-prop (ne (neNfₜ₌ neK () k≡m)) (sucᵣ x₃)
  transNatural-prop (ne [k≡k′]) (ne [k′≡k″]) =
    ne (transEqTermNe [k≡k′] [k′≡k″])

-- Transitivty of term equality.
transEqTerm : ∀ {l Γ A t u v}
              ([A] : Γ ⊩⟨ l ⟩ A)
            → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
            → Γ ⊩⟨ l ⟩ u ≡ v ∷ A / [A]
            → Γ ⊩⟨ l ⟩ t ≡ v ∷ A / [A]
transEqTerm (Uᵣ′ .⁰ 0<1 ⊢Γ)
            (Uₜ₌ A B d d′ typeA typeB t≡u [t] [u] [t≡u])
            (Uₜ₌ A₁ B₁ d₁ d₁′ typeA₁ typeB₁ t≡u₁ [t]₁ [u]₁ [t≡u]₁)
            rewrite whrDet*Term (redₜ d′ , typeWhnf typeB) (redₜ d₁ , typeWhnf typeA₁) =
  Uₜ₌ A B₁ d d₁′ typeA typeB₁ (≅ₜ-trans t≡u t≡u₁) [t] [u]₁
      (transEq [t] [u] [u]₁ [t≡u] (irrelevanceEq [t]₁ [u] [t≡u]₁))
transEqTerm (ℕᵣ D) (ιx [t≡u]) (ιx [u≡v]) = ιx (transEqTermℕ [t≡u] [u≡v])
transEqTerm (ne′ K D neK K≡K) (ιx (neₜ₌ k m d d′ (neNfₜ₌ neK₁ neM k≡m)))
                              (ιx (neₜ₌ k₁ m₁ d₁ d″ (neNfₜ₌ neK₂ neM₁ k≡m₁))) =
  let k₁≡m = whrDet*Term (redₜ d₁ , ne neK₂) (redₜ d′ , ne neM)
  in ιx (neₜ₌ k m₁ d d″
           (neNfₜ₌ neK₁ neM₁
                   (~-trans k≡m (PE.subst (λ x → _ ⊢ x ~ _ ∷ _) k₁≡m k≡m₁))))
transEqTerm (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g])
            (Πₜ₌ f₁ g₁ d₁ d₁′ funcF₁ funcG₁ f≡g₁ [f]₁ [g]₁ [f≡g]₁)
            rewrite whrDet*Term (redₜ d′ , functionWhnf funcG)
                            (redₜ d₁ , functionWhnf funcF₁) =
  Πₜ₌ f g₁ d d₁′ funcF funcG₁ (≅ₜ-trans f≡g f≡g₁) [f] [g]₁
      (λ ρ ⊢Δ [a] → transEqTerm ([G] ρ ⊢Δ [a])
                                ([f≡g] ρ ⊢Δ [a])
                                ([f≡g]₁ ρ ⊢Δ [a]))
transEqTerm (emb′ 0<1 x) (ιx t≡u) (ιx u≡v) = ιx (transEqTerm x t≡u u≡v)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt