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

-- I've been spinning my wheels quite a bit on this proof.

-- I've chatted with several people and feel confident my
-- functions are properly defined, but I'm really struggling
-- to see how to prove they are quasi-inverses (it has been a little
-- reassuring, no one I have talked to has correctly defined
-- the functions initially, hah).

-- At the moment I'm not sure if I'm just missing something obvious in
-- the proof, or if I'm simply going about the proof wrong. I've
-- begun focusing on the eckmann-hilton proof and plan to return to this
-- after that is done.

module Circle where

open import Level using (_⊔_)
open import Data.Product using (Σ; _,_)
open import Function renaming (_∘_ to _○_)
--open import Relation.Binary.PropositionalEquality renaming (_≡_ to _≡_; refl to Eqrefl)
--open import Relation.Binary.EqReasoning

infixr 8  _∘_     -- path composition
infix  4  _≡_     -- propositional equality
infix  4  _∼_     -- homotopy between two functions
infix  4  _≃_     -- type of equivalences
-- macros from tzaikin for equational rewriting over non-standard ≡
infixr 4 _≡⟨_⟩_
infix 4  _∎

------------------------------------------------------------------------------
-- A few HoTT primitives

data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
  refl : (a : A) → (a ≡ a)

pathInd : ∀ {u ℓ} → {A : Set u} →
          (C : {x y : A} → x ≡ y → Set ℓ) →
          (c : (x : A) → C (refl x)) →
          ({x y : A} (p : x ≡ y) → C p)
pathInd C c (refl x) = c x

-- inverse paths
! : ∀ {u} → {A : Set u} {x y : A} → (x ≡ y) → (y ≡ x)
! = pathInd (λ {x} {y} _ → y ≡ x) refl

-- path composition
_∘_ : ∀ {u} → {A : Set u} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_∘_ {u} {A} {x} {y} {z} p q =
  pathInd {u}
    (λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (λ x z q → pathInd (λ {x} {z} _ → x ≡ z) refl {x} {z} q)
    {x} {y} p z q

-- Handy "macros" (from tzaikin)
_∎ : {A : Set} → (p : A) → p ≡ p
p ∎ = refl p

_≡⟨_⟩_ : {A : Set} → {q r : A} → (p : A) → p ≡ q → q ≡ r → p ≡ r
p ≡⟨ α ⟩ β = α ∘ β

-- (x ≡ y) ≡ ((x ≡ y) ∘ (refl y))
unitTransR : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ (p ∘ refl y))
unitTransR {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ (p ∘ (refl y)))
    (λ x → refl (refl x))
    {x} {y} p

-- (x ≡ y) ≡ ((refl x) ∘ (x ≡ y))
unitTransL : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x ∘ p)
unitTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ (refl x) ∘ p)
    (λ x → refl (refl x))
    {x} {y} p

-- !(x ≡ y) ∘ (x ≡ y)  ≡ (refl y)
invTransL : {A : Set} {x y : A} → (p : x ≡ y) → (! p ∘ p ≡ refl y)
invTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! p ∘ p ≡ refl y)
    (λ x → refl (refl x))
    {x} {y} p

--  (x ≡ y) ∘ !(x ≡ y)  ≡ (refl x)
invTransR : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → (p ∘ ! p ≡ refl x)
invTransR {ℓ} {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ∘ ! p ≡ refl x)
    (λ x → refl (refl x))
    {x} {y} p

-- !!(x ≡ y) ≡ (x ≡ y)
invId : {A : Set} {x y : A} → (p : x ≡ y) → (! (! p) ≡ p)
invId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! (! p) ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

-- (x ≡ y) and (y ≡ z) ⇒ (x ≡ z)
assocP : {A : Set} {x y z w : A} → (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) →
         (p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
assocP {A} {x} {y} {z} {w} p q r =
  pathInd
    (λ {x} {y} p → (z : A) → (w : A) → (q : y ≡ z) → (r : z ≡ w) →
      p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
    (λ x z w q r →
      pathInd
        (λ {x} {z} q → (w : A) → (r : z ≡ w) →
          (refl x) ∘ (q ∘ r) ≡ ((refl x) ∘ q) ∘ r)
        (λ x w r →
          pathInd
            (λ {x} {w} r →
              (refl x) ∘ ((refl x) ∘ r) ≡
              ((refl x) ∘ (refl x)) ∘ r)
            (λ x → (refl (refl x)))
            {x} {w} r)
        {x} {z} q w r)
    {x} {y} p z w q r

-- !(p ∘ q) ≡ !q ∘ !p
invComp : {A : Set} {x y z : A} → (p : x ≡ y) → (q : y ≡ z) →
          ! (p ∘ q) ≡ ! q ∘ ! p
invComp {A} {x} {y} {z} p q =
  pathInd
    (λ {x} {y} p → (z : A) → (q : y ≡ z) → ! (p ∘ q) ≡ ! q ∘ ! p)
    (λ x z q →
      pathInd
        (λ {x} {z} q → ! (refl x ∘ q) ≡ ! q ∘ ! (refl x))
        (λ x → refl (refl x))
        {x} {z} q)
    {x} {y} p z q

-- (x ≡ y) ⇒ (f x) ≡ (f y)
ap : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {x y : A} →
     (f : A → B) → (x ≡ y) → (f x ≡ f y)
ap {ℓ} {ℓ'} {A} {B} {x} {y} f p =
  pathInd
    (λ {x} {y} p → f x ≡ f y)
    (λ x → refl (f x))
    {x} {y} p

-- sort of
-- p:(x ≡ y) ⇒ q:(y ≡ z) ⇒ (((f x) ≡ (f z)) ≡ (((f x) ≡ (f y)) ∘ ((f y) ≡ (f z))))
apfTrans : ∀ {u} → {A B : Set u} {x y z : A} →
  (f : A → B) → (p : x ≡ y) → (q : y ≡ z) → ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q)
apfTrans {u} {A} {B} {x} {y} {z} f p q =
  pathInd {u}
    (λ {x} {y} p → (z : A) → (q : y ≡ z) →
      ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q))
    (λ x z q →
      pathInd {u}
        (λ {x} {z} q →
          ap f (refl x ∘ q) ≡ (ap f (refl x)) ∘ (ap f q))
        (λ x → refl (refl (f x)))
        {x} {z} q)
    {x} {y} p z q

-- ap f (! p) ≡ ! (ap f p)
apfInv : ∀ {u} → {A B : Set u} {x y : A} → (f : A → B) → (p : x ≡ y) →
         ap f (! p) ≡ ! (ap f p)
apfInv {u} {A} {B} {x} {y} f p =
  pathInd {u}
    (λ {x} {y} p → ap f (! p) ≡ ! (ap f p))
    (λ x → refl (ap f (refl x)))
    {x} {y} p

-- ap g (ap f p) ≡ ap (g ○ f) p
apfComp : {A B C : Set} {x y : A} → (f : A → B) → (g : B → C) → (p : x ≡ y) →
          ap g (ap f p) ≡ ap (g ○ f) p
apfComp {A} {B} {C} {x} {y} f g p =
  pathInd
    (λ {x} {y} p → ap g (ap f p) ≡ ap (g ○ f) p)
    (λ x → refl (ap g (ap f (refl x))))
    {x} {y} p

--  ap id p ≡ p
apfId : {A : Set} {x y : A} → (p : x ≡ y) → ap id p ≡ p
apfId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ap id p ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

--  (x ≡ y) → P x → P y
transport : ∀ {ℓ ℓ'} → {A : Set ℓ} {x y : A} →
  (P : A → Set ℓ') → (p : x ≡ y) → P x → P y
transport {ℓ} {ℓ'} {A} {x} {y} P p =
  pathInd -- on p
    (λ {x} {y} p → (P x → P y))
    (λ _ → id)
    {x} {y} p

-- dependent ap
apd : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : A → Set ℓ'} {x y : A} → (f : (a : A) → B a) →
  (p : x ≡ y) → (transport B p (f x) ≡ f y)
apd {ℓ} {ℓ'} {A} {B} {x} {y} f p =
  pathInd
    (λ {x} {y} p → transport B p (f x) ≡ f y)
    (λ x → refl (f x))
    {x} {y} p

-- Homotopies and equivalences

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f ○ g) ∼ id
    β : (g ○ f) ∼ id

record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkisequiv
  field
    g : B → A
    α : (f ○ g) ∼ id
    h : B → A
    β : (h ○ f) ∼ id

equiv₁ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f
equiv₁ (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) isequiv

postulate
  univalence : {A B : Set} → (A ≡ B) ≃ (A ≃ B)

------------------------------------------------------------------------------
-- Exercise: let's show that the following two definitions of the
-- circle are "the same"

module Circle1 where
  private
    data S¹* : Set where
      base* : S¹*

  S¹ : Set
  S¹ = S¹*

  base : S¹
  base = base*

  postulate
    loop : base ≡ base

  recS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) → S¹ → C
  recS¹ cbase cloop base* = cbase

  postulate
    βrecS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) →
      ap (recS¹ cbase cloop) loop ≡ cloop

  indS¹ : {C : S¹ → Set} →
    (cbase : C base) → (cloop : transport C loop cbase ≡ cbase) →
    (circle : S¹) → C circle
  indS¹ cbase cloop base* = cbase

  postulate
    βindS¹ : {C : S¹ → Set} →
      (cbase : C base) → (cloop : transport C loop cbase ≡ cbase) →
      apd (indS¹ {C} cbase cloop) loop ≡ cloop

open Circle1 public

module Circle2 where
  private
    data S¹'* : Set where
      south* : S¹'*
      north* : S¹'*

  S¹' : Set
  S¹' = S¹'*

  south : S¹'
  south = south*

  north : S¹'
  north = north*

  postulate
    east : south ≡ north
    west : south ≡ north

  recS¹' : {C : Set} →
    (csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) → S¹' → C
  recS¹' csouth cnorth ceast cwest south* = csouth
  recS¹' csouth cnorth ceast cwest north* = cnorth

  postulate
    βreceastS¹' : {C : Set} →
      (csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) →
      ap (recS¹' csouth cnorth ceast cwest) east ≡ ceast
    βrecwestS¹' : {C : Set} →
      (csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) →
      ap (recS¹' csouth cnorth ceast cwest) west ≡ cwest

  indS¹' : {C : S¹' → Set} →
    (csouth : C south) → (cnorth : C north) →
    (ceast : transport C east csouth ≡ cnorth) →
    (cwest : transport C west csouth ≡ cnorth) →
    (circle : S¹') → C circle
  indS¹' csouth cnorth ceast cwest south* = csouth
  indS¹' csouth cnorth ceast cwest north* = cnorth

  postulate
    βindeastS¹' : {C : S¹' → Set} →
      (csouth : C south) → (cnorth : C north) →
      (ceast : transport C east csouth ≡ cnorth) →
      (cwest : transport C west csouth ≡ cnorth) →
      apd (indS¹' {C} csouth cnorth ceast cwest) east ≡ ceast
    βindwestS¹' : {C : S¹' → Set} →
      (csouth : C south) → (cnorth : C north) →
      (ceast : transport C east csouth ≡ cnorth) →
      (cwest : transport C west csouth ≡ cnorth) →
      apd (indS¹' {C} csouth cnorth ceast cwest) west ≡ cwest

open Circle2 public

Smap : S¹ → S¹'
Smap s = recS¹ south (west ∘ (! east)) s

S'map : S¹' → S¹
S'map s = recS¹' {C = S¹} base base (refl base) loop s

S'toS≡id : S¹' -> Set
S'toS≡id = (λ s' → (Smap ○ S'map) s' ≡ id s')

StoS'≡id : S¹ -> Set
StoS'≡id = (λ s → (S'map ○ Smap) s ≡ id s)

Sqinv : qinv Smap
Sqinv = mkqinv S'map
               -- P(s') = (Smap ○ S'map) s' ≡ id s'
               (indS¹'
                 {C = S'toS≡id}
                 (refl south)
                 (transport S'toS≡id east (refl south))
                 ((refl (transport S'toS≡id east (refl south))))
                 -- I've spent several hours exploring how I might
                 -- prove this and I'm completely lost.
                 -- I must be missing something obvious or I'm going about this
                 -- totally wrong =\
                 (transport S'toS≡id west (refl south) ≡⟨ {!!} ⟩
                  transport S'toS≡id east (refl south) ∎))
               -- P(s) = (S'map ○ Smap) s ≡ id s
               (indS¹
                 {C = (λ s → (S'map ○ Smap) s ≡ id s)} -- P
                 (refl base) -- P(base)
                 -- P()
                 (transport StoS'≡id loop (refl base) ≡⟨ {!!} ⟩ -- needs Thm 2.11.3, transportId
                  refl base ∎)) -- ap E x≡y where E is a context allows you to rewrite
sequiv : S¹ ≃ S¹'               -- any E[x] to E[y]
sequiv = (Smap , equiv₁ Sqinv)

spath : S¹ ≡ S¹'
spath with univalence
... | (_ , eq) = isequiv.g eq sequiv

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

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


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

module Definition.Typed.Weakening where

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed

import Tools.PropositionalEquality as PE

-- Weakening type

data _∷_⊆_ : Wk → Con Term → Con Term → Set where
  id   : ∀ {Γ}       → id ∷ Γ ⊆ Γ
  step : ∀ {Γ Δ A r ρ} → ρ  ∷ Δ ⊆ Γ → step ρ ∷ Δ ∙ A ^ r ⊆ Γ
  lift : ∀ {Γ Δ A r ρ} → ρ  ∷ Δ ⊆ Γ → lift ρ ∷ Δ ∙ U.wk ρ A ^ r ⊆ Γ ∙ A ^ r

-- -- Weakening composition

_•ₜ_ : ∀ {ρ ρ′ Γ Δ Δ′} → ρ ∷ Γ ⊆ Δ → ρ′ ∷ Δ ⊆ Δ′ → ρ • ρ′ ∷ Γ ⊆ Δ′
id     •ₜ η′ = η′
step η •ₜ η′ = step (η •ₜ η′)
lift η •ₜ id = lift η
lift η •ₜ step η′ = step (η •ₜ η′)
_•ₜ_ {lift ρ} {lift ρ′} {Δ′ = Δ′ ∙ A ^ rA} (lift η) (lift η′) =
  PE.subst (λ x → lift (ρ • ρ′) ∷ x ⊆ Δ′ ∙ A ^ rA)
           (PE.cong₂ (λ x y → x ∙ y ^ rA) PE.refl (PE.sym (wk-comp ρ ρ′ A)))
           (lift (η •ₜ η′))

-- Weakening of judgements

wkIndex : ∀ {Γ Δ n A r ρ} → ρ ∷ Δ ⊆ Γ →
        let ρA = U.wk ρ A
            ρn = wkVar ρ n
        in  ⊢ Δ → n ∷ A ^ r ∈ Γ → ρn ∷ ρA ^ r ∈ Δ
wkIndex id ⊢Δ i = PE.subst (λ x → _ ∷ x ^ _ ∈ _) (PE.sym (wk-id _)) i
wkIndex (step ρ) (⊢Δ ∙ A) i = PE.subst (λ x → _ ∷ x ^ _ ∈ _)
                                       (wk1-wk _ _)
                                       (there (wkIndex ρ ⊢Δ i))
wkIndex (lift ρ) (⊢Δ ∙ A) (there i) = PE.subst (λ x → _ ∷ x ^ _ ∈ _)
                                               (wk1-wk≡lift-wk1 _ _)
                                               (there (wkIndex ρ ⊢Δ i))
wkIndex (lift ρ) ⊢Δ here =
  let G = _
      n = _
  in  PE.subst (λ x → n ∷ x ^ _ ∈ G)
               (wk1-wk≡lift-wk1 _ _)
               here

mutual
  wk : ∀ {Γ Δ A r ρ} → ρ ∷ Δ ⊆ Γ →
     let ρA = U.wk ρ A
     in  ⊢ Δ → Γ ⊢ A ^ r → Δ ⊢ ρA ^ r
  wk ρ ⊢Δ (Uⱼ ⊢Γ) = Uⱼ ⊢Δ
  wk ρ ⊢Δ (univ A) = univ (wkTerm ρ ⊢Δ A)

  wkTerm : ∀ {Γ Δ A t r ρ} → ρ ∷ Δ ⊆ Γ →
         let ρA = U.wk ρ A
             ρt = U.wk ρ t
         in ⊢ Δ → Γ ⊢ t ∷ A ^ r → Δ ⊢ ρt ∷ ρA ^ r
  wkTerm ρ ⊢Δ (univ <l ⊢Γ) = univ <l ⊢Δ
  wkTerm ρ ⊢Δ (ℕⱼ ⊢Γ) = ℕⱼ ⊢Δ
  wkTerm ρ ⊢Δ (Emptyⱼ ⊢Γ) = Emptyⱼ ⊢Δ
  wkTerm ρ ⊢Δ (Πⱼ <l ▹ <l' ▹ F ▹ G) = let ρF = wkTerm ρ ⊢Δ F
                                      in  Πⱼ <l ▹ <l' ▹ ρF ▹ (wkTerm (lift ρ) (⊢Δ ∙ univ ρF) G)
  wkTerm ρ ⊢Δ (∃ⱼ F ▹ G) = let ρF = wkTerm ρ ⊢Δ F
                          in  ∃ⱼ ρF ▹ (wkTerm (lift ρ) (⊢Δ ∙ univ ρF) G)
  wkTerm ρ ⊢Δ (var ⊢Γ x) = var ⊢Δ (wkIndex ρ ⊢Δ x)
  wkTerm ρ ⊢Δ (lamⱼ <l <l' F t) = let ρF = wk ρ ⊢Δ F
                                  in lamⱼ <l <l' ρF (wkTerm (lift ρ) (⊢Δ ∙ ρF) t)
  wkTerm ρ ⊢Δ (_∘ⱼ_ {G = G} g a) = PE.subst (λ x → _ ⊢ _ ∷ x ^ _)
                                           (PE.sym (wk-β G))
                                           (wkTerm ρ ⊢Δ g ∘ⱼ wkTerm ρ ⊢Δ a)
  wkTerm ρ ⊢Δ (⦅_,_,_,_⦆ⱼ {G = GG} F G t u )
    = let ρF = wk ρ ⊢Δ F in ⦅ wk ρ ⊢Δ F , wk (lift ρ) (⊢Δ ∙ ρF) G , wkTerm ρ ⊢Δ t ,  PE.subst (λ X → _ ⊢ _ ∷ X ^ [ % , _ ]) (wk-β GG) (wkTerm ρ ⊢Δ u) ⦆ⱼ
  wkTerm ρ ⊢Δ (fstⱼ F G t) = let ρF = wkTerm ρ ⊢Δ F in
    let ρG = (wkTerm (lift ρ) (⊢Δ ∙ univ ρF) G) in
    fstⱼ ρF ρG (wkTerm ρ ⊢Δ t)
  wkTerm ρ ⊢Δ (sndⱼ {G = G} F Gⱼ t) = let ρF = wkTerm ρ ⊢Δ F in
    let ρG = (wkTerm (lift ρ) (⊢Δ ∙ univ ρF) Gⱼ) in
    PE.subst (λ X → _ ⊢ _ ∷ X ^ [ % , _ ]) (PE.sym (wk-β G)) (sndⱼ ρF ρG (wkTerm ρ ⊢Δ t))
  wkTerm ρ ⊢Δ (zeroⱼ ⊢Γ) = zeroⱼ ⊢Δ
  wkTerm ρ ⊢Δ (sucⱼ n) = sucⱼ (wkTerm ρ ⊢Δ n)
  wkTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrecⱼ {G = G} {rG = rG} {lG = lG}  {s = s} ⊢G ⊢z ⊢s ⊢n) =
    PE.subst (λ x → _ ⊢ natrec _ _ _ _ _ ∷ x ^ _) (PE.sym (wk-β G))
             (natrecⱼ (wk (lift [ρ]) (⊢Δ ∙ univ (ℕⱼ ⊢Δ)) ⊢G)
                      (PE.subst (λ x → _ ⊢ _ ∷ x ^ _) (wk-β G) (wkTerm [ρ] ⊢Δ ⊢z))
                      (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x ^ [ rG , ι lG ])
                                (wk-β-natrec ρ G rG lG)
                                (wkTerm [ρ] ⊢Δ ⊢s))
                      (wkTerm [ρ] ⊢Δ ⊢n))
  wkTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (Emptyrecⱼ {A = A} {e = e} ⊢A ⊢e) =
    (Emptyrecⱼ (wk [ρ] ⊢Δ ⊢A) (wkTerm [ρ] ⊢Δ ⊢e))
  wkTerm ρ ⊢Δ (Idⱼ A t u) = Idⱼ (wkTerm ρ ⊢Δ A) (wkTerm ρ ⊢Δ t) (wkTerm ρ ⊢Δ u)
  wkTerm ρ ⊢Δ (Idreflⱼ t) = Idreflⱼ (wkTerm ρ ⊢Δ t)
  wkTerm ρ ⊢Δ (transpⱼ {P = P} A Pⱼ t s u e) =
    let ρA = wk ρ ⊢Δ A in
    let ρP = wk (lift ρ) (⊢Δ ∙ ρA) Pⱼ in
    let ρt = wkTerm ρ ⊢Δ t in
    let ρs = PE.subst (λ x → _ ⊢ _ ∷ x ^ _) (wk-β P) (wkTerm ρ ⊢Δ s) in
    let ρu = wkTerm ρ ⊢Δ u in
    let ρe = wkTerm ρ ⊢Δ e in
    PE.subst (λ x → _ ⊢ transp _ _ _ _ _ _ ∷ x ^ _) (PE.sym (wk-β P))
      (transpⱼ ρA ρP ρt ρs ρu ρe)
  wkTerm ρ ⊢Δ (castⱼ A B e t) =
    castⱼ (wkTerm ρ ⊢Δ A) (wkTerm ρ ⊢Δ B) (wkTerm ρ ⊢Δ e) (wkTerm ρ ⊢Δ t)
  wkTerm ρ ⊢Δ (castreflⱼ A t) =
    castreflⱼ (wkTerm ρ ⊢Δ A) (wkTerm ρ ⊢Δ t)
  wkTerm ρ ⊢Δ (conv t A≡B) = conv (wkTerm ρ ⊢Δ t) (wkEq ρ ⊢Δ A≡B)

  wkEq : ∀ {Γ Δ A B r ρ} → ρ ∷ Δ ⊆ Γ →
       let ρA = U.wk ρ A
           ρB = U.wk ρ B
       in ⊢ Δ → Γ ⊢ A ≡ B ^ r → Δ ⊢ ρA ≡ ρB ^ r
  wkEq ρ ⊢Δ (univ A≡B) = univ (wkEqTerm ρ ⊢Δ A≡B)
  wkEq ρ ⊢Δ (refl A) = refl (wk ρ ⊢Δ A)
  wkEq ρ ⊢Δ (sym A≡B) = sym (wkEq ρ ⊢Δ A≡B)
  wkEq ρ ⊢Δ (trans A≡B B≡C) = trans (wkEq ρ ⊢Δ A≡B) (wkEq ρ ⊢Δ B≡C)

  wkEqTerm : ∀ {Γ Δ A t u r ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρt = U.wk ρ t
               ρu = U.wk ρ u
           in ⊢ Δ → Γ ⊢ t ≡ u ∷ A ^ r → Δ ⊢ ρt ≡ ρu ∷ ρA ^ r
  wkEqTerm ρ ⊢Δ (refl t) = refl (wkTerm ρ ⊢Δ t)
  wkEqTerm ρ ⊢Δ (sym t≡u) = sym (wkEqTerm ρ ⊢Δ t≡u)
  wkEqTerm ρ ⊢Δ (trans t≡u u≡r) = trans (wkEqTerm ρ ⊢Δ t≡u) (wkEqTerm ρ ⊢Δ u≡r)
  wkEqTerm ρ ⊢Δ (conv t≡u A≡B) = conv (wkEqTerm ρ ⊢Δ t≡u) (wkEq ρ ⊢Δ A≡B)
  wkEqTerm ρ ⊢Δ (Π-cong <l <l' F F≡H G≡E) =
    let ρF = wk ρ ⊢Δ F
    in  Π-cong <l <l' ρF (wkEqTerm ρ ⊢Δ F≡H)
                         (wkEqTerm (lift ρ) (⊢Δ ∙ ρF) G≡E)
  wkEqTerm ρ ⊢Δ (∃-cong F F≡H G≡E) =
    let ρF = wk ρ ⊢Δ F
    in  ∃-cong ρF (wkEqTerm ρ ⊢Δ F≡H)
                  (wkEqTerm (lift ρ) (⊢Δ ∙ ρF) G≡E)
  wkEqTerm ρ ⊢Δ (app-cong {G = G} f≡g a≡b) =
    PE.subst (λ x → _ ⊢ _ ≡ _ ∷ x ^ _)
             (PE.sym (wk-β G))
             (app-cong (wkEqTerm ρ ⊢Δ f≡g) (wkEqTerm ρ ⊢Δ a≡b))
  wkEqTerm ρ ⊢Δ (β-red {a = a} {t = t} {G = G} l< l<' F ⊢t ⊢a) =
    let ρF = wk ρ ⊢Δ F
    in  PE.subst (λ x → _ ⊢ _ ≡ _ ∷ x ^ _)
                 (PE.sym (wk-β G))
                 (PE.subst (λ x → _ ⊢ U.wk _ ((lam _ ▹ t ^ _) ∘ a ^ _) ≡ x ∷ _ ^ _)
                           (PE.sym (wk-β t))
                           (β-red l< l<' ρF (wkTerm (lift ρ) (⊢Δ ∙ ρF) ⊢t)
                                     (wkTerm ρ ⊢Δ ⊢a)))
  wkEqTerm ρ ⊢Δ (η-eq lF lG F f g f0≡g0) =
    let ρF = wk ρ ⊢Δ F
    in  η-eq lF lG ρF (wkTerm ρ ⊢Δ f)
                (wkTerm ρ ⊢Δ g)
                (PE.subst (λ t → _ ⊢ t ∘ _ ^ _ ≡ _ ∷ _ ^ _)
                          (PE.sym (wk1-wk≡lift-wk1 _ _))
                          (PE.subst (λ t → _ ⊢ _ ≡ t ∘ _ ^ _ ∷ _ ^ _)
                                    (PE.sym (wk1-wk≡lift-wk1 _ _))
                                    (wkEqTerm (lift ρ) (⊢Δ ∙ ρF) f0≡g0)))
  wkEqTerm ρ ⊢Δ (suc-cong m≡n) = suc-cong (wkEqTerm ρ ⊢Δ m≡n)
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-cong {s = s} {s′ = s′} {F = F} {l = l}
                                     F≡F′ z≡z′ s≡s′ n≡n′) =
    PE.subst (λ x → Δ ⊢ natrec _ _ _ _ _ ≡ _ ∷ x ^ _) (PE.sym (wk-β F))
             (natrec-cong (wkEq (lift [ρ]) (⊢Δ ∙ univ (ℕⱼ ⊢Δ)) F≡F′)
                          (PE.subst (λ x → Δ ⊢ _ ≡ _ ∷ x ^ _) (wk-β F)
                                    (wkEqTerm [ρ] ⊢Δ z≡z′))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ s
                                             ≡ U.wk ρ s′ ∷ x ^ [ ! , ι l ])
                                    (wk-β-natrec _ F ! l)
                                    (wkEqTerm [ρ] ⊢Δ s≡s′))
                          (wkEqTerm [ρ] ⊢Δ n≡n′))
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-zero {z} {s} {F} {l = l} ⊢F ⊢z ⊢s) =
    PE.subst (λ x → Δ ⊢ natrec _ (U.wk (lift _) F) _ _ _ ≡ _ ∷ x ^ _)
             (PE.sym (wk-β F))
             (natrec-zero (wk (lift [ρ]) (⊢Δ ∙ univ (ℕⱼ ⊢Δ)) ⊢F)
                          (PE.subst (λ x → Δ ⊢ U.wk ρ z ∷ x ^ _)
                                    (wk-β F)
                                    (wkTerm [ρ] ⊢Δ ⊢z))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x ^ [ ! , ι l ])
                                    (wk-β-natrec _ F ! l)
                                    (wkTerm [ρ] ⊢Δ ⊢s)))
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-suc {n} {z} {s} {F} {l = l} ⊢n ⊢F ⊢z ⊢s) =
    PE.subst (λ x → Δ ⊢ natrec _ (U.wk (lift _) F) _ _ _
                      ≡ _ ∘ (natrec _ _ _ _ _) ^ _ ∷ x ^ _)
             (PE.sym (wk-β F))
             (natrec-suc (wkTerm [ρ] ⊢Δ ⊢n)
                         (wk (lift [ρ]) (⊢Δ ∙ univ (ℕⱼ ⊢Δ)) ⊢F)
                         (PE.subst (λ x → Δ ⊢ U.wk ρ z ∷ x ^ _)
                                   (wk-β F)
                                   (wkTerm [ρ] ⊢Δ ⊢z))
                         (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x ^ [ ! , ι l ])
                                   (wk-β-natrec _ F ! l)
                                   (wkTerm [ρ] ⊢Δ ⊢s)))
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (Emptyrec-cong {A = A} {A' = A'} {e = e} {e' = e'} A≡A' ⊢e ⊢e') =
    Emptyrec-cong (wkEq [ρ] ⊢Δ A≡A') (wkTerm [ρ] ⊢Δ ⊢e) (wkTerm [ρ] ⊢Δ ⊢e')
  wkEqTerm [ρ] ⊢Δ (proof-irrelevance t u) = proof-irrelevance (wkTerm [ρ] ⊢Δ t) (wkTerm [ρ] ⊢Δ u)
  wkEqTerm ρ ⊢Δ (Id-cong A t u) = Id-cong (wkEqTerm ρ ⊢Δ A) (wkEqTerm ρ ⊢Δ t) (wkEqTerm ρ ⊢Δ u)
  wkEqTerm {ρ = ρ} [ρ] ⊢Δ (Id-Π {rA = rA} {t = t} {u = u} <l <l' Aⱼ Bⱼ tⱼ uⱼ) =
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ in
    let ρB = wkTerm (lift [ρ]) (⊢Δ ∙ univ ρA) Bⱼ in
    let ρt = wkTerm [ρ] ⊢Δ tⱼ in
    let ρu = wkTerm [ρ] ⊢Δ uⱼ in
    PE.subst
      (λ x → _ ⊢ Id _ (U.wk ρ t) _ ≡ Π _ ^ _ ° _ ▹ Id _ (x ∘ _ ^ _) _ ° _ ° _ ∷ _ ^ [ ! , _ ])
      (wk1-wk≡lift-wk1 ρ t)
      (PE.subst
        (λ x → _ ⊢ Id _ _ (U.wk ρ u) ≡ Π _ ^ _ ° _ ▹ Id _ _ (x ∘ _ ^ _) ° _ ° _ ∷ _ ^ [ ! , _ ])
        (wk1-wk≡lift-wk1 ρ u)
        (Id-Π <l <l' ρA ρB ρt ρu))
  wkEqTerm ρ ⊢Δ (Id-ℕ-00 ⊢Γ) = Id-ℕ-00 ⊢Δ
  wkEqTerm ρ ⊢Δ (Id-ℕ-SS m n) = Id-ℕ-SS (wkTerm ρ ⊢Δ m) (wkTerm ρ ⊢Δ n)
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (Id-U-ΠΠ {A = A} {A' = A'} {rA = rA} {B = B} {B' = B'} Aⱼ Bⱼ A'ⱼ B'ⱼ) =
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ in
    let ρA' = wkTerm [ρ] ⊢Δ A'ⱼ in
    let ρB = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA)) Bⱼ in
    let ρB' = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA')) B'ⱼ in
    let l = ⁰ in
    let l' = ¹ in
    let pred = λ A1 A1' A2' B1 B1' → Δ ⊢ U.wk ρ (Id (U l) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° l)) ≡ ∃ U.wk ρ (Id (Univ rA l) A A') ▹ (Π A1' ^ rA ° ⁰ ▹ Id (U l) (B1 [ cast l A2' A1 (Idsym (Univ rA l) A1 A2' (var 1)) (var 0) ]↑) B1' ° l' ° l') ∷ SProp l' ^ [ ! , next l' ] in
    let j1 : pred (wk1 (wk1 (U.wk ρ A))) (wk1 (U.wk ρ A')) (wk1 (wk1 (U.wk ρ A'))) (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))
        j1 = Id-U-ΠΠ ρA ρB ρA' ρB' in
    let j2 = PE.subst (λ x → pred (wk1 (wk1 (U.wk ρ A))) x (wk1 (wk1 (U.wk ρ A'))) (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))) (wk1-wk≡lift-wk1 ρ A') j1 in
    let j3 = PE.subst (λ x → pred x (U.wk (lift ρ) (wk1 A')) (wk1 (wk1 (U.wk ρ A'))) (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))) (wk1wk1-wk≡liftlift-wk1 ρ A) j2 in
    let j4 = PE.subst (λ x → pred (U.wk (lift (lift ρ)) (wk1 (wk1 A))) (U.wk (lift ρ) (wk1 A')) x (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))) (wk1wk1-wk≡liftlift-wk1 ρ A') j3 in
    let j5 = PE.subst (λ x → pred (U.wk (lift (lift ρ)) (wk1 (wk1 A))) (U.wk (lift ρ) (wk1 A')) (U.wk (lift (lift ρ)) (wk1 (wk1 A'))) x (wk1d (U.wk (lift ρ) B'))) (wk1d-wk≡lift-wk1d ρ B) j4 in
    let j6 = PE.subst (λ x → pred (U.wk (lift (lift ρ)) (wk1 (wk1 A))) (U.wk (lift ρ) (wk1 A')) (U.wk (lift (lift ρ)) (wk1 (wk1 A'))) (U.wk (lift (lift ρ)) (wk1d B)) x) (wk1d-wk≡lift-wk1d ρ B') j5 in
    let j7 = PE.subst (λ x → Δ ⊢ U.wk ρ (Id (U l) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° l)) ≡ ∃ U.wk ρ (Id (Univ rA l) A A') ▹ (Π U.wk (lift ρ) (wk1 A') ^ rA ° ⁰ ▹ Id (U l) (U.wk (lift (lift ρ)) (wk1d B) [ (cast l (U.wk (lift (lift ρ)) (wk1 (wk1 A'))) (U.wk (lift (lift ρ)) (wk1 (wk1 A))) x (var 0)) ]↑) (U.wk (lift (lift ρ)) (wk1d B')) ° l' ° l') ∷ SProp l' ^ [ ! , next l' ]) (PE.sym (wk-Idsym (lift (lift ρ)) (Univ rA l) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1))) j6 in
    PE.subst (λ x → Δ ⊢ U.wk ρ (Id (U l) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° l)) ≡ ∃ U.wk ρ (Id (Univ rA l) A A') ▹ (Π U.wk (lift ρ) (wk1 A') ^ rA ° ⁰ ▹ Id (U l) x (U.wk (lift (lift ρ)) (wk1d B')) ° l' ° l') ∷ SProp l' ^ [ ! , _ ]) (PE.sym (wk-β↑ {ρ = lift ρ} {a = cast l (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA l) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0)} (wk1d B))) j7
  wkEqTerm ρ ⊢Δ (Id-U-ℕℕ ⊢Γ) = Id-U-ℕℕ ⊢Δ
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (Id-SProp {A = A} {B = B} Aⱼ Bⱼ) =
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ
        ρB = wkTerm [ρ] ⊢Δ Bⱼ
        l = ⁰
        l' = ¹
    in
    PE.subst
      (λ x → _ ⊢ Id (SProp l) (U.wk ρ A) _ ≡ ∃ (Π U.wk ρ A ^ % ° ⁰ ▹ _ ° ⁰ ° l') ▹ (Π _ ^ % ° ⁰ ▹ x ° _ ° l') ∷ _ ^ [ ! , _ ])
      (wk1d-wk≡lift-wk1d ρ (wk1 A))
      (PE.subst
              (λ x → _ ⊢ Id (SProp l) (U.wk ρ A) _ ≡ ∃ (Π U.wk ρ A ^ % ° ⁰ ▹ _ ° ⁰ ° l') ▹ (Π _ ^ % ° ⁰ ▹  U.wk (lift (step id)) x ° _ ° l') ∷ _ ^ [ ! , _ ])
              (wk1-wk≡lift-wk1 ρ A)
              (PE.subst
                 (λ x → _ ⊢ Id (SProp l) (U.wk ρ A) (U.wk ρ B) ≡ ∃ (Π U.wk ρ A ^ % ° ⁰ ▹ x ° ⁰ ° l') ▹ (Π x ^ % ° ⁰ ▹ _ ° ⁰ ° l') ∷ SProp ¹ ^ [ ! , _ ])
                 (wk1-wk≡lift-wk1 ρ B) (Id-SProp {A = U.wk ρ A} {B = U.wk ρ B} ρA ρB)))
  wkEqTerm ρ ⊢Δ (Id-ℕ-0S n) = Id-ℕ-0S (wkTerm ρ ⊢Δ n)
  wkEqTerm ρ ⊢Δ (Id-ℕ-S0 n) = Id-ℕ-S0 (wkTerm ρ ⊢Δ n)
  wkEqTerm ρ ⊢Δ (Id-U-ℕΠ A B) =
    let ρA = wkTerm ρ ⊢Δ A in
    let ρB = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) B in
    Id-U-ℕΠ ρA ρB
  wkEqTerm ρ ⊢Δ (Id-U-Πℕ A B) =
    let ρA = wkTerm ρ ⊢Δ A in
    let ρB = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) B in
    Id-U-Πℕ ρA ρB
  wkEqTerm ρ ⊢Δ (Id-U-ΠΠ!% eq A B A' B') =
    let ρA = wkTerm ρ ⊢Δ A
        ρB = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) B
        ρA' = wkTerm ρ ⊢Δ A'
        ρB' = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA')) B'
    in Id-U-ΠΠ!% eq ρA ρB ρA' ρB'
  wkEqTerm ρ ⊢Δ (cast-cong A B t e e') = cast-cong (wkEqTerm ρ ⊢Δ A) (wkEqTerm ρ ⊢Δ B) (wkEqTerm ρ ⊢Δ t) (wkTerm ρ ⊢Δ e) (wkTerm ρ ⊢Δ e')
  wkEqTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (cast-Π {A = A} {A' = A'} {rA = rA} {B = B} {B' = B'} {e = e} {f = f} Aⱼ Bⱼ A'ⱼ B'ⱼ eⱼ fⱼ) = let l = ⁰ in let lA = ⁰ in let lB = ⁰ in
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ in
    let ρA' = wkTerm [ρ] ⊢Δ A'ⱼ in
    let ρB = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA)) Bⱼ in
    let ρB' = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA')) B'ⱼ in
    let ρe = wkTerm [ρ] ⊢Δ eⱼ in
    let ρf = wkTerm [ρ] ⊢Δ fⱼ in
    let pred = λ A1 A1' e1 f1 → Δ ⊢ U.wk ρ (cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° l) e f) ≡ (lam (U.wk ρ A') ▹ (let a = cast l A1' A1 (Idsym (Univ rA l) A1 A1' (fst e1)) (var 0) in cast l ((U.wk (lift ρ) B) [ a ]↑) (U.wk (lift ρ) B') ((snd e1) ∘ (var 0) ^ ¹) (f1 ∘ a ^ l)) ^ l) ∷ U.wk ρ (Π A' ^ rA ° lA ▹ B' ° lB ° l) ^ [ ! , _ ] in
    let j0 : pred (wk1 (U.wk ρ A)) (wk1 (U.wk ρ A')) (wk1 (U.wk ρ e)) (wk1 (U.wk ρ f))
        j0 = cast-Π ρA ρB ρA' ρB' ρe ρf
    in
    let j1 = PE.subst (λ x → pred x (wk1 (U.wk ρ A')) (wk1 (U.wk ρ e)) (wk1 (U.wk ρ f))) (wk1-wk≡lift-wk1 ρ A) j0 in
    let j2 = PE.subst (λ x → pred (U.wk (lift ρ) (wk1 A)) x (wk1 (U.wk ρ e)) (wk1 (U.wk ρ f))) (wk1-wk≡lift-wk1 ρ A') j1 in
    let j3 = PE.subst (λ x → pred (U.wk (lift ρ) (wk1 A)) (U.wk (lift ρ) (wk1 A')) x (wk1 (U.wk ρ f))) (wk1-wk≡lift-wk1 ρ e) j2 in
    let j4 = PE.subst (λ x → pred (U.wk (lift ρ) (wk1 A)) (U.wk (lift ρ) (wk1 A')) (U.wk (lift ρ) (wk1 e)) x) (wk1-wk≡lift-wk1 ρ f) j3 in
    let j5 = PE.subst (λ x → Δ ⊢ U.wk ρ (cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° l) e f) ≡ (lam (U.wk ρ A') ▹ (let a = cast l (U.wk (lift ρ) (wk1 A')) (U.wk (lift ρ) (wk1 A)) x (var 0) in cast l ((U.wk (lift ρ) B) [ a ]↑) (U.wk (lift ρ) B') ((snd (U.wk (lift ρ) (wk1 e))) ∘ (var 0) ^ ¹) ((U.wk (lift ρ) (wk1 f)) ∘ a ^ l)) ^ l) ∷ U.wk ρ (Π A' ^ rA ° lA ▹ B' ° lB ° l) ^ [ ! , ι l ]) (PE.sym (wk-Idsym (lift ρ) (Univ rA l) (wk1 A) (wk1 A') (fst (wk1 e)))) j4 in
    PE.subst (λ x → Δ ⊢ U.wk ρ (cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° l) e f) ≡ (lam (U.wk ρ A') ▹ (let a = U.wk (lift ρ) (cast l (wk1 A') (wk1 A) (Idsym (Univ rA l) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0)) in cast l x (U.wk (lift ρ) B') ((snd (U.wk (lift ρ) (wk1 e))) ∘ (var 0) ^ ¹) ((U.wk (lift ρ) (wk1 f)) ∘ a ^ l)) ^ l) ∷ U.wk ρ (Π A' ^ rA ° lA ▹ B' ° lB ° l) ^ [ ! , ι l ]) (PE.sym (wk-β↑ {ρ = ρ} {a = (cast l (wk1 A') (wk1 A) (Idsym (Univ rA l) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0))} B)) j5
  wkEqTerm ρ ⊢Δ (cast-ℕ-0 e) = cast-ℕ-0 (wkTerm ρ ⊢Δ e)
  wkEqTerm ρ ⊢Δ (cast-ℕ-S e n) = cast-ℕ-S (wkTerm ρ ⊢Δ e) (wkTerm ρ ⊢Δ n)

mutual
  wkRed : ∀ {Γ Δ A B r ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρB = U.wk ρ B
           in ⊢ Δ → Γ ⊢ A ⇒ B ^ r → Δ ⊢ ρA ⇒ ρB ^ r
  wkRed ρ ⊢Δ (univ A⇒B) = univ (wkRedTerm ρ ⊢Δ A⇒B)

  wkRedTerm : ∀ {Γ Δ A l t u ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρt = U.wk ρ t
               ρu = U.wk ρ u
           in ⊢ Δ → Γ ⊢ t ⇒ u ∷ A ^ l → Δ ⊢ ρt ⇒ ρu ∷ ρA ^ l
  wkRedTerm ρ ⊢Δ (conv t⇒u A≡B) = conv (wkRedTerm ρ ⊢Δ t⇒u) (wkEq ρ ⊢Δ A≡B)
  wkRedTerm ρ ⊢Δ (app-subst {B = B} t⇒u a) =
    PE.subst (λ x → _ ⊢ _ ⇒ _ ∷ x ^ _) (PE.sym (wk-β B))
             (app-subst (wkRedTerm ρ ⊢Δ t⇒u) (wkTerm ρ ⊢Δ a))
  wkRedTerm ρ ⊢Δ (β-red {A} {B} {lF} {lG} {a} {t} l< l<' ⊢A ⊢t ⊢a) =
    let ⊢ρA = wk ρ ⊢Δ ⊢A
    in  PE.subst (λ x → _ ⊢ _ ⇒ _ ∷ x ^ _) (PE.sym (wk-β B))
                 (PE.subst (λ x → _ ⊢ U.wk _ ((lam _ ▹ t ^ _) ∘ a ^ _) ⇒ x ∷ _ ^ _)
                           (PE.sym (wk-β t))
                           (β-red l< l<' ⊢ρA (wkTerm (lift ρ) (⊢Δ ∙ ⊢ρA) ⊢t)
                                      (wkTerm ρ ⊢Δ ⊢a)))
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-subst {s = s} {F = F} {l = l} ⊢F ⊢z ⊢s n⇒n′) =
    PE.subst (λ x → _ ⊢ natrec _ _ _ _ _ ⇒ _ ∷ x ^ _) (PE.sym (wk-β F))
             (natrec-subst (wk (lift [ρ]) (⊢Δ ∙ univ (ℕⱼ ⊢Δ)) ⊢F)
                           (PE.subst (λ x → _ ⊢ _ ∷ x ^ _) (wk-β F)
                                     (wkTerm [ρ] ⊢Δ ⊢z))
                           (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x ^ [ ! , ι l ])
                                     (wk-β-natrec _ F ! l)
                                     (wkTerm [ρ] ⊢Δ ⊢s))
                           (wkRedTerm [ρ] ⊢Δ n⇒n′))
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-zero {s = s} {F = F} {l = l} ⊢F ⊢z ⊢s) =
    PE.subst (λ x → _ ⊢ natrec _ (U.wk (lift ρ) F) _ _ _ ⇒ _ ∷ x ^ _)
             (PE.sym (wk-β F))
             (natrec-zero (wk (lift [ρ]) (⊢Δ ∙ univ (ℕⱼ ⊢Δ)) ⊢F)
                          (PE.subst (λ x → _ ⊢ _ ∷ x ^ _)
                                    (wk-β F)
                                    (wkTerm [ρ] ⊢Δ ⊢z))
                          (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x ^ [ ! , ι l ])
                                    (wk-β-natrec ρ F ! l)
                                    (wkTerm [ρ] ⊢Δ ⊢s)))
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (natrec-suc {s = s} {F = F} {l = l} ⊢n ⊢F ⊢z ⊢s) =
    PE.subst (λ x → _ ⊢ natrec _ _ _ _ _ ⇒ _ ∘ natrec _ _ _ _ _ ^ _ ∷ x  ^ _)
             (PE.sym (wk-β F))
             (natrec-suc (wkTerm [ρ] ⊢Δ ⊢n)
                         (wk (lift [ρ]) (⊢Δ ∙ univ (ℕⱼ ⊢Δ)) ⊢F)
                         (PE.subst (λ x → _ ⊢ _ ∷ x ^ _)
                                   (wk-β F)
                                   (wkTerm [ρ] ⊢Δ ⊢z))
                         (PE.subst (λ x → Δ ⊢ U.wk ρ s ∷ x ^ [ ! , ι l ])
                                   (wk-β-natrec ρ F ! l)
                                   (wkTerm [ρ] ⊢Δ ⊢s)))
  wkRedTerm ρ ⊢Δ (Id-subst A t u) = Id-subst (wkRedTerm ρ ⊢Δ A) (wkTerm ρ ⊢Δ t) (wkTerm ρ ⊢Δ u)
  wkRedTerm ρ ⊢Δ (Id-ℕ-subst m n) = Id-ℕ-subst (wkRedTerm ρ ⊢Δ m) (wkTerm ρ ⊢Δ n)
  wkRedTerm ρ ⊢Δ (Id-ℕ-0-subst n) = Id-ℕ-0-subst (wkRedTerm ρ ⊢Δ n)
  wkRedTerm ρ ⊢Δ (Id-ℕ-S-subst m n) = Id-ℕ-S-subst (wkTerm ρ ⊢Δ m) (wkRedTerm ρ ⊢Δ n)
  wkRedTerm ρ ⊢Δ (Id-U-subst A B) = Id-U-subst (wkRedTerm ρ ⊢Δ A) (wkTerm ρ ⊢Δ B)
  wkRedTerm ρ ⊢Δ (Id-U-ℕ-subst B) = Id-U-ℕ-subst (wkRedTerm ρ ⊢Δ B)
  wkRedTerm ρ ⊢Δ (Id-U-Π-subst A P B) = let ρA = wkTerm ρ ⊢Δ A in Id-U-Π-subst ρA (wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) P) (wkRedTerm ρ ⊢Δ B)
  wkRedTerm {ρ = ρ} [ρ] ⊢Δ (Id-Π {t = t} {u = u} <l <l' Aⱼ Bⱼ tⱼ uⱼ) =
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ in
    let ρB = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA)) Bⱼ in
    let ρt = wkTerm [ρ] ⊢Δ tⱼ in
    let ρu = wkTerm [ρ] ⊢Δ uⱼ in
    PE.subst
      (λ x → _ ⊢ Id _ (U.wk ρ t) _ ⇒ Π _ ^ _ ° _ ▹ Id _ (x ∘ _ ^ _) _ ° _ ° _ ∷ _ ^ _)
      (wk1-wk≡lift-wk1 ρ t)
      (PE.subst
        (λ x → _ ⊢ Id _ _ (U.wk ρ u) ⇒ Π _ ^ _ ° _ ▹ Id _ _ (x ∘ _ ^ _) ° _ ° _ ∷ _ ^ _)
        (wk1-wk≡lift-wk1 ρ u)
        (Id-Π <l <l' ρA ρB ρt ρu))
  wkRedTerm ρ ⊢Δ (Id-ℕ-00 ⊢Γ) = Id-ℕ-00 ⊢Δ
  wkRedTerm ρ ⊢Δ (Id-ℕ-SS m n) = Id-ℕ-SS (wkTerm ρ ⊢Δ m) (wkTerm ρ ⊢Δ n)
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (Id-U-ΠΠ {A = A} {A' = A'} {rA = rA} {B = B} {B' = B'} Aⱼ Bⱼ A'ⱼ B'ⱼ) =
    let l = ⁰ in
    let l' = ¹ in
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ in
    let ρA' = wkTerm [ρ] ⊢Δ A'ⱼ in
    let ρB = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA)) Bⱼ in
    let ρB' = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA')) B'ⱼ in
    let pred = λ A1 A1' A2' B1 B1' → Δ ⊢ U.wk ρ (Id (U l) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° l)) ⇒ ∃ U.wk ρ (Id (Univ rA l) A A') ▹ (Π A1' ^ rA ° ⁰ ▹ Id (U l) (B1 [ cast l A2' A1 (Idsym (Univ rA l) A1 A2' (var 1)) (var 0) ]↑) B1' ° l' ° l') ∷ SProp l' ^ next l' in
    let j1 : pred (wk1 (wk1 (U.wk ρ A))) (wk1 (U.wk ρ A')) (wk1 (wk1 (U.wk ρ A'))) (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))
        j1 = Id-U-ΠΠ ρA ρB ρA' ρB' in
    let j2 = PE.subst (λ x → pred (wk1 (wk1 (U.wk ρ A))) x (wk1 (wk1 (U.wk ρ A'))) (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))) (wk1-wk≡lift-wk1 ρ A') j1 in
    let j3 = PE.subst (λ x → pred x (U.wk (lift ρ) (wk1 A')) (wk1 (wk1 (U.wk ρ A'))) (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))) (wk1wk1-wk≡liftlift-wk1 ρ A) j2 in
    let j4 = PE.subst (λ x → pred (U.wk (lift (lift ρ)) (wk1 (wk1 A))) (U.wk (lift ρ) (wk1 A')) x (wk1d (U.wk (lift ρ) B)) (wk1d (U.wk (lift ρ) B'))) (wk1wk1-wk≡liftlift-wk1 ρ A') j3 in
    let j5 = PE.subst (λ x → pred (U.wk (lift (lift ρ)) (wk1 (wk1 A))) (U.wk (lift ρ) (wk1 A')) (U.wk (lift (lift ρ)) (wk1 (wk1 A'))) x (wk1d (U.wk (lift ρ) B'))) (wk1d-wk≡lift-wk1d ρ B) j4 in
    let j6 = PE.subst (λ x → pred (U.wk (lift (lift ρ)) (wk1 (wk1 A))) (U.wk (lift ρ) (wk1 A')) (U.wk (lift (lift ρ)) (wk1 (wk1 A'))) (U.wk (lift (lift ρ)) (wk1d B)) x) (wk1d-wk≡lift-wk1d ρ B') j5 in
    let j7 = PE.subst (λ x → Δ ⊢ U.wk ρ (Id (U l) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° l)) ⇒ ∃ U.wk ρ (Id (Univ rA l) A A') ▹ (Π U.wk (lift ρ) (wk1 A') ^ rA ° ⁰ ▹ Id (U l) (U.wk (lift (lift ρ)) (wk1d B) [ (cast l (U.wk (lift (lift ρ)) (wk1 (wk1 A'))) (U.wk (lift (lift ρ)) (wk1 (wk1 A))) x (var 0)) ]↑) (U.wk (lift (lift ρ)) (wk1d B')) ° l' ° l') ∷ SProp l' ^ next l') (PE.sym (wk-Idsym (lift (lift ρ)) (Univ rA l) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1))) j6 in
    PE.subst (λ x → Δ ⊢ U.wk ρ (Id (U l) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° l)) ⇒ ∃ U.wk ρ (Id (Univ rA l) A A') ▹ (Π U.wk (lift ρ) (wk1 A') ^ rA ° ⁰ ▹ Id (U l) x (U.wk (lift (lift ρ)) (wk1d B')) ° l' ° l') ∷ SProp l' ^ next l') (PE.sym (wk-β↑ {ρ = lift ρ} {a = cast l (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA l) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0)} (wk1d B))) j7
  wkRedTerm ρ ⊢Δ (Id-U-ℕℕ ⊢Γ) = Id-U-ℕℕ ⊢Δ
  wkRedTerm {ρ = ρ} [ρ] ⊢Δ (Id-SProp {A = A} {B = B} Aⱼ Bⱼ) =
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ
        ρB = wkTerm [ρ] ⊢Δ Bⱼ
        l = ⁰
        l' = ¹
    in
    PE.subst
      (λ x → _ ⊢ Id (SProp l) (U.wk ρ A) _ ⇒ ∃ (Π U.wk ρ A ^ % ° ⁰ ▹ _ ° ⁰ ° _) ▹ (Π _ ^ % ° ⁰ ▹ x ° _ ° _) ∷ _ ^ _)
      (wk1d-wk≡lift-wk1d ρ (wk1 A))
      (PE.subst
              (λ x → _ ⊢ Id (SProp l) (U.wk ρ A) _ ⇒ ∃ (Π U.wk ρ A ^ % ° ⁰ ▹ _ ° ⁰ ° _) ▹ (Π _ ^ % ° ⁰ ▹  U.wk (lift (step id)) x ° _ ° _) ∷ _ ^ _ )
              (wk1-wk≡lift-wk1 ρ A)
              (PE.subst
                 (λ x → _ ⊢ Id (SProp l) (U.wk ρ A) (U.wk ρ B) ⇒ ∃ (Π U.wk ρ A ^ % ° ⁰ ▹ x ° ⁰ ° _) ▹ (Π x ^ % ° ⁰ ▹ _ ° ⁰ ° _) ∷ SProp ¹ ^ _ )
                 (wk1-wk≡lift-wk1 ρ B) (Id-SProp {A = U.wk ρ A} {B = U.wk ρ B} ρA ρB)))
  wkRedTerm ρ ⊢Δ (Id-ℕ-0S n) = Id-ℕ-0S (wkTerm ρ ⊢Δ n)
  wkRedTerm ρ ⊢Δ (Id-ℕ-S0 n) = Id-ℕ-S0 (wkTerm ρ ⊢Δ n)
  wkRedTerm ρ ⊢Δ (Id-U-ℕΠ A B) =
    let ρA = wkTerm ρ ⊢Δ A in
    let ρB = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) B in
    Id-U-ℕΠ ρA ρB
  wkRedTerm ρ ⊢Δ (Id-U-Πℕ A B) =
    let ρA = wkTerm ρ ⊢Δ A in
    let ρB = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) B in
    Id-U-Πℕ ρA ρB
  wkRedTerm ρ ⊢Δ (Id-U-ΠΠ!% eq A B A' B') =
    let ρA = wkTerm ρ ⊢Δ A
        ρB = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) B
        ρA' = wkTerm ρ ⊢Δ A'
        ρB' = wkTerm (lift ρ) (⊢Δ ∙ (univ ρA')) B'
    in Id-U-ΠΠ!% eq ρA ρB ρA' ρB'
  wkRedTerm ρ ⊢Δ  (cast-subst A B e t) = cast-subst (wkRedTerm ρ ⊢Δ A) (wkTerm ρ ⊢Δ  B) (wkTerm ρ ⊢Δ e) (wkTerm ρ ⊢Δ t)
  wkRedTerm ρ ⊢Δ  (cast-ℕ-subst B e t) = cast-ℕ-subst (wkRedTerm ρ ⊢Δ B) (wkTerm ρ ⊢Δ e) (wkTerm ρ ⊢Δ t)
  wkRedTerm ρ ⊢Δ  (cast-Π-subst A P B e t) = let ρA = wkTerm ρ ⊢Δ A in cast-Π-subst ρA (wkTerm (lift ρ) (⊢Δ ∙ (univ ρA)) P) (wkRedTerm ρ ⊢Δ B) (wkTerm ρ ⊢Δ e) (wkTerm ρ ⊢Δ t)
  wkRedTerm {Δ = Δ} {ρ = ρ} [ρ] ⊢Δ (cast-Π {A = A} {A' = A'} {rA = rA} {B = B} {B' = B'} {e = e} {f = f} Aⱼ Bⱼ A'ⱼ B'ⱼ eⱼ fⱼ) = let l = ⁰ in let lA = ⁰ in let lB = ⁰ in
    let ρA = wkTerm [ρ] ⊢Δ Aⱼ in
    let ρA' = wkTerm [ρ] ⊢Δ A'ⱼ in
    let ρB = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA)) Bⱼ in
    let ρB' = wkTerm (lift [ρ]) (⊢Δ ∙ (univ ρA')) B'ⱼ in
    let ρe = wkTerm [ρ] ⊢Δ eⱼ in
    let ρf = wkTerm [ρ] ⊢Δ fⱼ in
    let pred = λ A1 A1' e1 f1 → Δ ⊢ U.wk ρ (cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° l) e f) ⇒ (lam (U.wk ρ A') ▹ (let a = cast l A1' A1 (Idsym (Univ rA l) A1 A1' (fst e1)) (var 0) in cast l ((U.wk (lift ρ) B) [ a ]↑) (U.wk (lift ρ) B') ((snd e1) ∘ (var 0) ^ ¹) (f1 ∘ a ^ l))  ^ l) ∷ U.wk ρ (Π A' ^ rA ° lA ▹ B' ° lB ° l) ^ _ in
    let j0 : pred (wk1 (U.wk ρ A)) (wk1 (U.wk ρ A')) (wk1 (U.wk ρ e)) (wk1 (U.wk ρ f))
        j0 = cast-Π ρA ρB ρA' ρB' ρe ρf
    in
    let j1 = PE.subst (λ x → pred x (wk1 (U.wk ρ A')) (wk1 (U.wk ρ e)) (wk1 (U.wk ρ f))) (wk1-wk≡lift-wk1 ρ A) j0 in
    let j2 = PE.subst (λ x → pred (U.wk (lift ρ) (wk1 A)) x (wk1 (U.wk ρ e)) (wk1 (U.wk ρ f))) (wk1-wk≡lift-wk1 ρ A') j1 in
    let j3 = PE.subst (λ x → pred (U.wk (lift ρ) (wk1 A)) (U.wk (lift ρ) (wk1 A')) x (wk1 (U.wk ρ f))) (wk1-wk≡lift-wk1 ρ e) j2 in
    let j4 = PE.subst (λ x → pred (U.wk (lift ρ) (wk1 A)) (U.wk (lift ρ) (wk1 A')) (U.wk (lift ρ) (wk1 e)) x) (wk1-wk≡lift-wk1 ρ f) j3 in
    let j5 = PE.subst (λ x → Δ ⊢ U.wk ρ (cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° l) e f) ⇒ (lam (U.wk ρ A') ▹ (let a = cast l (U.wk (lift ρ) (wk1 A')) (U.wk (lift ρ) (wk1 A)) x (var 0) in cast l ((U.wk (lift ρ) B) [ a ]↑) (U.wk (lift ρ) B') ((snd (U.wk (lift ρ) (wk1 e))) ∘ (var 0) ^ ¹) ((U.wk (lift ρ) (wk1 f)) ∘ a ^ l)) ^ l) ∷ U.wk ρ (Π A' ^ rA ° lA ▹ B' ° lB ° l) ^ ι l) (PE.sym (wk-Idsym (lift ρ) (Univ rA l) (wk1 A) (wk1 A') (fst (wk1 e)))) j4 in
   PE.subst (λ x → Δ ⊢ U.wk ρ (cast l (Π A ^ rA ° lA ▹ B ° lB ° l) (Π A' ^ rA ° lA ▹ B' ° lB ° l) e f) ⇒ (lam (U.wk ρ A') ▹ (let a = U.wk (lift ρ) (cast l (wk1 A') (wk1 A) (Idsym (Univ rA l) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0)) in cast l x (U.wk (lift ρ) B') ((snd (U.wk (lift ρ) (wk1 e))) ∘ (var 0) ^ ¹) ((U.wk (lift ρ) (wk1 f)) ∘ a ^ l)) ^ l) ∷ U.wk ρ (Π A' ^ rA ° lA ▹ B' ° lB ° l) ^ ι l) (PE.sym (wk-β↑ {ρ = ρ} {a = (cast l (wk1 A') (wk1 A) (Idsym (Univ rA l) (wk1 A) (wk1 A') (fst (wk1 e))) (var 0))} B)) j5
  wkRedTerm ρ ⊢Δ (cast-ℕ-0 e) = cast-ℕ-0 (wkTerm ρ ⊢Δ e)
  wkRedTerm ρ ⊢Δ (cast-ℕ-S e n) = cast-ℕ-S (wkTerm ρ ⊢Δ e) (wkTerm ρ ⊢Δ n)
  wkRedTerm ρ ⊢Δ (cast-ℕ-cong e n) = cast-ℕ-cong (wkTerm ρ ⊢Δ e) (wkRedTerm ρ ⊢Δ n)

wkRed* : ∀ {Γ Δ A B r ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρB = U.wk ρ B
           in ⊢ Δ → Γ ⊢ A ⇒* B ^ r → Δ ⊢ ρA ⇒* ρB ^ r
wkRed* ρ ⊢Δ (id A) = id (wk ρ ⊢Δ A)
wkRed* ρ ⊢Δ (A⇒A′ ⇨ A′⇒*B) = wkRed ρ ⊢Δ A⇒A′ ⇨ wkRed* ρ ⊢Δ A′⇒*B

wkRed*Term : ∀ {Γ Δ A l t u ρ} → ρ ∷ Δ ⊆ Γ →
           let ρA = U.wk ρ A
               ρt = U.wk ρ t
               ρu = U.wk ρ u
           in ⊢ Δ → Γ ⊢ t ⇒* u ∷ A ^ l → Δ ⊢ ρt ⇒* ρu ∷ ρA ^ l
wkRed*Term ρ ⊢Δ (id t) = id (wkTerm ρ ⊢Δ t)
wkRed*Term ρ ⊢Δ (t⇒t′ ⇨ t′⇒*u) = wkRedTerm ρ ⊢Δ t⇒t′ ⇨ wkRed*Term ρ ⊢Δ t′⇒*u

wkRed:*: : ∀ {Γ Δ A B r ρ} → ρ ∷ Δ ⊆ Γ →
         let ρA = U.wk ρ A
             ρB = U.wk ρ B
         in ⊢ Δ → Γ ⊢ A :⇒*: B ^ r → Δ ⊢ ρA :⇒*: ρB ^ r
wkRed:*: ρ ⊢Δ [[ ⊢A , ⊢B , D ]] = [[ wk ρ ⊢Δ ⊢A , wk ρ ⊢Δ ⊢B , wkRed* ρ ⊢Δ D ]]

wkRed:*:Term : ∀ {Γ Δ A l t u ρ} → ρ ∷ Δ ⊆ Γ →
             let ρA = U.wk ρ A
                 ρt = U.wk ρ t
                 ρu = U.wk ρ u
             in ⊢ Δ → Γ ⊢ t :⇒*: u ∷ A ^ l → Δ ⊢ ρt :⇒*: ρu ∷ ρA ^ l
wkRed:*:Term ρ ⊢Δ [[ ⊢t , ⊢u , d ]] =
  [[ wkTerm ρ ⊢Δ ⊢t , wkTerm ρ ⊢Δ ⊢u , wkRed*Term ρ ⊢Δ d ]]

ext: agda

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

module Tools.Function where

-- Identity function
idᶠ : {A : Set} → A → A
idᶠ x = x

-- Function composition (simply typed variant)
_∘ᶠ_ : {A B C : Set} → (B → C) → (A → B) → A → C
_∘ᶠ_ f g a = f (g a)


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

module Function.Reasoning where

open import Level

infixr 2 _⟨⟩⇒_ ⟨∙⟩⇒-syntax

⟨∙⟩⇒-syntax : ∀ (A : Type a) → (B → C) → (A → B) → A → C
⟨∙⟩⇒-syntax _ f g x = f (g x)

syntax ⟨∙⟩⇒-syntax A f g = A ⟨ g ⟩⇒ f

_⟨⟩⇒_ : ∀ (A : Type a) → (A → B) → A → B
_ ⟨⟩⇒ f = f

infix 2.5 _⇒∎
_⇒∎ : (A : Type a) → A → A
_⇒∎ _ x = x

infixr 1.5 [_]⇒_
[_]⇒_ : A → (A → B) → B
[ x ]⇒ f = f x

-- infix 2.5 _⇒[_]
-- _⇒[_] : (A : Type a) → A → A
-- _ ⇒[ x ] = x

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2016-04-13 display forms do not work for projection patterns

-- {-# OPTIONS -v tc.display:100 #-}

postulate B : Set

module M (A : Set) where
  record R : Set where
    field f : A

open M B

test : R
test = {!!}  -- C-c C-c RET  split on result here

-- Is:
-- M.R.f test = ?
--
-- Expected:
-- R.f test = ?

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Arithmetic where

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

  _+_ : ℕ → ℕ → ℕ
  zero     + b = b
  (succ a) + b = succ (a + b)

  -- ℕ + ℕ =  succ (succ ℕ))

  _*_ : ℕ → ℕ → ℕ
  zero     * b = zero
  (succ a) * b = a + b * a


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

open import HoTT
open import cohomology.CofiberSequence
open import cohomology.Exactness
open import cohomology.FunctionOver
open import cohomology.Theory
open import cohomology.ProductRepr
open import cohomology.WedgeCofiber

{- Finite additivity is provable (and in a stronger form) without using
 - the additivity axiom. We have

         Cⁿ(X ∨ Y) == Cⁿ(X) × Cⁿ(Y)

 - and over this path
 -   ∙ Cⁿ(winl) corresponds to fst : Cⁿ(X) × Cⁿ(Y) → Cⁿ(X),
 -   ∙ Cⁿ(winr) corresponds to snd : Cⁿ(X) × Cⁿ(Y) → Cⁿ(Y),
 -   ∙ Cⁿ(Wedge-rec winl* winr* wglue*) : Cⁿ(Z) → Cⁿ(X ∨ Y)
       corresponds to Cⁿ(winl*) × Cⁿ(winr*).
 -   ∙ Cⁿ(f) : Cⁿ(X ∨ Y) → Cⁿ(Z)
       corresponds to Cⁿ(projl ∘ f) + Cⁿ(projr ∘ f) : Cⁿ(X) × Cⁿ(Y) → Cⁿ(Z)
 -}

module cohomology.Wedge {i} (CT : CohomologyTheory i) where

module CWedge (n : ℤ) (X Y : Ptd i) where

  open WedgeCofiber X Y

  open CohomologyTheory CT
  open import cohomology.Functor CT

  private
    βl : CF-hom n ⊙winl ∘ᴳ CF-hom n (⊙projl X Y) == idhom _
    βl = ! (CF-comp n (⊙projl X Y) ⊙winl) ∙ CF-ident n

    βr : CF-hom n ⊙winr ∘ᴳ CF-hom n (⊙projr X Y) == idhom _
    βr = ! (CF-comp n (⊙projr X Y) ⊙winr)
         ∙ ap (CF-hom n) ⊙projr-winr
         ∙ CF-ident n
      where
      ⊙projr-winr : ⊙projr X Y ⊙∘ ⊙winr == ⊙idf _
      ⊙projr-winr = ⊙λ= (λ _ → idp) $
        ∙-unit-r _ ∙ ap-! (projr X Y) wglue ∙ ap ! (Projr.glue-β X Y)

  open ProductRepr
    (CF-hom n (⊙projl X Y)) (CF-hom n (⊙projr X Y))
    (CF-hom n ⊙winl) (CF-hom n ⊙winr)
    (app= (ap GroupHom.f βl)) (app= (ap GroupHom.f βr))
    (transport
      (λ {(_ , g) → is-exact (CF-hom n g) (CF-hom n ⊙winr)})
      (pair= CofWinr.⊙path CofWinr.cfcod-over)
      (C-exact n ⊙winr))
    (transport
      (λ {(_ , g) → is-exact (CF-hom n g) (CF-hom n ⊙winl)})
      (pair= CofWinl.⊙path CofWinl.cfcod-over)
      (C-exact n ⊙winl))
    public

  ⊙wedge-rec-over : {Z : Ptd i} (winl* : fst (X ⊙→ Z)) (winr* : fst (Y ⊙→ Z))
    → CF-hom n (⊙wedge-rec winl* winr*)
      == ×ᴳ-hom-in (CF-hom n winl*) (CF-hom n (winr*))
      [ (λ K → C n Z →ᴳ K) ↓ path ]
  ⊙wedge-rec-over winl* winr* = codomain-over-iso $
    codomain-over-equiv (CF n R.⊙f) _
    ▹ ap2 (λ f g z → (f z , g z))
          (ap GroupHom.f $ ! (CF-comp n R.⊙f ⊙winl) ∙ ap (CF-hom n) R.⊙winl-β)
          (ap GroupHom.f $ ! (CF-comp n R.⊙f ⊙winr) ∙ ap (CF-hom n) R.⊙winr-β)
    where
    module R = ⊙WedgeRec winl* winr*

  wedge-hom-η : {Z : Ptd i} (φ : C n (⊙Wedge X Y) →ᴳ C n Z)
    → φ == ×ᴳ-sum-hom (C-abelian n _) (φ ∘ᴳ CF-hom n (⊙projl X Y))
                                      (φ ∘ᴳ CF-hom n (⊙projr X Y))
      [ (λ G → G →ᴳ C n Z) ↓ path ]
  wedge-hom-η φ =
    lemma (C-abelian n _) (C-abelian n _) inl-over inr-over
    where
    lemma : {G H K L : Group i}
      (aG : is-abelian G) (aL : is-abelian L) {p : G == H ×ᴳ K}
      {φ : H →ᴳ G} {ψ : K →ᴳ G} {χ : G →ᴳ L}
      → φ == ×ᴳ-inl [ (λ J → H →ᴳ J) ↓ p ]
      → ψ == ×ᴳ-inr {G = H} [ (λ J → K →ᴳ J) ↓ p ]
      → χ == ×ᴳ-sum-hom aL (χ ∘ᴳ φ) (χ ∘ᴳ ψ) [ (λ J → J →ᴳ L) ↓ p ]
    lemma {H = H} {K = K} aG aL {p = idp} {χ = χ} idp idp =
      ap (λ α → χ ∘ᴳ α) (×ᴳ-sum-hom-η H K aG)
      ∙ ! (∘-×ᴳ-sum-hom aG aL χ (×ᴳ-inl {G = H}) (×ᴳ-inr {G = H}))

  wedge-in-over : {Z : Ptd i} (f : fst (Z ⊙→ ⊙Wedge X Y))
    → CF-hom n f
      == ×ᴳ-sum-hom (C-abelian n _) (CF-hom n (⊙projl X Y ⊙∘ f))
                                    (CF-hom n (⊙projr X Y ⊙∘ f))
      [ (λ G → G →ᴳ C n Z) ↓ path ]
  wedge-in-over f =
    wedge-hom-η (CF-hom n f)
    ▹ ap2 (×ᴳ-sum-hom (C-abelian n _))
        (! (CF-comp n (⊙projl X Y) f))
        (! (CF-comp n (⊙projr X Y) f))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Model where

open import Data.Product
open import Data.Char
open import Data.String
open import Data.Container.Indexed
open import IO.Primitive

open import Signature

postulate
  Model        : Set
  initialModel : Model

  moveModel          : Dir → Model → Model
  setMode            : Mode → Model → Model
  getPrompt          : Model → Prompt
  addCharToBuffer    : Char → Model → Model
  getBuffer          : Model → String
  setCurrentFeed     : Model → Feed → Model
  getCurrentFeedsUrl : Model → String
  searchModel        : String → Model → Model
  searchNextModel    : String → Model → Model
  addFeedToModel     : String → Model → Model

cmdToResp : ∀ {m} (c : Command Hårss m) → Model → IO (Response Hårss c)
cmdToResp (moveP d)    m = return _
cmdToResp (promptP p)  m = return _
cmdToResp (putCharP c) m = return _
cmdToResp doneP        m = return (getBuffer m , getPrompt m)
cmdToResp fetchP       m = fetchUrl (getCurrentFeedsUrl m)
  where
  postulate
    fetchUrl : String → IO Feed
cmdToResp searchNextP  m = return (getBuffer m)

max_stars_repo_name: stevana/haarss

max_issues_repo_name: stevana/haarss

max_forks_repo_name: stevana/haarss


text:
{-# OPTIONS --without-K  #-}
module sets.fin where

open import sets.fin.core public
-- open import sets.fin.properties public
-- open import sets.fin.ordering public
-- open import sets.fin.universe public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
import      Lvl
open import Structure.Category
open import Structure.Setoid
open import Type

-- TODO: Deprecate this file and use Relator.Equals.Category instead
module Structure.Category.Morphism.IdTransport where

import      Functional.Dependent as Fn
import      Function.Equals
open        Function.Equals.Dependent
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Relator.Equals using ([≡]-intro) renaming (_≡_ to _≡ₑ_)
open import Relator.Equals.Proofs
import      Structure.Categorical.Names as Names
open import Structure.Category.Functor
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Syntax.Transitivity

module _
  {ℓₒ ℓₘ ℓₑ : Lvl.Level}
  (cat : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ})
  where

  open CategoryObject(cat)
  open Category(category) using (_∘_ ; id ; identityₗ ; identityᵣ)
  open Category.ArrowNotation(category)
  open Morphism.OperModule ⦃ morphism-equiv ⦄ (\{x} → _∘_ {x})
  open Morphism.IdModule   ⦃ morphism-equiv ⦄ (\{x} → _∘_ {x})(id)

  private variable a b c : Object

  -- Essentially the identity morphism masquerading as a morphism between two arbitrary but identical objects.
  transport : (a ≡ₑ b) → (a ⟶ b)
  transport = sub₂(_≡ₑ_)(_⟶_) ⦃ [≡]-sub-of-reflexive ⦃ intro id ⦄ ⦄

  transport-function : Function ⦃ [≡]-equiv ⦄ ⦃ morphism-equiv ⦄ (transport {a = a}{b = b})
  Function.congruence transport-function xy = sub₂(_≡ₑ_)(_≡_) ⦃ [≡]-sub-of-reflexive ⦃ Equiv.reflexivity(morphism-equiv) ⦄ ⦄ ([≡]-with(transport) xy)

  transport-of-reflexivity : (transport(reflexivity(_≡ₑ_)) ≡ id{a})
  transport-of-reflexivity = reflexivity(_≡_) ⦃ Equiv.reflexivity morphism-equiv ⦄

  -- transport-of-symmetry : ∀{ab : (a ≡ₑ b)}{ba : (b ≡ₑ a)} → (transitivity(_≡ₑ_) ab ba ≡ reflexivity(_≡ₑ_)) → (transport(symmetry(_≡ₑ_) ab) ≡ transport ba)

  transport-of-transitivity : ∀{ab : (a ≡ₑ b)}{bc : (b ≡ₑ c)} → (transport(transitivity(_≡ₑ_) ab bc) ≡ transport(bc) ∘ transport(ab))
  transport-of-transitivity {ab = [≡]-intro} {bc = [≡]-intro} = symmetry(_≡_) ⦃ Equiv.symmetry morphism-equiv ⦄ (Morphism.identityₗ(_∘_)(id))

  [∘]-on-transport-inverseₗ : ∀{ab : (a ≡ₑ b)} → ((transport (symmetry(_≡ₑ_) ab)) ∘ (transport ab) ≡ id)
  [∘]-on-transport-inverseₗ {ab = [≡]-intro} = Morphism.identityₗ(_∘_)(id)

  instance
    transport-inverseₗ : ∀{ab : (a ≡ₑ b)} → Inverseₗ(transport ab) (transport(symmetry(_≡ₑ_) ab))
    transport-inverseₗ {ab = ab} = Morphism.intro ([∘]-on-transport-inverseₗ {ab = ab})

  [∘]-on-transport-inverseᵣ : ∀{ab : (a ≡ₑ b)} → ((transport ab) ∘ (transport (symmetry(_≡ₑ_) ab)) ≡ id)
  [∘]-on-transport-inverseᵣ {ab = [≡]-intro} = Morphism.identityᵣ(_∘_)(id)

  instance
    transport-inverseᵣ : ∀{ab : (a ≡ₑ b)} → Inverseᵣ(transport ab) (transport(symmetry(_≡ₑ_) ab))
    transport-inverseᵣ {ab = ab} = Morphism.intro ([∘]-on-transport-inverseᵣ {ab = ab})

  instance
    transport-isomorphism : ∀{ab : (a ≡ₑ b)} → Isomorphism(transport ab)
    transport-isomorphism {ab = ab} = [∃]-intro (transport(symmetry(_≡_) ab)) ⦃ [∧]-intro (transport-inverseₗ {ab = ab}) (transport-inverseᵣ {ab = ab}) ⦄

  transport-congruence-symmetry-involution : ∀{ab : (a ≡ₑ b)} → ((transport Fn.∘ symmetry(_≡ₑ_) Fn.∘ symmetry(_≡ₑ_)) ab ≡ transport ab)
  transport-congruence-symmetry-involution {ab = [≡]-intro} = reflexivity(_≡_) ⦃ Equiv.reflexivity morphism-equiv ⦄

module _
  {ℓₒₗ ℓₘₗ ℓₑₗ ℓₒᵣ ℓₘᵣ ℓₑᵣ : Lvl.Level}
  {catₗ : CategoryObject{ℓₒₗ}{ℓₘₗ}{ℓₑₗ}}
  {catᵣ : CategoryObject{ℓₒᵣ}{ℓₘᵣ}{ℓₑᵣ}}
  where

  open CategoryObject
  open Category using (_∘_ ; id ; identityₗ ; identityᵣ)
  open Category.ArrowNotation

  private open module Equivᵣ {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv(catᵣ){x}{y} ⦄) using ()

  transport-of-congruenced-functor : (([∃]-intro F ⦃ intro map ⦄) : catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ) → ∀{a b : Object(catₗ)}{ab : (a ≡ₑ b)} → (transport(catᵣ)(congruence₁ F ab) ≡ map(transport(catₗ)(ab)))
  transport-of-congruenced-functor ([∃]-intro F functor@⦃ intro map ⦄) {ab = [≡]-intro} =
    transport catᵣ (congruence₁ F [≡]-intro) 🝖[ _≡_ ]-[]
    transport catᵣ [≡]-intro                 🝖[ _≡_ ]-[]
    id(category(catᵣ))                       🝖[ _≡_ ]-[ Functor.id-preserving functor ]-sym
    map(id(category(catₗ)))                  🝖[ _≡_ ]-[]
    map(transport catₗ [≡]-intro)            🝖-end

  -- transport-of-congruenced-bifunctor : ∀{ab : (a ≡ₑ b)}{[∃]-intro F : Bifunctor} → (F(transport(ab)(cd)) ≡ transport(congruence₂ F ab cd))

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:
{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

module _ where

data Unit : Set where
  unit : Unit

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

subst : {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y
subst P refl p = p

module _ (p : false ≡ true) where

  block : {A : Set} → Unit → A → A
  block unit x = x

  r : ∀ u → block u false ≡ true
  r unit = p

  {-# REWRITE r #-}

  r′ : ∀ u → block u false ≡ true
  r′ u = refl

  lazy : false ≡ true
  lazy = r′ unit

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

module _ (p : false ≡ true) where

  bool : (Bool → Bool) → Bool
  bool = subst T (lazy p)

  fun : Bool → (Bool → Bool)
  fun = subst T (sym (lazy p))

  omega : Bool → Bool
  omega = λ x → fun x x

  loop : Bool
  loop = omega (bool omega)

-- omega = λ p x → x x
-- loop = λ p → <BLACKHOLE>


text:
module Lemmachine.Default.Proofs where
open import Lemmachine
import Lemmachine.Default
import Lemmachine.Lemmas
open import Lemmachine.Default.Lemmas
open Lemmachine.Lemmas Lemmachine.Default.resource
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Maybe
open import Data.Product hiding (map)
open import Data.Function using (const)
open import Data.List.Any

methodNotAllowed : ∀ r → method r ∉ allowedMethods r
                       → resolveStatus r ≡ MethodNotAllowed
methodNotAllowed r p with methodAlwaysKnown r | methodIsntAllowed r p
... | p₂ | p₃ rewrite p₂ | p₃ = refl

optionsOK : ∀ r → method r ∈ allowedMethods r
                → method r ≡ OPTIONS
                → resolveStatus r ≡ OK
optionsOK r p p₂ with methodAlwaysKnown r | methodIsAllowed r p
... | p₃ | p₄  rewrite p₃ | p₄ | p₂ = refl

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Common.Prelude

⟨_⟩_ : Bool → Bool → Bool
⟨ _ ⟩_ = λ b → b


text:
-- Andreas, 2017-12-16, issue #2870
-- Nicer error for non-printable character in lexer.

postulate
  beforeHyphenafterHyphen : Set

-- Expected something like:
-- Lexical error (unprintable character)


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

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

module Rings.Primes.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Divisible.Definition R
open import Rings.IntegralDomains.Lemmas intDom
open import Rings.Ideals.Definition R
open import Rings.Primes.Definition intDom
open import Rings.Ideals.Prime.Definition {R = R}
open import Rings.Irreducibles.Definition intDom
open Ring R
open Setoid S
open Equivalence eq

primeImpliesPrimeIdeal : {a : A} → Prime a → PrimeIdeal (generatedIdeal a)
primeImpliesPrimeIdeal {a} record { isPrime = isPrime ; nonzero = nonzero ; nonunit = nonunit } = record { isPrime = λ {r} {s} → isPrime r s ; notContained = 1R ; notContainedIsNotContained = bad }
  where
    bad : a ∣ 1R → False
    bad (c , ac=1) = nonunit (c , ac=1)

primeIdealImpliesPrime : {a : A} → ((a ∼ 0R) → False) → PrimeIdeal (generatedIdeal a) → Prime a
Prime.isPrime (primeIdealImpliesPrime {a} a!=0 record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) r s a|rs aNot|r = isPrime a|rs aNot|r
Prime.nonzero (primeIdealImpliesPrime {a} a!=0 record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) = a!=0
Prime.nonunit (primeIdealImpliesPrime {a} a!=0 record { isPrime = isPrime ; notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained }) (c , ac=1) = notContainedIsNotContained ((c * notContained) , transitive *Associative (transitive (*WellDefined ac=1 reflexive) identIsIdent))

primeIsIrreducible : {a : A} → Prime a → Irreducible a
Irreducible.nonzero (primeIsIrreducible {a} prime) = Prime.nonzero prime
Irreducible.nonunit (primeIsIrreducible {a} prime) = Prime.nonunit prime
Irreducible.irreducible (primeIsIrreducible {a} prime) x y xy=a xNonunit = underlying pr , yUnit
  where
    a|xy : a ∣ (x * y)
    a|xy = 1R , transitive *Commutative (transitive identIsIdent (symmetric xy=a))
    a|yFalse : (a ∣ y) → False
    a|yFalse (c , ac=y) = xNonunit (c , transitive *Commutative t)
      where
        s : (a * (c * x)) ∼ a
        s = transitive *Associative (transitive (*WellDefined ac=y reflexive) (transitive *Commutative xy=a))
        t : (c * x) ∼ 1R
        t = cancelIntDom {a} {c * x} {1R} (transitive s (symmetric (transitive *Commutative identIsIdent))) (Prime.nonzero prime)
    pr : Sg A (λ c → (a * c) ∼ x)
    pr = Prime.isPrime prime y x (divisibleWellDefined reflexive *Commutative a|xy) a|yFalse
    yUnit : (y * underlying pr) ∼ 1R
    yUnit with pr
    ... | c , ac=x = transitive *Commutative (cancelIntDom {a} {c * y} {1R} (transitive *Associative (transitive (*WellDefined ac=x reflexive) (transitive xy=a (symmetric (transitive *Commutative identIsIdent))))) (Prime.nonzero prime))


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

open import Level
open import Categories.Category
open import Categories.Monad

module Categories.Monad.Morphism {o ℓ e} {C D : Category o ℓ e} where

open import Categories.NaturalTransformation
open import Categories.Functor

open NaturalTransformation

-- monad morphism in the sense of the nLab
-- https://ncatlab.org/nlab/show/monad#the_bicategory_of_monads
-- between generic monads t : a -> a & s : b -> b
record Monad⇒ (M : Monad C) (N : Monad D) : Set (o ⊔ ℓ ⊔ e) where

  private
    module M = Monad M
    module N = Monad N

  open module D = Category D using (_∘_; _≈_)

  field
    X : Functor C D
    α : NaturalTransformation (N.F ∘F X) (X ∘F M.F)

  module X = Functor X
  module α = NaturalTransformation α

  field
    unit-comp : ∀ {U} → α.η U ∘ (N.η.η (X.₀ U)) ≈ X.₁ (M.η.η U)
    mult-comp : ∀ {U} → α.η U ∘ (N.μ.η (X.₀ U)) ≈ X.₁ (M.μ.η U) ∘ α.η (M.F.₀ U) ∘ N.F.₁ (α.η U)

-- monad morphism in a different sense:
-- monads are on the same category, X is the identity
record Monad⇒-id (M N : Monad C) : Set (o ⊔ ℓ ⊔ e) where

  private
    module M = Monad M
    module N = Monad N

  field
    α : NaturalTransformation N.F M.F

  module α = NaturalTransformation α

  open module C = Category C using (_∘_; _≈_)

  field
    unit-comp : ∀ {U} → α.η U ∘ N.η.η U ≈ M.η.η U
    mult-comp : ∀ {U} → α.η U ∘ (N.μ.η U) ≈ M.μ.η U ∘ α.η (M.F.₀ U) ∘ N.F.₁ (α.η U)

-- monad 2-cell in the sense of https://ncatlab.org/nlab/show/monad#the_bicategory_of_monads
record Monad²⇒ {M : Monad C} {N : Monad D} (Γ Δ : Monad⇒ M N) : Set (o ⊔ ℓ ⊔ e) where

  private
    module M = Monad M
    module N = Monad N
    module Γ = Monad⇒ Γ
    module Δ = Monad⇒ Δ

  field
    m : NaturalTransformation Γ.X Δ.X

  module m = NaturalTransformation m

  open module D = Category D using (_∘_; _≈_)

  field
    comm : ∀ {U} → Δ.α.η U ∘ N.F.₁ (m.η U) ≈ m.η (M.F.₀ U) ∘ Γ.α.η U

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:
module Issue679a where

data ty : Set where
  _`→_ : ty → ty → ty

⟦_⟧ : ty → Set
⟦ A `→ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

eq : ∀ (σ : ty) (a b : ⟦ σ ⟧) → Set
eq (A `→ B) f g = ∀ {a : ⟦ A ⟧} → eq B (f a) (g a)

eq-sym : ∀ σ {f g} (h : eq σ f g) → eq σ g f
eq-sym (A `→ B) h with B
... | B' = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive vectors
------------------------------------------------------------------------

{-# OPTIONS --without-K --guardedness --sized-types #-}

module Codata.Musical.Covec where

open import Codata.Musical.Notation
open import Codata.Musical.Conat as Coℕ using (Coℕ; zero; suc; _+_)
open import Codata.Musical.Cofin using (Cofin; zero; suc)
open import Codata.Musical.Colist as Colist using (Colist; []; _∷_)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product using (_,_)
open import Function using (_∋_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- The type

infixr 5 _∷_
data Covec {a} (A : Set a) : Coℕ → Set a where
  []  : Covec A zero
  _∷_ : ∀ {n} (x : A) (xs : ∞ (Covec A (♭ n))) → Covec A (suc n)

module _ {a} {A : Set a} where

 ∷-injectiveˡ : ∀ {a b} {n} {as bs} → (Covec A (suc n) ∋ a ∷ as) ≡ b ∷ bs → a ≡ b
 ∷-injectiveˡ P.refl = P.refl

 ∷-injectiveʳ : ∀ {a b} {n} {as bs} → (Covec A (suc n) ∋ a ∷ as) ≡ b ∷ bs → as ≡ bs
 ∷-injectiveʳ P.refl = P.refl

------------------------------------------------------------------------
-- Some operations

map : ∀ {a b} {A : Set a} {B : Set b} {n} → (A → B) → Covec A n → Covec B n
map f []       = []
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

module _ {a} {A : Set a} where

 fromVec : ∀ {n} → Vec A n → Covec A (Coℕ.fromℕ n)
 fromVec []       = []
 fromVec (x ∷ xs) = x ∷ ♯ fromVec xs

 fromColist : (xs : Colist A) → Covec A (Colist.length xs)
 fromColist []       = []
 fromColist (x ∷ xs) = x ∷ ♯ fromColist (♭ xs)

 take : ∀ m {n} → Covec A (m + n) → Covec A m
 take zero    xs       = []
 take (suc n) (x ∷ xs) = x ∷ ♯ take (♭ n) (♭ xs)

 drop : ∀ m {n} → Covec A (Coℕ.fromℕ m + n) → Covec A n
 drop zero    xs       = xs
 drop (suc n) (x ∷ xs) = drop n (♭ xs)

 replicate : ∀ n → A → Covec A n
 replicate zero    x = []
 replicate (suc n) x = x ∷ ♯ replicate (♭ n) x

 lookup : ∀ {n} → Cofin n → Covec A n → A
 lookup zero    (x ∷ xs) = x
 lookup (suc n) (x ∷ xs) = lookup n (♭ xs)

 infixr 5 _++_

 _++_ : ∀ {m n} → Covec A m → Covec A n → Covec A (m + n)
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)

 [_] : A → Covec A (suc (♯ zero))
 [ x ] = x ∷ ♯ []

------------------------------------------------------------------------
-- Equality and other relations

-- xs ≈ ys means that xs and ys are equal.

 infix 4 _≈_

 data _≈_ : ∀ {n} (xs ys : Covec A n) → Set a where
   []  : [] ≈ []
   _∷_ : ∀ {n} x {xs ys}
         (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → _≈_ {n = suc n} (x ∷ xs) (x ∷ ys)

-- x ∈ xs means that x is a member of xs.

 infix 4 _∈_

 data _∈_ : ∀ {n} → A → Covec A n → Set a where
   here  : ∀ {n x  } {xs}                   → _∈_ {n = suc n} x (x ∷ xs)
   there : ∀ {n x y} {xs} (x∈xs : x ∈ ♭ xs) → _∈_ {n = suc n} x (y ∷ xs)

-- xs ⊑ ys means that xs is a prefix of ys.

 infix 4 _⊑_

 data _⊑_ : ∀ {m n} → Covec A m → Covec A n → Set a where
   []  : ∀ {n} {ys : Covec A n} → [] ⊑ ys
   _∷_ : ∀ {m n} x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) →
         _⊑_ {m = suc m} {suc n} (x ∷ xs) (x ∷ ys)

------------------------------------------------------------------------
-- Some proofs

setoid : ∀ {a} → Set a → Coℕ → Setoid _ _
setoid A n = record
  { Carrier       = Covec A n
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : ∀ {n} → Reflexive (_≈_ {n = n})
  refl {x = []}     = []
  refl {x = x ∷ xs} = x ∷ ♯ refl

  sym : ∀ {n} → Symmetric (_≈_ {A = A} {n})
  sym []        = []
  sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)

  trans : ∀ {n} → Transitive (_≈_ {A = A} {n})
  trans []        []         = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

poset : ∀ {a} → Set a → Coℕ → Poset _ _ _
poset A n = record
  { Carrier        = Covec A n
  ; _≈_            = _≈_
  ; _≤_            = _⊑_
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = Setoid.isEquivalence (setoid A n)
      ; reflexive     = reflexive
      ; trans         = trans
      }
    ; antisym  = antisym
    }
  }
  where
  reflexive : ∀ {n} → _≈_ {n = n} ⇒ _⊑_
  reflexive []        = []
  reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈)

  trans : ∀ {n} → Transitive (_⊑_ {n = n})
  trans []        _          = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

  tail : ∀ {n x y xs ys} →
         _∷_ {n = n} x xs ⊑ _∷_ {n = n} y ys → ♭ xs ⊑ ♭ ys
  tail (_ ∷ p) = ♭ p

  antisym : ∀ {n} → Antisymmetric (_≈_ {n = n}) _⊑_
  antisym []       [] = []
  antisym (x ∷ p₁) p₂ = x ∷ ♯ antisym (♭ p₁) (tail p₂)

map-cong : ∀ {a b} {A : Set a} {B : Set b} {n} (f : A → B) → _≈_ {n = n} =[ map f ]⇒ _≈_
map-cong f []        = []
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)

take-⊑ : ∀ {a} {A : Set a} m {n} (xs : Covec A (m + n)) → take m xs ⊑ xs
take-⊑ zero    xs       = []
take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ (♭ n) (♭ xs)

------------------------------------------------------------------------
-- Legacy

import Codata.Covec as C
open import Codata.Thunk
import Size

module _ {a} {A : Set a} where

  fromMusical : ∀ {i n} → Covec A n → C.Covec A i (Coℕ.fromMusical n)
  fromMusical []       = C.[]
  fromMusical (x ∷ xs) = x C.∷ λ where .force → fromMusical (♭ xs)

  toMusical : ∀ {n} → C.Covec A Size.∞ n → Covec A (Coℕ.toMusical n)
  toMusical C.[]       = []
  toMusical (x C.∷ xs) = x ∷ ♯ toMusical (xs .force)


text:
open import FRP.JS.Behaviour using ( Beh ; map ; [_] )
open import FRP.JS.DOM using ( DOM ; text ; _++_ )
open import FRP.JS.RSet using ( ⟦_⟧ )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing )
open import FRP.JS.String using ( String )
open import FRP.JS.Geolocation using ( geolocation )
open import FRP.JS.Geolocation.Coords using ( Coords ; toString )

module FRP.JS.Demo.Geolocation where

show : Maybe Coords → String
show nothing       = "unknown"
show (just coords) = toString coords

main : ∀ {w} → ⟦ Beh (DOM w) ⟧
main =
  text ["Current location: "] ++
  text (map show geolocation) ++
  text ["."]

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Bool

data D (A : Set) : Set where
  con : (a : A) → D A

pr : ∀ {A} → D A → A
pr (con a) = a

postulate
  f : D Bool → Bool
  prf : pr ≡ f

{-# REWRITE prf #-}


text:
{-
This file proves the monotonicity of potential function over reductions.
CorrectBinding is required in order to guarantee that SI and SC introduced
by the loop never accidentally capture signals in the loop body.

canₖ-monotonic : ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ k →
    k ∈ Canₖ r' θ →
    k ∈ Canₖ r θ

canₛ-monotonic : ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ S' →
    Signal.unwrap S' ∈ Canₛ r' θ →
    Signal.unwrap S' ∈ Canₛ r θ

canₛₕ-monotonic : ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ s' →
    SharedVar.unwrap s' ∈ Canₛₕ r' θ →
    SharedVar.unwrap s' ∈ Canₛₕ r θ

In addition to the main lemmas, there are various random small propositions
dealing with the computatin of the calculation of Can in the loop body
(the big ρ-θ-emit-present term introduced by the loop-unroll rule).
-}
module can-function-preserve where

open import sn-calculus
open import utility

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Properties
open import Esterel.Context
  using (EvaluationContext1 ; EvaluationContext ; _⟦_⟧e ; _≐_⟦_⟧e)
open import Esterel.Context.Properties
  using (unplug ; Erefl)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Data.Bool
  using (Bool ; true ; false ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; _++_ ; map ; concatMap ; foldr)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using (++⁻)
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _≟_ ; _+_)
open import Data.Product
  using (Σ ; proj₁ ; proj₂ ; ∃ ; _,_ ; _,′_ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function
  using (_∘_ ; _∋_ ; id)
open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; _≢_ ; refl ; trans ; sym ; cong ; subst
       ; inspect ; Reveal_·_is_ ; [_] ; module ≡-Reasoning)

open EvaluationContext1
open _≐_⟦_⟧e

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ListSet Data.Nat._≟_
  using (set-subtract ; set-subtract-[] ; set-subtract-split ; set-subtract-merge
       ; set-subtract-notin ; set-subtract-[a]≡set-remove
       ; set-remove-mono-∈ ; set-remove-removed ; set-remove-not-removed)

canₛ-present-lemma : ∀ S p q θ →
  ∀ S' →
    Signal.unwrap S' ∈ Canₛ (present S ∣⇒ p ∣⇒ q) θ →
    Signal.unwrap S' ∈ Canₛ p θ ⊎ Signal.unwrap S' ∈ Canₛ q θ
canₛ-present-lemma S p q θ S' S'∈can-present with Env.Sig∈ S θ
canₛ-present-lemma S p q θ S' S'∈can-present | yes S∈
  with Env.sig-stats {S} θ S∈
... | Signal.present = inj₁ S'∈can-present
... | Signal.absent  = inj₂ S'∈can-present
... | Signal.unknown = ++⁻ (Canₛ p θ) S'∈can-present
canₛ-present-lemma S p q θ S' S'∈can-present | no  S∉ =
  ++⁻ (Canₛ p θ) S'∈can-present

canₛₕ-present-lemma : ∀ S p q θ →
  Canₛₕ p θ ≡ [] → Canₛₕ q θ ≡ [] →
  Canₛₕ (present S ∣⇒ p ∣⇒ q) θ ≡ []
canₛₕ-present-lemma S p q θ can-p≡[] can-q≡[] with Env.Sig∈ S θ
canₛₕ-present-lemma S p q θ can-p≡[] can-q≡[] | yes S∈
  with Env.sig-stats {S} θ S∈
... | Signal.present = can-p≡[]
... | Signal.absent  = can-q≡[]
... | Signal.unknown rewrite can-p≡[] | can-q≡[] = refl
canₛₕ-present-lemma S p q θ can-p≡[] can-q≡[] | no  S∉
  rewrite can-p≡[] | can-q≡[] = refl

canₖ-monotonic : ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ k →
    k ∈ Canₖ r' θ →
    k ∈ Canₖ r θ

canₛ-monotonic : ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ S' →
    Signal.unwrap S' ∈ Canₛ r' θ →
    Signal.unwrap S' ∈ Canₛ r θ

canₛₕ-monotonic : ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ s' →
    SharedVar.unwrap s' ∈ Canₛₕ r' θ →
    SharedVar.unwrap s' ∈ Canₛₕ r θ

canθₖ-monotonic : ∀ sigs S' → ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ k →
    k ∈ Canθₖ sigs S' r' θ →
    k ∈ Canθₖ sigs S' r θ

canθₛ-monotonic : ∀ sigs S'' → ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ S' →
    Signal.unwrap S' ∈ Canθₛ sigs S'' r' θ →
    Signal.unwrap S' ∈ Canθₛ sigs S'' r θ

canθₛₕ-monotonic : ∀ sigs S' → ∀ {BV FV} θ r r' →
  CorrectBinding r BV FV →
  r sn⟶₁ r' →
  ∀ s' →
    SharedVar.unwrap s' ∈ Canθₛₕ sigs S' r' θ →
    SharedVar.unwrap s' ∈ Canθₛₕ sigs S' r θ

canθₖ-monotonic [] S' cb red = canₖ-monotonic cb red
canθₖ-monotonic (nothing ∷ sigs) S' = canθₖ-monotonic sigs (suc S')
canθₖ-monotonic (just Signal.present ∷ sigs) S' θ
  = canθₖ-monotonic sigs (suc S') (θ ← _)
canθₖ-monotonic (just Signal.absent ∷ sigs) S' θ
  = canθₖ-monotonic sigs (suc S') (θ ← _)
canθₖ-monotonic (just Signal.unknown ∷ sigs) S' θ r r' cb red
  with any (_≟_ S') (Canθₛ sigs (suc S') r  (θ ← ([S]-env (S' ₛ))))
     | any (_≟_ S') (Canθₛ sigs (suc S') r' (θ ← ([S]-env (S' ₛ))))
... | yes S'∈Canr | yes S'∈Canr' = canθₖ-monotonic sigs (suc S') (θ ← [S]-env (S' ₛ)) r r' cb red
... | no  S'∉Canr | no  S'∉Canr' = canθₖ-monotonic sigs (suc S') (θ ← [S]-env-absent (S' ₛ)) r r' cb red
... | no  S'∉Canr | yes S'∈Canr'
  = ⊥-elim (S'∉Canr (canθₛ-monotonic sigs (suc S') (θ ← [S]-env (S' ₛ)) r r' cb red (S' ₛ) S'∈Canr'))
... | yes S'∈Canr | no  S'∉Canr'
   with (canθₖ-monotonic sigs (suc S') (θ ← [S]-env-absent (S' ₛ)) r r' cb red)
... | rec rewrite sym (Env.sig-set-clobber-single-as-← (S' ₛ) Signal.absent Signal.unknown θ (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ))
  = λ k k∈ →  canθₖ-set-sig-monotonic sigs (suc S') r (S' ₛ) (θ ← [S]-env (S' ₛ))
                                      (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ) Signal.absent
                                      (Env.sig-stats-1map-right-← (S' ₛ) Signal.unknown θ (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ))
                                      (n∉map-suc-n-+ S' (SigM.Dom' sigs))
                                      k (rec k k∈)

canθₛ-monotonic [] S' cb red = canₛ-monotonic cb red
canθₛ-monotonic (nothing ∷ sigs) S' = canθₛ-monotonic sigs (suc S')
canθₛ-monotonic (just Signal.present ∷ sigs) S' θ
  = canθₛ-monotonic sigs (suc S') (θ ← _)
canθₛ-monotonic (just Signal.absent ∷ sigs) S' θ
  = canθₛ-monotonic sigs (suc S') (θ ← _)
canθₛ-monotonic (just Signal.unknown ∷ sigs) S' θ r r' cb red
  with any (_≟_ S') (Canθₛ sigs (suc S') r  (θ ← ([S]-env (S' ₛ))))
     | any (_≟_ S') (Canθₛ sigs (suc S') r' (θ ← ([S]-env (S' ₛ))))
... | yes S'∈Canr | yes S'∈Canr' = canθₛ-monotonic sigs (suc S') (θ ← [S]-env (S' ₛ)) r r' cb red
... | no  S'∉Canr | no  S'∉Canr' = canθₛ-monotonic sigs (suc S') (θ ← [S]-env-absent (S' ₛ)) r r' cb red
... | no  S'∉Canr | yes S'∈Canr'
  = ⊥-elim (S'∉Canr (canθₛ-monotonic sigs (suc S') (θ ← [S]-env (S' ₛ)) r r' cb red (S' ₛ) S'∈Canr'))
... | yes S'∈Canr | no  S'∉Canr'
   with (canθₛ-monotonic sigs (suc S') (θ ← [S]-env-absent (S' ₛ)) r r' cb red)
... | rec rewrite sym (Env.sig-set-clobber-single-as-← (S' ₛ) Signal.absent Signal.unknown θ (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ))
  = λ k k∈ →  canθₛ-set-sig-monotonic sigs (suc S') r (S' ₛ) (θ ← [S]-env (S' ₛ))
                                      (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ) Signal.absent
                                      (Env.sig-stats-1map-right-← (S' ₛ) Signal.unknown θ (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ))
                                      (n∉map-suc-n-+ S' (SigM.Dom' sigs))
                                      (Signal.unwrap k) (rec k k∈)

canθₛₕ-monotonic [] S' cb red = canₛₕ-monotonic cb red
canθₛₕ-monotonic (nothing ∷ sigs) S' = canθₛₕ-monotonic sigs (suc S')
canθₛₕ-monotonic (just Signal.present ∷ sigs) S' θ
  = canθₛₕ-monotonic sigs (suc S') (θ ← _)
canθₛₕ-monotonic (just Signal.absent ∷ sigs) S' θ
  = canθₛₕ-monotonic sigs (suc S') (θ ← _)
canθₛₕ-monotonic (just Signal.unknown ∷ sigs) S' θ r r' cb red
  with any (_≟_ S') (Canθₛ sigs (suc S') r  (θ ← ([S]-env (S' ₛ))))
     | any (_≟_ S') (Canθₛ sigs (suc S') r' (θ ← ([S]-env (S' ₛ))))
... | yes S'∈Canr | yes S'∈Canr' = canθₛₕ-monotonic sigs (suc S') (θ ← [S]-env (S' ₛ)) r r' cb red
... | no  S'∉Canr | no  S'∉Canr' = canθₛₕ-monotonic sigs (suc S') (θ ← [S]-env-absent (S' ₛ)) r r' cb red
... | no  S'∉Canr | yes S'∈Canr'
  = ⊥-elim (S'∉Canr (canθₛ-monotonic sigs (suc S') (θ ← [S]-env (S' ₛ)) r r' cb red (S' ₛ) S'∈Canr'))
... | yes S'∈Canr | no  S'∉Canr'
   with (canθₛₕ-monotonic sigs (suc S') (θ ← [S]-env-absent (S' ₛ)) r r' cb red)
... | rec rewrite sym (Env.sig-set-clobber-single-as-← (S' ₛ) Signal.absent Signal.unknown θ (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ))
  = λ k k∈ →  canθₛₕ-set-sig-monotonic sigs (suc S') r (S' ₛ) (θ ← [S]-env (S' ₛ))
                                      (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ) Signal.absent
                                      (Env.sig-stats-1map-right-← (S' ₛ) Signal.unknown θ (Env.sig-∈-single-right-← (S' ₛ) Signal.unknown θ))
                                      (n∉map-suc-n-+ S' (SigM.Dom' sigs))
                                      (SharedVar.unwrap k) (rec k k∈)

canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-right hnothin q/done) k k∈can-r'-θ =
  any-map⁺² {xs = Code.nothin ∷ []} (λ k' → map (Code._⊔_ k') (Canₖ q θ))
    (here refl) (any-map⁺ (Code._⊔_ Code.nothin) k∈can-r'-θ)
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-right (hexit n) (dhalted hnothin)) k k∈can-r'-θ =
  k∈can-r'-θ
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-right (hexit n) (dhalted (hexit m))) k k∈can-r'-θ =
  k∈can-r'-θ
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-right (hexit n) (dpaused q/paused)) k k∈can-r'-θ
  rewrite canₖ-paused θ q/paused
  = k∈can-r'-θ
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-left (dhalted hnothin) q/halted) k k∈can-r'-θ =
  any-map⁺² {xs = Code.nothin ∷ []} (λ k' → map (Code._⊔_ k') (Canₖ q θ))
    (here refl) (any-map⁺ (Code._⊔_ Code.nothin) k∈can-r'-θ)
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-left (dhalted (hexit n)) hnothin) k k∈can-r'-θ =
  k∈can-r'-θ
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-left (dhalted (hexit n)) (hexit m)) k k∈can-r'-θ =
  k∈can-r'-θ
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-left (dpaused p/paused) hnothin) k k∈can-r'-θ
  rewrite canₖ-paused θ p/paused =
  k∈can-r'-θ
canₖ-monotonic θ (p ∥ q) _ cb
  (rpar-done-left (dpaused p/paused) (hexit m)) k k∈can-r'-θ
  rewrite canₖ-paused θ p/paused =
  k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (ris-present {S = S} {p = p} {E = E} S∈ θ'S≡present r≐E⟦present⟧) k k∈can-r'-θ
  rewrite canθ-is-present (Env.sig θ') S∈ θ r≐E⟦present⟧  θ'S≡present
  =   k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (ris-absent {S = S} S∈ θ'S≡absent r≐E⟦present⟧) k k∈can-r'-θ
  rewrite canθ-is-absent (Env.sig θ') S∈ θ r≐E⟦present⟧ θ'S≡absent
  =  k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (remit {S = S} {E = E} S∈ θ'S≢absent r≐E⟦emit⟧) k k∈can-r'-θ
  = canθₖ-emit θ' S∈ θ r≐E⟦emit⟧ θ'S≢absent ((canθₛ-membership (Env.sig θ') 0 r θ S
                                                (λ θ* → canₛ-capture-emit-signal θ* r≐E⟦emit⟧)))
               k k∈can-r'-θ
canₖ-monotonic θ (loop r) r' cb rloop-unroll k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ .(nothin >> r') r' cb
  rseq-done k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ .(exit _ >> _) .(exit _) cb
  rseq-exit k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ .(loopˢ (exit _)  _) .(exit _) cb
  rloopˢ-exit k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ (suspend r S) .r cb
  (rsuspend-done r/halted) k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ (trap r) .nothin   cb
  (rtrap-done hnothin) k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ (trap r) .nothin   cb
  (rtrap-done (hexit zero)) k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ (trap r) .(exit n) cb
  (rtrap-done (hexit (suc n))) k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ (signl S r) r' cb
  rraise-signal k k∈can-r'-θ = k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rraise-shared {s = s} {e = e} {p = p} {E = E} e' r≐E⟦shared⟧) k k∈can-r'-θ
  rewrite sym (unplug r≐E⟦shared⟧)
        | sym (canθₖ-raise-lemma{A = WAIT} (Env.sig θ') 0 θ E (tshared (δ e') s e p))
  =   k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rset-shared-value-old {s = s} {e = e} {E = E} e' s∈ θ's≡old r≐E⟦s⇐e⟧) k k∈can-r'-θ
  rewrite canθ-shr-var-irr (Env.sig (Env.set-shr {s} θ' s∈ SharedVar.new (δ e'))) 0 r θ θ refl
        | sym (unplug r≐E⟦s⇐e⟧)
  =   canθₖ-term-nothin-lemma
      (Env.sig (Env.set-shr {s} θ' s∈ SharedVar.new (δ e')))
      0
      θ
      E (tset-shr s e) k k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rset-shared-value-new {s = s} {e = e} {E = E} e' s∈ θ's≡new r≐E⟦s⇐e⟧) k k∈can-r'-θ
  rewrite canθ-shr-var-irr (Env.sig (Env.set-shr {s} θ' s∈ SharedVar.new (Env.shr-vals {s} θ' s∈ + δ e')))
                           0 r θ θ refl
        | sym (unplug r≐E⟦s⇐e⟧)
  = canθₖ-term-nothin-lemma
      (Env.sig (Env.set-shr {s} θ' s∈ SharedVar.new (Env.shr-vals {s} θ' s∈ + δ e')))
      0
      θ
      E (tset-shr s e) k k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rraise-var {x = x} {p = p} {e = e} {E = E} e' r≐E⟦var⟧) k k∈can-r'-θ
  rewrite sym (unplug r≐E⟦var⟧)
        | (canθₖ-raise-lemma (Env.sig θ') 0 θ E (tvar (δ e') x e p))
  =  k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rset-var {x = x} {e = e} {E = E} x∈ e' r≐E⟦x≔e⟧) k k∈can-r'-θ
  rewrite canθ-shr-var-irr (Env.sig (Env.set-var {x} θ' x∈ (δ e'))) 0 r θ θ refl
        | sym (unplug r≐E⟦x≔e⟧)
  =  canθₖ-term-nothin-lemma
      (Env.sig (Env.set-var {x} θ' x∈ (δ e')))
      0
      θ
      E (tset-var x e) k k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rif-false {p = p} {q = q} {x = x} {E = E} x∈ θ'x≡zero r≐E⟦if⟧) k k∈can-r'-θ
  rewrite sym (unplug r≐E⟦if⟧)
  =  canθₖ-if-false-lemma (Env.sig θ' ) 0 x p q θ E k k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rif-true {p = p} {q = q} {x = x} {E = E} x∈ θ'x≡suc r≐E⟦if⟧) k k∈can-r'-θ
  rewrite sym (unplug r≐E⟦if⟧)
  =  canθₖ-if-true-lemma (Env.sig θ') 0 x p q θ E k k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rabsence {S = S} S∈ θ'S≡unknown S∉can-r-θ') k k∈can-r'-θ
  rewrite Env.sig-switch-right S Signal.absent θ θ' S∈ (Env.sig-←-monoʳ S θ' θ S∈)
  = canθₖ-set-sig-monotonic-absence-lemma (Env.sig θ') 0 r S θ  S∈
      θ'S≡unknown k k∈can-r'-θ
  where
    θ←θ'        = θ ← θ'
    S∈Domθ←θ'   = Env.sig-←-monoʳ S θ' θ S∈
    ⟨θ←θ'⟩S≡θ'S = Env.sig-stats-←-right-irr' S θ θ' S∈ S∈Domθ←θ'
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (rreadyness {s = s} s∈ θ's≡old⊎θ's≡new s∉can-r-θ') k k∈can-r'-θ
  rewrite can-shr-var-irr r (θ ← θ')
            (θ ← Env.set-shr {s} θ' s∈ SharedVar.ready (Env.shr-vals {s} θ' s∈)) refl
  = k∈can-r'-θ
canₖ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb@(CBρ cb')
  (rmerge {θ₁ = .θ'} {θ₂ = θ''} {p = rin} {E = E} r≐E⟦ρθ''·rin⟧) k k∈can-r'-θ
  = canθₖ-mergeˡ (Env.sig θ') θ cb' r≐E⟦ρθ''·rin⟧ k k∈can-r'-θ

canₛ-monotonic θ (p ∥ q) _ cb
  (rpar-done-right p/halted q/done) S' S'∈can-r'-θ
  rewrite canₛ-done θ (value-max-done (dhalted p/halted) q/done (inj₁ p/halted))
  with S'∈can-r'-θ
... | ()
canₛ-monotonic θ (p ∥ q) _ cb
  (rpar-done-left p/done q/halted) S' S'∈can-r'-θ
  rewrite canₛ-done θ (value-max-done p/done (dhalted q/halted) (inj₂ q/halted))
  with S'∈can-r'-θ
... | ()
canₛ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (ris-present {S = S} S∈ θ'S≡present r≐E⟦present⟧) S' S'∈can-r'-θ
    rewrite canθ-is-present (Env.sig θ') S∈ θ r≐E⟦present⟧  θ'S≡present
  =  S'∈can-r'-θ
canₛ-monotonic θ (ρ⟨ θ' , A ⟩· r) r' cb
  (ris-absent {S = S} S∈ θ'S≡absent r≐E⟦absent⟧) S' S'∈can-r'-θ
    rewrite canθ-is-absent (Env.sig θ') S∈ θ r≐E⟦absent⟧  θ'S≡absent
  =  S'∈can-r'-θ
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (remit {S = S} {E = E} S∈ θ'S≢absent r≐E⟦emit⟧) S' S'∈can-ρθ''·r'-θ
  with set-subtract-merge
         {xs = Canθₛ (Env.sig (Env.set-sig {S} θ' S∈ Signal.present)) 0 r' θ}
         {ys = proj₁ (Dom θ'')}
         S'∈can-ρθ''·r'-θ
... | S'∈can-r'-θ←θ'' , S'∉Domθ''
  with set-subtract-split {ys = proj₁ (Dom θ')}
         (canθₛ-emit θ' S∈ θ r≐E⟦emit⟧ θ'S≢absent
           (canθₛ-membership (Env.sig θ') 0 r θ S
               (λ θ* → canₛ-capture-emit-signal θ* r≐E⟦emit⟧))
           S' S'∈can-r'-θ←θ'')
... | inj₁ S'∈can-r-θ←θ'-θ' = S'∈can-r-θ←θ'-θ'
... | inj₂ S'∈Domθ' =
  ⊥-elim (S'∉Domθ'' (Env.sig-set-mono' {S'} {S} {θ'} {Signal.present} {S∈} S'∈Domθ'))
canₛ-monotonic θ (loop r) r' cb rloop-unroll S' S'∈can-r'-θ = S'∈can-r'-θ
canₛ-monotonic θ .(nothin >> r') r' cb
  rseq-done S' S'∈can-r'-θ = S'∈can-r'-θ
canₛ-monotonic θ .(exit _ >> _) .(exit _) cb
  rseq-exit S' S'∈can-r'-θ = S'∈can-r'-θ
canₛ-monotonic θ .(loopˢ (exit _) _) .(exit _) cb
  rloopˢ-exit S' S'∈can-r'-θ = S'∈can-r'-θ
canₛ-monotonic θ (suspend r S) .r cb
  (rsuspend-done r/halted) S' S'∈can-r'-θ
  rewrite canₛ-done θ (dhalted r/halted) with S'∈can-r'-θ
... | ()
canₛ-monotonic θ (trap r) r' cb
  (rtrap-done r/halted) S' S'∈can-r'-θ
  rewrite canₛ-done θ (dhalted (↓-well-behaved _ r/halted)) with S'∈can-r'-θ
... | ()
canₛ-monotonic θ (signl S r) r' cb
  rraise-signal S' S'∈can-r'-θ
  rewrite SigMap.keys-1map S Signal.unknown
        | set-subtract-[a]≡set-remove (Canθₛ (Env.sig ([S]-env S)) 0 r θ) (Signal.unwrap S)
  =  S'∈can-r'-θ
canₛ-monotonic θ (ρ⟨ θ' , A ⟩· r) (ρ⟨ .θ' , .A ⟩· r') cb
  (rraise-shared {s = s} {e = e} {p = p} {E = E} e' r≐E⟦shared⟧) S' S'∈can-ρθ'·r'-θ
    rewrite sym (unplug r≐E⟦shared⟧)
          | sym (canθₛ-raise-lemma{A = WAIT} (Env.sig θ') 0 θ E (tshared (δ e') s e p))
    =  S'∈can-ρθ'·r'-θ

canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (rset-shared-value-old{s = s}{e = e}{E = E} e' s∈ θ's≡old r≐E⟦s⇐e⟧) S' S'∈can-ρθ''·r'-θ
  with set-subtract-merge{xs = Canθₛ (Env.sig θ'') 0 r' θ}{ys = proj₁ (Dom θ'')} S'∈can-ρθ''·r'-θ
... | S'∈can-r'-θ←θ'' , S'∉Domθ''
  with set-subtract-split {xs = Canθₛ (Env.sig θ') 0 r θ} {ys = proj₁ (Dom θ')} {z = Signal.unwrap S'}
         (subst
            (λ x → _ ∈ Canθₛ (Env.sig θ') 0 x θ)
            (unplug r≐E⟦s⇐e⟧)
            (canθₛ-term-nothin-lemma (Env.sig θ'') 0 θ E (tset-shr s e)
                              (Signal.unwrap S')  S'∈can-r'-θ←θ'' )  )
... | inj₁ S'∈can-r-θ←θ'-θ' = S'∈can-r-θ←θ'-θ' -- θ' and θ'' differ only by shared var Dom
... | inj₂ S'∈Domθ' = ⊥-elim (S'∉Domθ'' S'∈Domθ')
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (rset-shared-value-new{s = s}{e = e}{E = E} e' s∈ θ's≡new r≐E⟦s⇐e⟧) S' S'∈can-ρθ''·r'-θ
  with set-subtract-merge{xs = Canθₛ (Env.sig θ'') 0 r' θ}{ys = proj₁ (Dom θ'')} S'∈can-ρθ''·r'-θ
... | S'∈can-r'-θ←θ'' , S'∉Domθ''
  with set-subtract-split {xs = Canθₛ (Env.sig θ') 0 r θ} {ys = proj₁ (Dom θ')} {z = Signal.unwrap S'}
         (subst
            (λ x → _ ∈ Canθₛ (Env.sig θ') 0 x θ)
            (unplug r≐E⟦s⇐e⟧)
            (canθₛ-term-nothin-lemma (Env.sig θ'') 0 θ E (tset-shr s e)
                              (Signal.unwrap S')  S'∈can-r'-θ←θ'' ))
... | inj₁ S'∈can-r-θ←θ'-θ' = S'∈can-r-θ←θ'-θ'
... | inj₂ S'∈Domθ' = ⊥-elim (S'∉Domθ'' S'∈Domθ')
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .θ' , .A' ⟩· r') cb
  (rraise-var {x = x} {p = p} {e = e} {E = E} e' r≐E⟦var⟧) S' S'∈can-ρθ'·r'-θ
  rewrite sym (canθₛ-raise-lemma{A = WAIT} (Env.sig θ') 0 θ E (tvar (δ e') x e p)) | (unplug r≐E⟦var⟧) = S'∈can-ρθ'·r'-θ
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (rset-var {x = x} {e = e} {E = E}  x∈ e' r≐E⟦x≔e⟧) S' S'∈can-ρθ''·r'-θ
  with set-subtract-merge {xs = Canθₛ (Env.sig θ'') 0 r' θ}{ys = proj₁ (Dom θ'')} S'∈can-ρθ''·r'-θ
... | S'∈can-r'-θ←θ'' , S'∉Domθ''
  with set-subtract-split {xs = Canθₛ (Env.sig θ') 0 r θ} {ys = proj₁ (Dom θ')}{z = Signal.unwrap S'}
         ( (subst
            (λ x → _ ∈ Canθₛ (Env.sig θ') 0 x θ)
            (unplug r≐E⟦x≔e⟧)
            (canθₛ-term-nothin-lemma (Env.sig θ'') 0 θ E (tset-var x e)
                              (Signal.unwrap S')  S'∈can-r'-θ←θ'' )) )
... | inj₁ S'∈can-r-θ←θ'-θ' = S'∈can-r-θ←θ'-θ' -- θ' and θ'' differ only by seq var Dom
... | inj₂ S'∈Domθ' = ⊥-elim (S'∉Domθ'' S'∈Domθ')
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .θ' , .A' ⟩· r') cb
  (rif-false {p = p} {q = q} {x = x} {E = E} x∈ θ'x≡zero r≐E⟦if⟧) S' S'∈can-ρθ'·r'-θ
    with set-subtract-merge{xs = (proj₁ (Canθ (Env.sig θ') 0 r' θ))} {ys = proj₁ (Dom θ')}{z = (Signal.unwrap S')} S'∈can-ρθ'·r'-θ
... | S'∈can-r'-θ←θ' , S'∉Domθ' rewrite sym (unplug r≐E⟦if⟧) =
  set-subtract-notin (canθₛ-if-false-lemma (Env.sig θ') 0 x p q θ E (Signal.unwrap S')  S'∈can-r'-θ←θ') S'∉Domθ'
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .θ' , .A' ⟩· r') cb
  (rif-true {p = p} {q = q} {x = x} {E = E} x∈ θ'x≡suc r≐E⟦if⟧) S' S'∈can-ρθ'·r'-θ
    with set-subtract-merge{xs = (proj₁ (Canθ (Env.sig θ') 0 r' θ))} {ys = proj₁ (Dom θ')}{z = (Signal.unwrap S')} S'∈can-ρθ'·r'-θ
... | S'∈can-r'-θ←θ' , S'∉Domθ' rewrite sym (unplug r≐E⟦if⟧) =
  set-subtract-notin (canθₛ-if-true-lemma (Env.sig θ') 0 x p q θ E (Signal.unwrap S')  S'∈can-r'-θ←θ') S'∉Domθ'
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· .r) cb
  (rabsence {S = S} S∈ θ'S≡unknown S∉can-r-θ') S' S'∈can-ρθ''·r-θ
  rewrite Env.sig-switch-right S Signal.absent θ θ' S∈ (Env.sig-←-monoʳ S θ' θ S∈)
  with set-subtract-merge{xs = Canθₛ (Env.sig θ'') 0 r θ } {ys = proj₁ (Dom θ'')} S'∈can-ρθ''·r-θ
... | S'∈can-r-θ←θ'' , S'∉Domθ''
  with set-subtract-split{xs = (Canθₛ (Env.sig θ') 0 r θ)}{ys = fst (Dom θ')}
         (canθₛ-set-sig-monotonic-absence-lemma (Env.sig θ') 0 r S θ S∈
           θ'S≡unknown (Signal.unwrap S') S'∈can-r-θ←θ'')
  where
    θ←θ'        = θ ← θ'
    S∈Domθ←θ'   = Env.sig-←-monoʳ S θ' θ S∈
    ⟨θ←θ'⟩S≡θ'S = Env.sig-stats-←-right-irr' S θ θ' S∈ S∈Domθ←θ'
... | inj₁ S'∈can-r-θ←θ'-θ' = S'∈can-r-θ←θ'-θ'
... | inj₂ S'∈Domθ' =
  ⊥-elim
    (S'∉Domθ''
      (Env.sig-set-mono' {S'} {S} {θ'} {Signal.absent} {S∈}
        S'∈Domθ'))
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) r' cb
  (rreadyness {s = s} s∈ θ's≡old⊎θ's≡new s∉can-r-θ') S' S'∈can-r'-θ
  = S'∈can-r'-θ
canₛ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .(θ' ← θ'') , .(A-max A' _) ⟩· r') cb@(CBρ cb')
  (rmerge {θ₁ = .θ'} {θ₂ = θ''} {p = rin} {E = E} r≐E⟦ρθ''·rin⟧) S' S'∈can-ρθ'←θ''·r'-θ
  with set-subtract-merge
         {xs = Canθₛ (Env.sig (θ' ← θ'')) 0 r' θ}
         {ys = proj₁ (Dom (θ' ← θ''))}
         S'∈can-ρθ'←θ''·r'-θ
... | S'∈can-r'-θ←θ'←θ'' , S'∉Domθ'←θ''
  = set-subtract-notin
      (canθₛ-mergeˡ (Env.sig θ') θ cb' r≐E⟦ρθ''·rin⟧
        S' (S'∉Domθ'←θ'' ∘ Env.sig-←-monoʳ S' θ'' θ') S'∈can-r'-θ←θ'←θ'')
      (S'∉Domθ'←θ'' ∘ Env.sig-←-monoˡ S' θ' θ'')

canₛₕ-monotonic θ (p ∥ q) _ cb
  (rpar-done-right p/halted q/done) s' s'∈can-r'-θ
  rewrite canₛₕ-done θ (value-max-done (dhalted p/halted) q/done (inj₁ p/halted))
  with s'∈can-r'-θ
... | ()
canₛₕ-monotonic θ (p ∥ q) _ cb
  (rpar-done-left p/done q/halted) s' s'∈can-r'-θ
  rewrite canₛₕ-done θ (value-max-done p/done (dhalted q/halted) (inj₂ q/halted))
  with s'∈can-r'-θ
... | ()
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) r' cb
  (ris-present {S = S} S∈ θ'S≡present r≐E⟦present⟧) s' s'∈can-r'-θ
  rewrite canθ-is-present (Env.sig θ') S∈ θ r≐E⟦present⟧ θ'S≡present
  =  s'∈can-r'-θ
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) r' cb
  (ris-absent {S = S} S∈ θ'S≡absent r≐E⟦present⟧) s' s'∈can-r'-θ
  rewrite canθ-is-absent (Env.sig θ') S∈ θ r≐E⟦present⟧ θ'S≡absent
  =  s'∈can-r'-θ
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (remit {S = S} {E = E} S∈ θ'S≢absent r≐E⟦emit⟧) s' s'∈can-ρθ''·r'-θ
  with set-subtract-merge
         {xs = Canθₛₕ (Env.sig (Env.set-sig {S} θ' S∈ Signal.present)) 0 r' θ}
         {ys = proj₁ (proj₂ (Dom θ''))}
         s'∈can-ρθ''·r'-θ
... | s'∈can-r'-θ←θ'' , s'∉Domθ''
  with set-subtract-split {ys = proj₁ (proj₂ (Dom θ'))}
         (canθₛₕ-emit θ' S∈ θ r≐E⟦emit⟧ θ'S≢absent
           (canθₛ-membership (Env.sig θ') 0 r θ S
             (λ θ* → canₛ-capture-emit-signal θ* r≐E⟦emit⟧))
           s' s'∈can-r'-θ←θ'')
... | inj₁ s'∈can-r-θ←θ'-θ' = s'∈can-r-θ←θ'-θ'
... | inj₂ s'∈Domθ' = ⊥-elim (s'∉Domθ'' s'∈Domθ') -- θ' and θ'' differ only by sig
canₛₕ-monotonic θ (loop r) r' cb rloop-unroll s' s'∈can-r'-θ = s'∈can-r'-θ
canₛₕ-monotonic θ .(nothin >> r') r' cb
  rseq-done s' s'∈can-r'-θ = s'∈can-r'-θ
canₛₕ-monotonic θ .(exit _ >> _) .(exit _) cb
  rseq-exit s' s'∈can-r'-θ = s'∈can-r'-θ
canₛₕ-monotonic θ .(loopˢ (exit _) _) .(exit _) cb
  rloopˢ-exit s' s'∈can-r'-θ = s'∈can-r'-θ
canₛₕ-monotonic θ (suspend r S) .r cb
  (rsuspend-done r/halted) s' s'∈can-r'-θ
  rewrite canₛₕ-done θ (dhalted r/halted) with s'∈can-r'-θ
... | ()
canₛₕ-monotonic θ (trap r) r' cb
  (rtrap-done r/halted) s' s'∈can-r'-θ
  rewrite canₛₕ-done θ (dhalted (↓-well-behaved _ r/halted)) with s'∈can-r'-θ
... | ()
canₛₕ-monotonic θ (signl S r) r' cb
  rraise-signal s' s'∈can-r'-θ
  rewrite set-subtract-[] (Canθₛₕ (Env.sig ([S]-env S)) 0 r θ)
  =  s'∈can-r'-θ
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .θ' , .A' ⟩· r') cb
  (rraise-shared {s = s} {e = e} {p = p} {E = E} e' r≐E⟦shared⟧) s' s'∈can-ρθ'·r'-θ
  with set-subtract-merge {ys = proj₁ (proj₂ (Dom θ'))} s'∈can-ρθ'·r'-θ
... | s'∈can-r'-θ←θ' , s'∉Domθ' =

  set-subtract-notin
    (canθₛₕ-subset (Env.sig θ') 0 (E ⟦ ρ⟨ [s,δe]-env s (δ e') , WAIT ⟩· p ⟧e) r
       θ (λ θ* S* → canₛ-raise θ* (tshared (δ e') s e p) r≐E⟦shared⟧ S*)
       (λ θ* s* → canₛₕ-raise θ* (tshared (δ e') s e p) r≐E⟦shared⟧ s*) s'
       s'∈can-r'-θ←θ')
    s'∉Domθ'

canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (rset-shared-value-old {s = s} {e = e} {E = E} e' s∈ θ's≡old r≐E⟦s⇐e⟧) s' s'∈can-ρθ''·r'-θ
  with set-subtract-merge {ys = proj₁ (proj₂ (Dom θ''))} s'∈can-ρθ''·r'-θ
... | s'∈can-r'-θ←θ'' , s'∉Domθ''
  with set-subtract-split {ys = proj₁ (proj₂ (Dom θ'))}
         (canθₛₕ-subset (Env.sig θ') 0 (E ⟦ nothin ⟧e) r θ
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-shr s e) r≐E⟦s⇐e⟧ S*)
           (λ θ* s* → canₛₕ-term-nothin θ* θ* refl (tset-shr s e) r≐E⟦s⇐e⟧ s*)
           s' s'∈can-r'-θ←θ'')
... | inj₁ s'∈can-r-θ←θ'-θ' = s'∈can-r-θ←θ'-θ'
... | inj₂ s'∈Domθ' =
  ⊥-elim
    (s'∉Domθ''
      (Env.shr-set-mono' {s'} {s} {θ'} {SharedVar.new} {δ e'} {s∈}
        s'∈Domθ'))
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (rset-shared-value-new {s = s} {e = e} {E = E} e' s∈ θ's≡new r≐E⟦s⇐e⟧) s' s'∈can-ρθ''·r'-θ
  with set-subtract-merge {ys = proj₁ (proj₂ (Dom θ''))} s'∈can-ρθ''·r'-θ
... | s'∈can-r'-θ←θ'' , s'∉Domθ''
  with set-subtract-split {ys = proj₁ (proj₂ (Dom θ'))}
         (canθₛₕ-subset (Env.sig θ') 0 (E ⟦ nothin ⟧e) r θ
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-shr s e) r≐E⟦s⇐e⟧ S*)
           (λ θ* s* → canₛₕ-term-nothin θ* θ* refl (tset-shr s e) r≐E⟦s⇐e⟧ s*)
           s' s'∈can-r'-θ←θ'')
... | inj₁ s'∈can-r-θ←θ'-θ' = s'∈can-r-θ←θ'-θ'
... | inj₂ s'∈Domθ' =
  ⊥-elim
    (s'∉Domθ''
      (Env.shr-set-mono' {s'} {s} {θ'} {SharedVar.new}
        {Env.shr-vals {s} θ' s∈ + δ e'} {s∈}
        s'∈Domθ'))
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .θ' , .A' ⟩· r') cb
  (rraise-var {x = x} {p = p} {e = e} {E = E} e' r≐E⟦var⟧) s' s'∈can-ρθ'·r'-θ
  with set-subtract-merge {ys = proj₁ (proj₂ (Dom θ'))} s'∈can-ρθ'·r'-θ
... | s'∈can-r'-θ←θ' , s'∉Domθ' =
  set-subtract-notin
    (canθₛₕ-subset (Env.sig θ') 0 (E ⟦ ρ⟨ [x,δe]-env x (δ e') , WAIT ⟩· p ⟧e) r θ
      (λ θ* S* → canₛ-raise θ* (tvar (δ e') x e p) r≐E⟦var⟧ S*)
      (λ θ* s* → canₛₕ-raise θ* (tvar (δ e') x e p) r≐E⟦var⟧ s*)
      s' s'∈can-r'-θ←θ')
    s'∉Domθ'
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· r') cb
  (rset-var {x = x} {e = e} {E = E} x∈ e' r≐E⟦x≔e⟧) s' s'∈can-ρθ''·r'-θ
  with set-subtract-merge {ys = proj₁ (proj₂ (Dom θ''))} s'∈can-ρθ''·r'-θ
... | s'∈can-r'-θ←θ'' , s'∉Domθ''
  with set-subtract-split {ys = proj₁ (proj₂ (Dom θ'))}
         (canθₛₕ-subset (Env.sig θ') 0 (E ⟦ nothin ⟧e) r θ
           (λ θ* S* → canₛ-term-nothin θ* θ* refl (tset-var x e) r≐E⟦x≔e⟧ S*)
           (λ θ* s* → canₛₕ-term-nothin θ* θ* refl (tset-var x e) r≐E⟦x≔e⟧ s*)
           s' s'∈can-r'-θ←θ'')
... | inj₁ s'∈can-r-θ←θ'-θ' = s'∈can-r-θ←θ'-θ' -- θ' and θ'' differ only by seq var Dom
... | inj₂ s'∈Domθ' = ⊥-elim (s'∉Domθ'' s'∈Domθ')
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .θ' , .A' ⟩· r') cb
  (rif-false {p = p} {q = q} {x = x} {E = E} x∈ θ'x≡zero r≐E⟦if⟧) s' s'∈can-ρθ'·r'-θ
  with set-subtract-merge{xs = (thd (Canθ (Env.sig θ') 0 r' θ))} {ys = snd (Dom θ')}{z = (SharedVar.unwrap s')} s'∈can-ρθ'·r'-θ
... |  s'∈can-r'-θ←θ' , s'∉Domθ'
    rewrite sym (unplug r≐E⟦if⟧)
  = set-subtract-notin
      (canθₛₕ-if-false-lemma (Env.sig θ' ) 0 x p q θ E (SharedVar.unwrap s')   s'∈can-r'-θ←θ' )
      s'∉Domθ'
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .θ' , .A' ⟩· r') cb
  (rif-true {p = p} {q = q} {x = x} {E = E} x∈ θ'x≡suc r≐E⟦if⟧) s' s'∈can-ρθ'·r'-θ
    with set-subtract-merge{xs = (thd (Canθ (Env.sig θ') 0 r' θ))} {ys = snd (Dom θ')}{z = (SharedVar.unwrap s')} s'∈can-ρθ'·r'-θ
... |  s'∈can-r'-θ←θ' , s'∉Domθ'
    rewrite sym (unplug r≐E⟦if⟧)
  = set-subtract-notin
      (canθₛₕ-if-true-lemma (Env.sig θ' ) 0 x p q θ E (SharedVar.unwrap s')   s'∈can-r'-θ←θ' )
      s'∉Domθ'
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ θ'' , A'' ⟩· .r) cb
  (rabsence {S = S} S∈ θ'S≡unknown S∉can-r-θ') s' s'∈can-ρθ''·r-θ
  rewrite Env.sig-switch-right S Signal.absent θ θ' S∈ (Env.sig-←-monoʳ S θ' θ S∈)
 with set-subtract-merge {xs = Canθₛₕ (Env.sig θ'') 0 r θ }{ys = proj₁ (proj₂ (Dom θ''))} s'∈can-ρθ''·r-θ
... | s'∈can-r-θ←θ'' , s'∉Domθ''
  with set-subtract-split
         (canθₛₕ-set-sig-monotonic-absence-lemma (Env.sig θ') 0 r S θ S∈
            θ'S≡unknown (SharedVar.unwrap s') s'∈can-r-θ←θ'')
  where
    θ←θ'        = θ ← θ'
    S∈Domθ←θ'   = Env.sig-←-monoʳ S θ' θ S∈
    ⟨θ←θ'⟩S≡θ'S = Env.sig-stats-←-right-irr' S θ θ' S∈ S∈Domθ←θ'
... | inj₁ s'∈can-r-θ←θ'-θ' = s'∈can-r-θ←θ'-θ'
... | inj₂ s'∈Domθ' = ⊥-elim (s'∉Domθ'' s'∈Domθ') -- θ' and θ'' differ only by sig
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) r' cb
  (rreadyness {s = s} s∈ θ's≡old⊎θ's≡new s∉can-r-θ') s' s'∈can-r'-θ
  rewrite cong (proj₁ ∘ proj₂)
            (Env.shr-set-dom-eq s SharedVar.ready (Env.shr-vals {s} θ' s∈) θ' s∈)
        | can-shr-var-irr r (θ ← θ')
            (θ ← Env.set-shr {s} θ' s∈ SharedVar.ready (Env.shr-vals {s} θ' s∈)) refl
  = s'∈can-r'-θ
canₛₕ-monotonic θ (ρ⟨ θ' , A' ⟩· r) (ρ⟨ .(θ' ← θ'') , .(A-max A' _) ⟩· r') cb@(CBρ cb')
  (rmerge {θ₁ = .θ'} {θ₂ = θ''} {p = rin} {E = E} r≐E⟦ρθ''·rin⟧) s' s'∈can-ρθ'←θ''·r'-θ
  with set-subtract-merge
         {xs = Canθₛₕ (Env.sig (θ' ← θ'')) 0 r' θ}
         {ys = proj₁ (proj₂ (Dom (θ' ← θ'')))}
         s'∈can-ρθ'←θ''·r'-θ
 -- rewrite Env.←-assoc θ θ' θ''
... | s'∈can-r'-θ←θ'←θ'' , s'∉Domθ'←θ'' =
  set-subtract-notin
    (canθₛₕ-mergeˡ (Env.sig θ') θ cb' r≐E⟦ρθ''·rin⟧
      s' (s'∉Domθ'←θ'' ∘ Env.shr-←-monoʳ s' θ'' θ')
      s'∈can-r'-θ←θ'←θ'')
    (s'∉Domθ'←θ'' ∘ Env.shr-←-monoˡ s' θ' θ'')

infix 4 _⊑₃_
_⊑₃_ : SigSet.ST × CodeSet.ST × ShrSet.ST -> SigSet.ST × CodeSet.ST × ShrSet.ST -> Set
_⊑₃_ (Ss , ks , ss)  (Ss' , ks' , ss') =
  ((∀ S → (Signal.unwrap S) ∈ Ss → (Signal.unwrap S) ∈ Ss') ×
   (∀ k → k ∈ ks → k ∈ ks') ×
   (∀ s → (SharedVar.unwrap s) ∈ ss → (SharedVar.unwrap s) ∈ ss'))

can-antimonotonic :
  ∀ θ p q →
    CB p →
    p sn⟶₁ q →
  Can q θ ⊑₃ Can p θ
can-antimonotonic θ r r' CBr rsn⟶₁r' =
  (canₛ-monotonic  θ r r' CBr rsn⟶₁r' ,′
   canₖ-monotonic  θ r r' CBr rsn⟶₁r' ,′
   canₛₕ-monotonic  θ r r' CBr rsn⟶₁r')

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Lib.Eq where

open import Lib.Prelude as P hiding (String)
open import Lib.Nat renaming (_==_ to _=Nat=_)
open import Lib.Fin
open import Lib.List
open import Lib.Bool

-- Wrapper type, used to ensure that El is constructor-headed.

record String : Set where
  constructor string
  field unString : P.String

-- Codes for types supporting equality

data EqU : Set where
  nat    : EqU
  bool   : EqU
  string : EqU
  unit   : EqU
  fin    : Nat -> EqU
  list   : EqU -> EqU
  pair   : EqU -> EqU -> EqU

El : EqU -> Set
El nat        = Nat
El bool       = Bool
El string     = String
El unit       = Unit
El (fin n)    = Fin n
El (list u)   = List (El u)
El (pair u v) = El u × El v

primitive primStringEquality : P.String -> P.String -> Bool

infix 30 _==_

_==_ : {u : EqU} -> El u -> El u -> Bool
_==_ {nat}      n          m          = n =Nat= m
_==_ {fin n}    i          j          = finEq i j
_==_ {bool}     false      y          = not y
_==_ {bool}     true       y          = y
_==_ {string}   (string x) (string y) = primStringEquality x y
_==_ {unit}     _          _          = true
_==_ {list u}   []         []         = true
_==_ {list u}   (x :: xs)  (y :: ys)  = x == y && xs == ys
_==_ {list u}   _          _          = false
_==_ {pair u v} (x₁ , y₁)  (x₂ , y₂)  = x₁ == x₂ && y₁ == y₂