text:
{-
Basic properties of the Can function and utilities used in the reasoning.

The basic properties of the Can function include

- Can-θ function shadows the environment

    canθ-shadowing-irr' : ∀ sigs' S'' p S status θ θo →
      S ∈ map (_+_ S'') (SigMap.keys sigs') →
        Canθ sigs' S'' p ((θ ← [ (S ₛ) ↦ status ]) ← θo) ≡
        Canθ sigs' S'' p (θ ← θo)

    canθ-shadowing-irr : ∀ sigs' S'' p S status θ →
      Signal.unwrap S ∈ map (_+_ S'') (SigMap.keys sigs') →
        Canθ sigs' S'' p θ ≡
        Canθ sigs' S'' p (θ ← [ S ↦ status ])

- Can only look at signals in the environment. Actually, if we define Can on top
  of SigMap instead of the whole Env, this would be unnecessary:

  can-shr-var-irr : ∀ p θ θ' →
    Env.sig θ ≡ Env.sig θ' →
    Can p θ ≡ Can p θ'

- term-nothing captures those terms that cause a side-effect and reduce to nothin.

  canₖ-term-nothin : ∀ {r} θ → term-nothin r → Canₖ r θ ≡ (Code.nothin ∷ [])

  So the result of the Can function will not change:

  canₖ-term-nothin-lemma : ∀ {r₁ r₂} θ E →
    term-nothin r₁ → term-nothin r₂ →
    ∀ k →
      k ∈ Canₖ (E ⟦ r₁ ⟧e) θ →
      k ∈ Canₖ (E ⟦ r₂ ⟧e) θ

- paused terms have return code pause.

  canₖ-paused : ∀ {p} θ → paused p → Canₖ p θ ≡ (Code.pause ∷ [])

- done terms basically do nothing -- their Canₛ and Canₛₕ are empty.

  canₛ-done : ∀ {p} θ → done p → Canₛ p θ ≡ []

- Canₛ and Canₛₕ only captures free variables -- bound variables are removed. This
  property has a weaker converse: emit S and s ⇐ e in some *evaluation context*
  will be captured by Can.

  canₛ-⊆-FV-lemma : ∀ {p BV FV} θ →
    CorrectBinding p BV FV →
    ∀ S →
      S ∈ Canₛ p θ →
      S ∈ proj₁ FV

  (and its canₛₕ counterpart)

  canₛ-capture-emit-signal : ∀ {p S E} θ →
    p ≐ E ⟦ emit S ⟧e →
    Signal.unwrap S ∈ Canₛ p θ

  canₛₕ-capture-set-shared : ∀ {p s e E} θ →
    p ≐ E ⟦ s ⇐ e ⟧e →
    SharedVar.unwrap s ∈ Canₛₕ p θ

- Subset relation of Can bubbles up through Canθ (a weaker version). Note that
  the lemmas for codes and shared variables requires subset relation of the
  signals as well.

  canθₛ-subset : ∀ sigs S'' p q θ →
    (∀ θ' S →
       Signal.unwrap S ∈ Canₛ p θ' →
       Signal.unwrap S ∈ Canₛ q θ') →
    ∀ S →
      Signal.unwrap S ∈ Canθₛ sigs S'' p θ →
      Signal.unwrap S ∈ Canθₛ sigs S'' q θ

  canθₛₕ-subset : ∀ sigs S'' p q θ →
    (∀ θ' S →
       Signal.unwrap S ∈ Canₛ p θ' →
       Signal.unwrap S ∈ Canₛ q θ') →
    (∀ θ' s →
       SharedVar.unwrap s ∈ Canₛₕ p θ' →
       SharedVar.unwrap s ∈ Canₛₕ q θ') →
    ∀ s →
      SharedVar.unwrap s ∈ Canθₛₕ sigs S'' p θ →
      SharedVar.unwrap s ∈ Canθₛₕ sigs S'' q θ

  canθ'ₛ-subset-lemma : ∀ sigs S'' κ κ' θ →
    (∀ θ' S → S ∈ proj₁ (κ θ') → S ∈ proj₁ (κ' θ')) →
    (∀ θ S status S' →
      S' ∈ proj₁ (κ' (θ ← Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty)) →
      S' ∈ proj₁ (κ' (θ ← [S]-env S))) →
    ∀ S → S ∈ proj₁ (Canθ' sigs S'' κ θ) → S ∈ proj₁ (Canθ' sigs S'' κ' θ)

- Certain type of mootonicity relationship between the Can-θ function
  and the evaluation context

    canθₛ-p⊆canθₛ-E₁⟦p⟧ : ∀ sigs S'' θ E₁ pin →
      ∀ S' →
        Signal.unwrap S' ∈ Canθₛ sigs S'' pin θ →
        Signal.unwrap S' ∈ Canθₛ sigs S'' ((E₁ ∷ []) ⟦ pin ⟧e) θ

    canθₛ-E₁⟦p⟧⊆canθₛ-p : ∀ {pin E₁ E₁⟦nothin⟧ BV FV} sigs S'' θ →
      E₁⟦nothin⟧ ≐ (E₁ ∷ []) ⟦ nothin ⟧e →
      CorrectBinding E₁⟦nothin⟧ BV FV →

      distinct' (map (_+_ S'') (SigMap.keys sigs)) (proj₁ FV) →
      ∀ S' →
        Signal.unwrap S' ∉ proj₁ FV →
        Signal.unwrap S' ∈ Canθₛ sigs S'' ((E₁ ∷ []) ⟦ pin ⟧e) θ →
        Signal.unwrap S' ∈ Canθₛ sigs S'' pin θ

-}
module Esterel.Lang.CanFunction.Base where

open import utility
  renaming (_U̬_ to _∪_ ; _|̌_ to _-_)

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.SetSigMonotonic public -- weird dependency here
open import Esterel.Lang.Properties
  using (halted ; paused ; done)
open import Esterel.Context
  using (EvaluationContext1 ; EvaluationContext ; _⟦_⟧e ; _≐_⟦_⟧e)
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 EvaluationContext1
open _≐_⟦_⟧e

open import Data.Bool
  using (Bool ; not ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; _++_ ; map)
open import Data.List.Properties
  using (map-id)
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 ; maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _≟_ ; _+_)
open import Data.Nat.Properties.Simple
  using (+-comm ; +-right-identity)
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)

open halted
open paused
open done

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

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

-- Shorter local notation used in Can lemmas
[_↦_] : Signal → Signal.Status → Env
[ S ↦ status ] = Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty

data term-nothin : Term → Set where
  tnothin : term-nothin nothin
  temit : ∀ S → term-nothin (emit S)
  tset-shr : ∀ s e → term-nothin (s ⇐ e)
  tset-var : ∀ x e → term-nothin (x ≔ e)

data term-raise : ShrMap.Map (SharedVar.Status × ℕ) → VarMap.Map ℕ → Term → Term → Set where
  tshared : ∀ n s e p →
    term-raise ShrMap.[ s ↦ (SharedVar.old ,′ n) ]
           VarMap.empty
           (shared s ≔ e in: p) p
  tvar : ∀ n x e p →
    term-raise ShrMap.empty
           VarMap.[ x ↦ n ]
           (var x ≔ e in: p)    p

canₖ-term-nothin : ∀ {r} θ → term-nothin r → Canₖ r θ ≡ (Code.nothin ∷ [])
canₖ-term-nothin θ tnothin = refl
canₖ-term-nothin θ (temit S) = refl
canₖ-term-nothin θ (tset-shr s e) = refl
canₖ-term-nothin θ (tset-var x e) = refl

canₖ-paused : ∀ {p} θ → paused p → Canₖ p θ ≡ (Code.pause ∷ [])
canₖ-paused θ ppause                                             = refl
canₖ-paused θ (psuspend p/paused) rewrite canₖ-paused θ p/paused = refl
canₖ-paused θ (ptrap p/paused) rewrite canₖ-paused θ p/paused    = refl
canₖ-paused θ (ppar p/paused q/paused)
  rewrite canₖ-paused θ p/paused | canₖ-paused θ q/paused
  = refl
canₖ-paused {p >> q} θ (pseq p/paused) with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | no nothin∉can-p rewrite canₖ-paused θ p/paused = refl
... | yes nothin∈can-p rewrite canₖ-paused θ p/paused with nothin∈can-p
... | here ()
... | there ()

canₖ-paused {loopˢ p q} θ (ploopˢ p/paused) = canₖ-paused θ p/paused

canₛ-done : ∀ {p} θ → done p → Canₛ p θ ≡ []
canₛ-done θ (dhalted hnothin)   = refl
canₛ-done θ (dhalted (hexit _)) = refl
canₛ-done θ (dpaused ppause) = refl
canₛ-done θ (dpaused (ppar p/paused q/paused))
  rewrite canₛ-done θ (dpaused p/paused) | canₛ-done θ (dpaused q/paused)
  = refl
canₛ-done θ (dpaused (psuspend p/paused))
  rewrite canₛ-done θ (dpaused p/paused)
  = refl
canₛ-done θ (dpaused (ptrap p/paused))
  rewrite canₛ-done θ (dpaused p/paused)
  = refl
canₛ-done {loopˢ p q} θ (dpaused (ploopˢ p/paused)) = canₛ-done θ (dpaused p/paused)
canₛ-done {p >> q} θ (dpaused (pseq p/paused)) with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | no  nothin∉can-p rewrite canₛ-done θ (dpaused p/paused) = refl
... | yes nothin∈can-p rewrite canₖ-paused θ p/paused with nothin∈can-p
... | here ()
... | there ()

canₛₕ-done : ∀ {p} θ → done p → Canₛₕ p θ ≡ []
canₛₕ-done θ (dhalted hnothin)   = refl
canₛₕ-done θ (dhalted (hexit _)) = refl
canₛₕ-done θ (dpaused ppause) = refl
canₛₕ-done θ (dpaused (ppar p/paused q/paused))
  rewrite canₛₕ-done θ (dpaused p/paused) | canₛₕ-done θ (dpaused q/paused)
  = refl
canₛₕ-done θ (dpaused (psuspend p/paused))
  rewrite canₛₕ-done θ (dpaused p/paused)
  = refl
canₛₕ-done θ (dpaused (ptrap p/paused))
  rewrite canₛₕ-done θ (dpaused p/paused)
  = refl
canₛₕ-done {loopˢ p q} θ (dpaused (ploopˢ p/paused)) = canₛₕ-done θ (dpaused p/paused)
canₛₕ-done {p >> q} θ (dpaused (pseq p/paused)) with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | no  nothin∉can-p rewrite canₛₕ-done θ (dpaused p/paused) = refl
... | yes nothin∈can-p rewrite canₖ-paused θ p/paused with nothin∈can-p
... | here ()
... | there ()

can-shr-var-irr : ∀ p θ θ' →
  Env.sig θ ≡ Env.sig θ' →
  Can p θ ≡ Can p θ'

canθ-shr-var-irr : ∀ sigs S'' p θ θ' →
  Env.sig θ ≡ Env.sig θ' →
  Canθ sigs S'' p θ ≡ Canθ sigs S'' p θ'
canθ-shr-var-irr [] S'' p θ θ' θₛ≡θ'ₛ = can-shr-var-irr p θ θ' θₛ≡θ'ₛ
canθ-shr-var-irr (just Signal.present ∷ sigs) S'' p θ θ' θₛ≡θ'ₛ
  rewrite canθ-shr-var-irr sigs (suc S'') p
            (θ  ← [S]-env-present (S'' ₛ))
            (θ' ← [S]-env-present (S'' ₛ))
            (cong (λ sig* → SigMap.union sig* (Env.sig ([S]-env-present (S'' ₛ)))) θₛ≡θ'ₛ)
  = refl
canθ-shr-var-irr (just Signal.absent  ∷ sigs)  S'' p θ θ' θₛ≡θ'ₛ
  rewrite canθ-shr-var-irr sigs (suc S'') p
            (θ  ← [S]-env-absent (S'' ₛ))
            (θ' ← [S]-env-absent (S'' ₛ))
            (cong (λ sig* → SigMap.union sig* (Env.sig ([S]-env-absent (S'' ₛ)))) θₛ≡θ'ₛ)
  = refl
canθ-shr-var-irr (just Signal.unknown ∷ sigs) S'' p θ θ' θₛ≡θ'ₛ
  with any (S'' ≟_) (proj₁ (Canθ sigs (suc S'') p (θ  ← [S]-env (S'' ₛ))))
     | any (S'' ≟_) (proj₁ (Canθ sigs (suc S'') p (θ' ← [S]-env (S'' ₛ))))
... | yes S''∈canθ-θ←[S] | yes S''∈canθ-θ'←[S]
  rewrite canθ-shr-var-irr sigs (suc S'') p
            (θ ←  [S]-env (S'' ₛ))
            (θ' ← [S]-env (S'' ₛ))
            (cong (λ sig* → SigMap.union sig* (Env.sig ([S]-env (S'' ₛ)))) θₛ≡θ'ₛ)
  = refl
... | no  S''∉canθ-θ←[S] | no  S''∉canθ-θ'←[S]
  rewrite canθ-shr-var-irr sigs (suc S'') p
            (θ ← [S]-env-absent (S'' ₛ))
            (θ' ← [S]-env-absent (S'' ₛ))
            (cong (λ sig* → SigMap.union sig* (Env.sig ([S]-env-absent (S'' ₛ)))) θₛ≡θ'ₛ)
  = refl
... | no  S''∉canθ-θ←[S] | yes S''∈canθ-θ'←[S]
  rewrite canθ-shr-var-irr sigs (suc S'') p
            (θ ←  [S]-env (S'' ₛ))
            (θ' ← [S]-env (S'' ₛ))
            (cong (λ sig* → SigMap.union sig* (Env.sig ([S]-env (S'' ₛ)))) θₛ≡θ'ₛ)
  = ⊥-elim (S''∉canθ-θ←[S] S''∈canθ-θ'←[S])
... | yes S''∈canθ-θ←[S] | no  S''∉canθ-θ'←[S]
  rewrite canθ-shr-var-irr sigs (suc S'') p
            (θ ←  [S]-env (S'' ₛ))
            (θ' ← [S]-env (S'' ₛ))
            (cong (λ sig* → SigMap.union sig* (Env.sig ([S]-env (S'' ₛ)))) θₛ≡θ'ₛ)
  = ⊥-elim (S''∉canθ-θ'←[S] S''∈canθ-θ←[S])
canθ-shr-var-irr (nothing ∷ sigs) S'' p θ θ' θₛ≡θ'ₛ
  rewrite canθ-shr-var-irr sigs (suc S'') p θ θ' θₛ≡θ'ₛ
  = refl

can-shr-var-irr nothin θ θ' θₛ≡θ'ₛ = refl
can-shr-var-irr pause θ θ' θₛ≡θ'ₛ = refl
can-shr-var-irr (signl S p) θ θ' θₛ≡θ'ₛ
  rewrite canθ-shr-var-irr (Env.sig ([S]-env S)) 0 p θ θ' θₛ≡θ'ₛ
  = refl
can-shr-var-irr (present S ∣⇒ p ∣⇒ q) (Θ Ss ss xs) (Θ .Ss ss' xs') refl
  with Env.Sig∈ S (Θ Ss ss xs)
... | yes S∈
  rewrite can-shr-var-irr p (Θ Ss ss xs) (Θ Ss ss' xs') refl
        | can-shr-var-irr q (Θ Ss ss xs) (Θ Ss ss' xs') refl
  = refl
... | no  S∉
  rewrite can-shr-var-irr p (Θ Ss ss xs) (Θ Ss ss' xs') refl
        | can-shr-var-irr q (Θ Ss ss xs) (Θ Ss ss' xs') refl
  = refl
can-shr-var-irr (emit S) θ θ' θₛ≡θ'ₛ = refl
can-shr-var-irr (p ∥ q) θ θ' θₛ≡θ'ₛ
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
        | can-shr-var-irr q θ θ' θₛ≡θ'ₛ
  = refl
can-shr-var-irr (loop p) θ θ' θₛ≡θ'ₛ =
  can-shr-var-irr p θ θ' θₛ≡θ'ₛ
can-shr-var-irr (loopˢ p q) θ θ' θₛ≡θ'ₛ = can-shr-var-irr p θ θ' θₛ≡θ'ₛ
can-shr-var-irr (p >> q) θ θ' θₛ≡θ'ₛ
  with any (Code._≟_ Code.nothin) (Canₖ p θ)
     | any (Code._≟_ Code.nothin) (Canₖ p θ')
... | yes nothin∈can-p-θ | yes nothin∈can-p-θ'
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
        | can-shr-var-irr q θ θ' θₛ≡θ'ₛ
  = refl
... | yes nothin∈can-p-θ | (no nothin∉can-p-θ')
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
  = ⊥-elim (nothin∉can-p-θ' nothin∈can-p-θ)
... | no nothin∉can-p-θ | yes nothin∈can-p-θ'
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
  = ⊥-elim (nothin∉can-p-θ nothin∈can-p-θ')
... | no nothin∉can-p-θ | no nothin∉can-p-θ'
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
  = refl
can-shr-var-irr (suspend p S) θ θ' θₛ≡θ'ₛ =
  can-shr-var-irr p θ θ' θₛ≡θ'ₛ
can-shr-var-irr (trap p) θ θ' θₛ≡θ'ₛ
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
  = refl
can-shr-var-irr (exit x) θ θ' θₛ≡θ'ₛ = refl
can-shr-var-irr (shared s ≔ e in: p) θ θ' θₛ≡θ'ₛ
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
  = refl
can-shr-var-irr (s ⇐ e) θ θ' θₛ≡θ'ₛ = refl
can-shr-var-irr (var x ≔ e in: p) θ θ' θₛ≡θ'ₛ
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
  = refl
can-shr-var-irr (x ≔ e) θ θ' θₛ≡θ'ₛ = refl
can-shr-var-irr (if x ∣⇒ p ∣⇒ q) θ θ' θₛ≡θ'ₛ
  rewrite can-shr-var-irr p θ θ' θₛ≡θ'ₛ
        | can-shr-var-irr q θ θ' θₛ≡θ'ₛ
  = refl
can-shr-var-irr (ρ⟨ θ'' , A ⟩· p) θ θ' θₛ≡θ'ₛ
  rewrite canθ-shr-var-irr (Env.sig θ'') 0 p θ θ' θₛ≡θ'ₛ
  = refl

canₛ-capture-emit-signal : ∀ {p S E} θ →
  p ≐ E ⟦ emit S ⟧e →
  Signal.unwrap S ∈ Canₛ p θ
canₛ-capture-emit-signal θ dehole = here refl
canₛ-capture-emit-signal θ (depar₁ p≐E⟦emit⟧) =
  ++ˡ (canₛ-capture-emit-signal θ p≐E⟦emit⟧)
canₛ-capture-emit-signal {p ∥ _} θ (depar₂ p≐E⟦emit⟧) =
  ++ʳ (Canₛ p θ) (canₛ-capture-emit-signal θ p≐E⟦emit⟧)
canₛ-capture-emit-signal {loopˢ p _}  θ (deloopˢ p≐E⟦emit⟧) = canₛ-capture-emit-signal θ p≐E⟦emit⟧
canₛ-capture-emit-signal {p >> _}  θ (deseq p≐E⟦emit⟧)
  with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | yes nothin∈can-p = ++ˡ (canₛ-capture-emit-signal θ p≐E⟦emit⟧)
... | no  nothin∉can-p = canₛ-capture-emit-signal θ p≐E⟦emit⟧
canₛ-capture-emit-signal θ (desuspend p≐E⟦emit⟧) =
  canₛ-capture-emit-signal θ p≐E⟦emit⟧
canₛ-capture-emit-signal θ (detrap p≐E⟦emit⟧) =
  canₛ-capture-emit-signal θ p≐E⟦emit⟧

canₛₕ-capture-set-shared : ∀ {p s e E} θ →
  p ≐ E ⟦ s ⇐ e ⟧e →
  SharedVar.unwrap s ∈ Canₛₕ p θ
canₛₕ-capture-set-shared θ dehole = here refl
canₛₕ-capture-set-shared θ (depar₁ p≐E⟦s⇐e⟧) =
  ++ˡ (canₛₕ-capture-set-shared θ p≐E⟦s⇐e⟧)
canₛₕ-capture-set-shared {p ∥ _} θ (depar₂ q≐E⟦s⇐e⟧) =
  ++ʳ (Canₛₕ p θ) (canₛₕ-capture-set-shared θ q≐E⟦s⇐e⟧)
canₛₕ-capture-set-shared {loopˢ p _} θ (deloopˢ p≐E⟦s⇐e⟧) = canₛₕ-capture-set-shared θ p≐E⟦s⇐e⟧
canₛₕ-capture-set-shared {p >> _} θ (deseq p≐E⟦s⇐e⟧)
  with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | yes nothin∈can-p = ++ˡ (canₛₕ-capture-set-shared θ p≐E⟦s⇐e⟧)
... | no  nothin∉can-p = canₛₕ-capture-set-shared θ p≐E⟦s⇐e⟧
canₛₕ-capture-set-shared θ (desuspend p≐E⟦s⇐e⟧) =
  canₛₕ-capture-set-shared θ p≐E⟦s⇐e⟧
canₛₕ-capture-set-shared θ (detrap p≐E⟦s⇐e⟧) =
  canₛₕ-capture-set-shared θ p≐E⟦s⇐e⟧

canθₛ-membership : ∀ sigs S'' p θ S →
  (∀ θ' → Signal.unwrap S ∈ Canₛ p θ') →
  Signal.unwrap S ∈ Canθₛ sigs S'' p θ
canθₛ-membership [] S'' p θ S S∈can-p = S∈can-p θ
canθₛ-membership (nothing ∷ sigs) S'' p θ S S∈can-p =
  canθₛ-membership sigs (suc S'') p θ S S∈can-p
canθₛ-membership (just Signal.present ∷ sigs) S'' p θ S S∈can-p =
  canθₛ-membership sigs (suc S'') p (θ ← [S]-env-present (S'' ₛ)) S S∈can-p
canθₛ-membership (just Signal.absent ∷ sigs) S'' p θ S S∈can-p =
  canθₛ-membership sigs (suc S'') p (θ ← [S]-env-absent (S'' ₛ)) S S∈can-p
canθₛ-membership (just Signal.unknown ∷ sigs) S'' p θ S S∈can-p
  with any (_≟_ S'') (Canθₛ sigs (suc S'') p (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-p-θ←[S''] =
  canθₛ-membership sigs (suc S'') p (θ ← [S]-env (S'' ₛ)) S S∈can-p
... | no  S''∉canθ-p-θ←[S''] =
  canθₛ-membership sigs (suc S'') p (θ ← [S]-env-absent (S'' ₛ)) S S∈can-p

canθₛₕ-membership : ∀ sigs S'' p θ s →
  (∀ θ' → SharedVar.unwrap s ∈ Canₛₕ p θ') →
  SharedVar.unwrap s ∈ Canθₛₕ sigs S'' p θ
canθₛₕ-membership [] S'' p θ s s∈can-p = s∈can-p θ
canθₛₕ-membership (nothing ∷ sigs) S'' p θ s s∈can-p =
  canθₛₕ-membership sigs (suc S'') p θ s s∈can-p
canθₛₕ-membership (just Signal.present ∷ sigs) S'' p θ s s∈can-p =
  canθₛₕ-membership sigs (suc S'') p (θ ← [S]-env-present (S'' ₛ)) s s∈can-p
canθₛₕ-membership (just Signal.absent ∷ sigs) S'' p θ s s∈can-p =
  canθₛₕ-membership sigs (suc S'') p (θ ← [S]-env-absent (S'' ₛ)) s s∈can-p
canθₛₕ-membership (just Signal.unknown ∷ sigs) S'' p θ s s∈can-p
  with any (_≟_ S'') (Canθₛ sigs (suc S'') p (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-p-θ←[S''] =
  canθₛₕ-membership sigs (suc S'') p (θ ← [S]-env (S'' ₛ)) s s∈can-p
... | no  S''∉canθ-p-θ←[S''] =
  canθₛₕ-membership sigs (suc S'') p (θ ← [S]-env-absent (S'' ₛ)) s s∈can-p

canₛ-⊆-FV-lemma : ∀ {p BV FV} θ →
  CorrectBinding p BV FV →
  ∀ S →
    S ∈ Canₛ p θ →
    S ∈ proj₁ FV

canθₛ-⊆-FV-lemma : ∀ {p BV FV} sigs S'' θ →
  CorrectBinding p BV FV →
  ∀ S →
    S ∈ proj₁ (Canθ sigs S'' p θ) →
    S ∈ proj₁ FV
canθₛ-⊆-FV-lemma {FV = FV} [] S'' θ cb S S∈canθ-p-θ =
  canₛ-⊆-FV-lemma θ cb S S∈canθ-p-θ
canθₛ-⊆-FV-lemma (just Signal.present ∷ sigs) S'' θ cb S S∈canθ-p-θ =
  canθₛ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env-present (S'' ₛ)) cb S S∈canθ-p-θ
canθₛ-⊆-FV-lemma (just Signal.absent  ∷ sigs) S'' θ cb S S∈canθ-p-θ =
  canθₛ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) cb S S∈canθ-p-θ
canθₛ-⊆-FV-lemma {p} (just Signal.unknown ∷ sigs) S'' θ cb S S∈canθ-p-θ
  with any (S'' ≟_) (proj₁ (Canθ sigs (suc S'') p (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ-p-θ←[S] =
  canθₛ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env (S'' ₛ)) cb S S∈canθ-p-θ
... | no  S''∉canθ-p-θ←[S] =
  canθₛ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) cb S S∈canθ-p-θ
canθₛ-⊆-FV-lemma (nothing ∷ sigs) S'' θ cb S S∈canθ-p-θ =
  canθₛ-⊆-FV-lemma sigs (suc S'') θ cb S S∈canθ-p-θ

canₛ-⊆-FV-lemma θ CBnothing S ()
canₛ-⊆-FV-lemma θ CBpause S ()
canₛ-⊆-FV-lemma {signl S' p} θ (CBsig {FV = FV} cb) S S∈can-sig-p
  with Signal.unwrap S' Data.Nat.≟ S
... | yes refl =
  ⊥-elim (set-remove-removed {S} {Canθₛ (Env.sig ([S]-env S')) 0 p θ} S∈can-sig-p)
... | no  S'≢S
  rewrite set-subtract-[a]≡set-remove (proj₁ FV) (Signal.unwrap S')
  = set-remove-not-removed S'≢S
    (canθₛ-⊆-FV-lemma (Env.sig ([S]-env S')) 0 θ cb S
      (set-remove-mono-∈ (Signal.unwrap S') S∈can-sig-p))
canₛ-⊆-FV-lemma {present S' ∣⇒ p ∣⇒ q} θ (CBpresent {FVp = FVp} cbp cbq) S S∈can-S'?p:q
  with Env.Sig∈ S' θ
canₛ-⊆-FV-lemma {present S' ∣⇒ p ∣⇒ q} θ (CBpresent {FVp = FVp} cbp cbq) S S∈can-S'ᵘ?p:q
  | no  S'∉Domθ with ++⁻ (Canₛ p θ) S∈can-S'ᵘ?p:q
... | inj₁ S∈can-p = ++ʳ (Signal.unwrap S' ∷  []) (++ˡ (canₛ-⊆-FV-lemma θ cbp S S∈can-p))
... | inj₂ S∈can-q = ++ʳ (Signal.unwrap S' ∷ proj₁ FVp) (canₛ-⊆-FV-lemma θ cbq S S∈can-q)
canₛ-⊆-FV-lemma {present S' ∣⇒ p ∣⇒ q} θ (CBpresent {FVp = FVp} cbp cbq) S S∈can-S'ᵘ?p:q
  | yes S'∈Domθ with Env.sig-stats {S'} θ S'∈Domθ
... | Signal.present = ++ʳ (Signal.unwrap S' ∷  []) (++ˡ (canₛ-⊆-FV-lemma θ cbp S S∈can-S'ᵘ?p:q))
... | Signal.absent  = ++ʳ (Signal.unwrap S' ∷ proj₁ FVp) (canₛ-⊆-FV-lemma θ cbq S S∈can-S'ᵘ?p:q)
... | Signal.unknown with ++⁻ (Canₛ p θ) S∈can-S'ᵘ?p:q
... | inj₁ S∈can-p = ++ʳ (Signal.unwrap S' ∷  []) (++ˡ (canₛ-⊆-FV-lemma θ cbp S S∈can-p))
... | inj₂ S∈can-q = ++ʳ (Signal.unwrap S' ∷ proj₁ FVp) (canₛ-⊆-FV-lemma θ cbq S S∈can-q)
canₛ-⊆-FV-lemma θ CBemit S S∈can-p = S∈can-p
canₛ-⊆-FV-lemma {p ∥ q} θ (CBpar {FVp = FVp} cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) S S∈can-p∥q
  with ++⁻ (Canₛ p θ) S∈can-p∥q
... | inj₁ S∈can-p = ++ˡ (canₛ-⊆-FV-lemma θ cbp S S∈can-p)
... | inj₂ S∈can-q = ++ʳ (proj₁ FVp) (canₛ-⊆-FV-lemma θ cbq S S∈can-q)
canₛ-⊆-FV-lemma θ (CBloop cb BV≠FV) S S∈can-p =
  canₛ-⊆-FV-lemma θ cb S S∈can-p
canₛ-⊆-FV-lemma θ (CBloopˢ CBp CBq BVp≠FVq BVq≠FVq) S S∈can-loopˢp
  with canₛ-⊆-FV-lemma θ CBp S S∈can-loopˢp
... | sub = ++ˡ sub
canₛ-⊆-FV-lemma {p >> q} θ (CBseq {FVp = FVp} cbp cbq BVp≠FVq) S S∈can-p>>q
  with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | no  nothin∉can-p = ++ˡ (canₛ-⊆-FV-lemma θ cbp S S∈can-p>>q)
... | yes nothin∈can-p with ++⁻ (Canₛ p θ) S∈can-p>>q
... | inj₁ S∈can-p = ++ˡ (canₛ-⊆-FV-lemma θ cbp S S∈can-p)
... | inj₂ S∈can-q = ++ʳ (proj₁ FVp) (canₛ-⊆-FV-lemma θ cbq S S∈can-q)
canₛ-⊆-FV-lemma θ (CBsusp cb [S]≠BVp) S S∈can-p =
  there (canₛ-⊆-FV-lemma θ cb S S∈can-p)
canₛ-⊆-FV-lemma θ CBexit S ()
canₛ-⊆-FV-lemma θ (CBtrap cb) S S∈can-p =
  canₛ-⊆-FV-lemma θ cb S S∈can-p
canₛ-⊆-FV-lemma {shared _ ≔ e in: _} θ (CBshared {FV = FV} cb) S S∈can-p
  rewrite set-subtract-[] (proj₁ FV)
  = ++ʳ (proj₁ (FVₑ e)) (canₛ-⊆-FV-lemma θ cb S S∈can-p)
canₛ-⊆-FV-lemma θ CBsset S ()
canₛ-⊆-FV-lemma {var _ ≔ e in: _} θ (CBvar {FV = FV} cb) S S∈can-p
  rewrite set-subtract-[] (proj₁ FV)
  = ++ʳ (proj₁ (FVₑ e)) (canₛ-⊆-FV-lemma θ cb S S∈can-p)
canₛ-⊆-FV-lemma θ CBvset S ()
canₛ-⊆-FV-lemma {if _ ∣⇒ p ∣⇒ q} θ (CBif {FVp = FVp} cbp cbq) S S∈can-if-p-q
  with ++⁻ (Canₛ p θ) S∈can-if-p-q
... | inj₁ S∈can-p = ++ˡ (canₛ-⊆-FV-lemma θ cbp S S∈can-p)
... | inj₂ S∈can-q = ++ʳ (proj₁ FVp) (canₛ-⊆-FV-lemma θ cbq S S∈can-q)
canₛ-⊆-FV-lemma {ρ⟨ θ' , A ⟩· p} θ (CBρ cb) S S∈can-ρθp
  with set-subtract-merge {proj₁ (Canθ (Env.sig θ') 0 p θ)} {proj₁ (Dom θ')} S∈can-ρθp
... | S∈can-p-θ←θ' , S∉Domθ'
  with set-subtract-split (canθₛ-⊆-FV-lemma (Env.sig θ') 0 θ cb S S∈can-p-θ←θ')
... | inj₁ S∈FV = S∈FV
... | inj₂ S∈Domθ' = ⊥-elim (S∉Domθ' S∈Domθ')

canₛ-⊆-FV : ∀ {p BV FV} θ →
  CorrectBinding p BV FV →
  ∀ S →
    Signal.unwrap S ∈ Canₛ p θ →
    Signal.unwrap S ∈ proj₁ FV
canₛ-⊆-FV θ cb S = canₛ-⊆-FV-lemma θ cb (Signal.unwrap S)

canₛₕ-⊆-FV-lemma : ∀ {p BV FV} θ →
  CorrectBinding p BV FV →
  ∀ s →
    s ∈ Canₛₕ p θ →
    s ∈ proj₁ (proj₂ FV)

canθₛₕ-⊆-FV-lemma : ∀ {p BV FV} sigs S'' θ →
  CorrectBinding p BV FV →
  ∀ s →
    s ∈ proj₂ (proj₂ (Canθ sigs S'' p θ)) →
    s ∈ proj₁ (proj₂ FV)
canθₛₕ-⊆-FV-lemma {FV = FV} [] S'' θ cb s s∈canθ-p-θ =
  canₛₕ-⊆-FV-lemma θ cb s s∈canθ-p-θ
canθₛₕ-⊆-FV-lemma (just Signal.present ∷ sigs) S'' θ cb s s∈canθ-p-θ =
  canθₛₕ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env-present (S'' ₛ)) cb s s∈canθ-p-θ
canθₛₕ-⊆-FV-lemma (just Signal.absent  ∷ sigs) S'' θ cb s s∈canθ-p-θ =
  canθₛₕ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) cb s s∈canθ-p-θ
canθₛₕ-⊆-FV-lemma {p} (just Signal.unknown ∷ sigs) S'' θ cb s s∈canθ-p-θ
  with any (S'' ≟_) (proj₁ (Canθ sigs (suc S'') p (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ-p-θ←[S] =
  canθₛₕ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env (S'' ₛ)) cb s s∈canθ-p-θ
... | no  S''∉canθ-p-θ←[S] =
  canθₛₕ-⊆-FV-lemma sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) cb s s∈canθ-p-θ
canθₛₕ-⊆-FV-lemma (nothing ∷ sigs) S'' θ cb s s∈canθ-p-θ =
  canθₛₕ-⊆-FV-lemma sigs (suc S'') θ cb s s∈canθ-p-θ

canₛₕ-⊆-FV-lemma θ CBnothing s ()
canₛₕ-⊆-FV-lemma θ CBpause s ()
canₛₕ-⊆-FV-lemma {signl S' p} θ (CBsig {FV = FV} cb) s s∈can-p
  rewrite set-subtract-[] (proj₁ (proj₂ FV))
  = canθₛₕ-⊆-FV-lemma (Env.sig ([S]-env S')) 0 θ cb s s∈can-p
canₛₕ-⊆-FV-lemma {present S' ∣⇒ p ∣⇒ q} θ (CBpresent {FVp = FVp} cbp cbq) s s∈can-S'?p:q
  with Env.Sig∈ S' θ
canₛₕ-⊆-FV-lemma {present S' ∣⇒ p ∣⇒ q} θ (CBpresent {FVp = FVp} cbp cbq) s s∈can-S'ᵘ?p:q
  | no  S'∉Domθ with ++⁻ (Canₛₕ p θ) s∈can-S'ᵘ?p:q
... | inj₁ s∈can-p = ++ˡ (canₛₕ-⊆-FV-lemma θ cbp s s∈can-p)
... | inj₂ s∈can-q = ++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV-lemma θ cbq s s∈can-q)
canₛₕ-⊆-FV-lemma {present S' ∣⇒ p ∣⇒ q} θ (CBpresent {FVp = FVp} cbp cbq) s s∈can-S'ᵘ?p:q
  | yes S'∈Domθ with Env.sig-stats {S'} θ S'∈Domθ
... | Signal.present = ++ˡ (canₛₕ-⊆-FV-lemma θ cbp s s∈can-S'ᵘ?p:q)
... | Signal.absent  = ++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV-lemma θ cbq s s∈can-S'ᵘ?p:q)
... | Signal.unknown with ++⁻ (Canₛₕ p θ) s∈can-S'ᵘ?p:q
... | inj₁ s∈can-p = ++ˡ (canₛₕ-⊆-FV-lemma θ cbp s s∈can-p)
... | inj₂ s∈can-q = ++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV-lemma θ cbq s s∈can-q)
canₛₕ-⊆-FV-lemma θ CBemit s ()
canₛₕ-⊆-FV-lemma {p ∥ q} θ (CBpar {FVp = FVp} cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) s s∈can-p∥q
  with ++⁻ (Canₛₕ p θ) s∈can-p∥q
... | inj₁ s∈can-p = ++ˡ (canₛₕ-⊆-FV-lemma θ cbp s s∈can-p)
... | inj₂ s∈can-q = ++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV-lemma θ cbq s s∈can-q)
canₛₕ-⊆-FV-lemma θ (CBloop cb BV≠FV) s s∈can-p =
  canₛₕ-⊆-FV-lemma θ cb s s∈can-p
canₛₕ-⊆-FV-lemma θ (CBloopˢ CBp CBq BVp≠FVq BVq≠FVq) s s∈can-loopˢpq
  with canₛₕ-⊆-FV-lemma θ CBp s s∈can-loopˢpq
... | sub = ++ˡ sub
canₛₕ-⊆-FV-lemma {p >> q} θ (CBseq {FVp = FVp} cbp cbq BVp≠FVq) s s∈can-p>>q
  with any (Code._≟_ Code.nothin) (Canₖ p θ)
... | no  nothin∉can-p = ++ˡ (canₛₕ-⊆-FV-lemma θ cbp s s∈can-p>>q)
... | yes nothin∈can-p with ++⁻ (Canₛₕ p θ) s∈can-p>>q
... | inj₁ s∈can-p = ++ˡ (canₛₕ-⊆-FV-lemma θ cbp s s∈can-p)
... | inj₂ s∈can-q = ++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV-lemma θ cbq s s∈can-q)
canₛₕ-⊆-FV-lemma θ (CBsusp cb [S]≠BVp) s s∈can-p =
  canₛₕ-⊆-FV-lemma θ cb s s∈can-p
canₛₕ-⊆-FV-lemma θ CBexit s ()
canₛₕ-⊆-FV-lemma θ (CBtrap cb) s s∈can-p =
  canₛₕ-⊆-FV-lemma θ cb s s∈can-p
canₛₕ-⊆-FV-lemma {shared s' ≔ e in: p} θ (CBshared {FV = FV} cb) s s∈can-shared-p
  with SharedVar.unwrap s' Data.Nat.≟ s
... | yes refl = ⊥-elim (set-remove-removed {s} {Canₛₕ p θ} s∈can-shared-p)
... | no  s'≢s
  rewrite set-subtract-[a]≡set-remove (proj₁ (proj₂ FV)) (SharedVar.unwrap s')
  = ++ʳ (proj₁ (proj₂ (FVₑ e)))
    (set-remove-not-removed s'≢s
      (canₛₕ-⊆-FV-lemma θ cb s
        (set-remove-mono-∈ (SharedVar.unwrap s') s∈can-shared-p)))
canₛₕ-⊆-FV-lemma {s' ⇐ e} θ CBsset s s∈can-p = ++ˡ s∈can-p
canₛₕ-⊆-FV-lemma {var _ ≔ e in: _} θ (CBvar {FV = FV} cb) s s∈can-p
  rewrite set-subtract-[] (proj₁ (proj₂ FV))
  = ++ʳ (proj₁ (proj₂ (FVₑ e))) (canₛₕ-⊆-FV-lemma θ cb s s∈can-p)
canₛₕ-⊆-FV-lemma θ CBvset s ()
canₛₕ-⊆-FV-lemma {if _ ∣⇒ p ∣⇒ q} θ (CBif {FVp = FVp} cbp cbq) s s∈can-if-p-q
  with ++⁻ (Canₛₕ p θ) s∈can-if-p-q
... | inj₁ s∈can-p = ++ˡ (canₛₕ-⊆-FV-lemma θ cbp s s∈can-p)
... | inj₂ s∈can-q = ++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV-lemma θ cbq s s∈can-q)
canₛₕ-⊆-FV-lemma {ρ⟨ θ' , A ⟩· p} θ (CBρ cb) s s∈can-ρθp
  with set-subtract-merge
         {proj₂ (proj₂ (Canθ (Env.sig θ') 0 p θ))}
         {proj₁ (proj₂ (Dom θ'))}
         s∈can-ρθp
... | s∈can-p-θ←θ' , s∉Domθ'
  with set-subtract-split (canθₛₕ-⊆-FV-lemma (Env.sig θ') 0 θ cb s s∈can-p-θ←θ')
... | inj₁ s∈FV = s∈FV
... | inj₂ s∈Domθ' = ⊥-elim (s∉Domθ' s∈Domθ')

canₛₕ-⊆-FV : ∀ {p BV FV} θ →
  CorrectBinding p BV FV →
  ∀ s →
    SharedVar.unwrap s ∈ Canₛₕ p θ →
    SharedVar.unwrap s ∈ proj₁ (proj₂ FV)
canₛₕ-⊆-FV θ cb s = canₛₕ-⊆-FV-lemma θ cb (SharedVar.unwrap s)

canₖ-term-nothin-lemma : ∀ {r₁ r₂} θ E →
  term-nothin r₁ → term-nothin r₂ →
  ∀ k →
    k ∈ Canₖ (E ⟦ r₁ ⟧e) θ →
    k ∈ Canₖ (E ⟦ r₂ ⟧e) θ
canₖ-term-nothin-lemma θ [] r₁' r₂' k k∈can-E⟦r2⟧-θ'
  rewrite canₖ-term-nothin θ r₁' | canₖ-term-nothin θ r₂' = k∈can-E⟦r2⟧-θ'
canₖ-term-nothin-lemma θ (epar₁ q ∷ E) r₁' r₂' k k∈can-E⟦r2⟧-θ' =
  map-mono² Code._⊔_
    (canₖ-term-nothin-lemma θ E r₁' r₂')
    (λ _ → id)
    k k∈can-E⟦r2⟧-θ'
canₖ-term-nothin-lemma θ (epar₂ p ∷ E) r₁' r₂' k k∈can-E⟦r2⟧-θ' =
  map-mono² {xs = Canₖ p θ} Code._⊔_
    (λ _ → id)
    (canₖ-term-nothin-lemma θ E r₁' r₂')
    k
    k∈can-E⟦r2⟧-θ'
canₖ-term-nothin-lemma {r₁} {r₂} θ (eloopˢ q ∷ E) r₁' r₂' k k∈can-E⟦r2⟧-θ' = canₖ-term-nothin-lemma θ E r₁' r₂' k k∈can-E⟦r2⟧-θ'
canₖ-term-nothin-lemma {r₁} {r₂} θ (eseq q ∷ E) r₁' r₂' k k∈can-E⟦r2⟧-θ'
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ r₁ ⟧e) θ)
     | any (Code._≟_ Code.nothin) (Canₖ (E ⟦ r₂ ⟧e) θ)
... | yes nothin∈can-E⟦r₁⟧ | no  nothin∉can-E⟦r₂⟧ =
  ⊥-elim (nothin∉can-E⟦r₂⟧ (canₖ-term-nothin-lemma θ E r₁' r₂' Code.nothin nothin∈can-E⟦r₁⟧))
... | no  nothin∉can-E⟦r₁⟧ | yes nothin∈can-E⟦r₂⟧ =
  ⊥-elim (nothin∉can-E⟦r₁⟧ (canₖ-term-nothin-lemma θ E r₂' r₁' Code.nothin nothin∈can-E⟦r₂⟧))
... | no  nothin∉can-E⟦r₁⟧ | no  nothin∉can-E⟦r₂⟧ =
  canₖ-term-nothin-lemma θ E r₁' r₂' k k∈can-E⟦r2⟧-θ'
... | yes nothin∈can-E⟦r₁⟧ | yes nothin∈can-E⟦r₂⟧
  with ++⁻ (CodeSet.set-remove (Canₖ (E ⟦ r₁ ⟧e) θ) Code.nothin) k∈can-E⟦r2⟧-θ'
... | inj₂ k∈can-q =
  ++ʳ (CodeSet.set-remove (Canₖ (E ⟦ r₂ ⟧e) θ) Code.nothin) k∈can-q
... | inj₁ k∈can-E⟦r1⟧-nothin with Code.nothin Code.≟ k
... | yes refl =
  ⊥-elim (CodeSet.set-remove-removed {Code.nothin} {Canₖ (E ⟦ r₁ ⟧e) θ} k∈can-E⟦r1⟧-nothin)
... | no nothin≢k =
  ++ˡ (CodeSet.set-remove-not-removed nothin≢k
        (canₖ-term-nothin-lemma θ E r₁' r₂' k
          (CodeSet.set-remove-mono-∈ Code.nothin k∈can-E⟦r1⟧-nothin)))
canₖ-term-nothin-lemma θ (esuspend S' ∷ E) r₁' r₂' k k∈can-E⟦r2⟧-θ' =
  canₖ-term-nothin-lemma θ E r₁' r₂' k k∈can-E⟦r2⟧-θ'
canₖ-term-nothin-lemma θ (etrap ∷ E) r₁' r₂' k k∈can-E⟦r2⟧-θ' =
  map-mono Code.↓* (canₖ-term-nothin-lemma θ E r₁' r₂') k k∈can-E⟦r2⟧-θ'

canθₛ-subset-lemma : ∀ sigs S'' p q θ →
  (∀ θ' S → S ∈ Canₛ p θ' → S ∈ Canₛ q θ') →
  ∀ S → S ∈ Canθₛ sigs S'' p θ → S ∈ Canθₛ sigs S'' q θ
canθₛ-subset-lemma [] S'' p q θ canₛ-p⊆canₛ-q S S∈canθ-p-θ =
  canₛ-p⊆canₛ-q θ S S∈canθ-p-θ
canθₛ-subset-lemma (nothing ∷ sigs) S'' p q θ canₛ-p⊆canₛ-q S S∈canθ-p-θ =
  canθₛ-subset-lemma sigs (suc S'') p q θ canₛ-p⊆canₛ-q S S∈canθ-p-θ
canθₛ-subset-lemma (just Signal.present ∷ sigs) S'' p q θ canₛ-p⊆canₛ-q S S∈canθ-p-θ =
  canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-present (S'' ₛ)) canₛ-p⊆canₛ-q S S∈canθ-p-θ
canθₛ-subset-lemma (just Signal.absent ∷ sigs) S'' p q θ canₛ-p⊆canₛ-q S S∈canθ-p-θ =
  canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ)) canₛ-p⊆canₛ-q S S∈canθ-p-θ
canθₛ-subset-lemma (just Signal.unknown ∷ sigs) S'' p q θ canₛ-p⊆canₛ-q S S∈canθ-p-θ
  with any (_≟_ S'') (Canθₛ sigs (suc S'') p (θ ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs (suc S'') q (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-p-θ' | yes S''∈canθ-q-θ' =
  canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env (S'' ₛ)) canₛ-p⊆canₛ-q S S∈canθ-p-θ
... | no  S''∉canθ-p-θ' | no  S''∉canθ-q-θ' =
  canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ)) canₛ-p⊆canₛ-q S S∈canθ-p-θ
... | yes S''∈canθ-p-θ' | no  S''∉canθ-q-θ' =
  ⊥-elim
    (S''∉canθ-q-θ'
      (canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env (S'' ₛ)) canₛ-p⊆canₛ-q
        S'' S''∈canθ-p-θ'))
... | no  S''∉canθ-p-θ' | yes S''∈canθ-q-θ' =
  canθₛ-add-sig-monotonic sigs (suc S'') q θ (S'' ₛ) Signal.absent S
    (canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ)) canₛ-p⊆canₛ-q
      S S∈canθ-p-θ)

canθₛ-subset : ∀ sigs S'' p q θ →
  (∀ θ' S →
     Signal.unwrap S ∈ Canₛ p θ' →
     Signal.unwrap S ∈ Canₛ q θ') →
  ∀ S →
    Signal.unwrap S ∈ Canθₛ sigs S'' p θ →
    Signal.unwrap S ∈ Canθₛ sigs S'' q θ
canθₛ-subset sigs S'' p q θ canₛ-p⊆canₛ-q S S∈canθ-p-θ =
  canθₛ-subset-lemma sigs S'' p q θ
    (λ θ' S → canₛ-p⊆canₛ-q θ' (S ₛ))
    (Signal.unwrap S) S∈canθ-p-θ

canθₛₕ-subset-lemma : ∀ sigs S'' p q θ →
  (∀ θ' S → S ∈ Canₛ p θ' → S ∈ Canₛ q θ') →
  (∀ θ' s → s ∈ Canₛₕ p θ' → s ∈ Canₛₕ q θ') →
  ∀ s → s ∈ Canθₛₕ sigs S'' p θ → s ∈ Canθₛₕ sigs S'' q θ
canθₛₕ-subset-lemma [] S'' p q θ
  canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ =
  canₛₕ-p⊆canₛₕ-q θ s s∈canθ-p-θ
canθₛₕ-subset-lemma (nothing ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ =
  canθₛₕ-subset-lemma sigs (suc S'') p q θ
    canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ
canθₛₕ-subset-lemma (just Signal.present ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ =
  canθₛₕ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-present (S'' ₛ))
    canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ
canθₛₕ-subset-lemma (just Signal.absent ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ =
  canθₛₕ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ))
    canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ
canθₛₕ-subset-lemma (just Signal.unknown ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ
  with any (_≟_ S'') (Canθₛ sigs (suc S'') p (θ ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs (suc S'') q (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-p-θ' | yes S''∈canθ-q-θ' =
  canθₛₕ-subset-lemma sigs (suc S'') p q (θ ← [S]-env (S'' ₛ))
    canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ
... | no  S''∉canθ-p-θ' | no  S''∉canθ-q-θ' =
  canθₛₕ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ))
    canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ
... | yes S''∈canθ-p-θ' | no  S''∉canθ-q-θ' =
  ⊥-elim
    (S''∉canθ-q-θ'
      (canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env (S'' ₛ)) canₛ-p⊆canₛ-q
        S'' S''∈canθ-p-θ'))
... | no  S''∉canθ-p-θ' | yes S''∈canθ-q-θ' =
  canθₛₕ-add-sig-monotonic sigs (suc S'') q θ (S'' ₛ) Signal.absent s
    (canθₛₕ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ))
      canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ)

canθₛₕ-subset : ∀ sigs S'' p q θ →
  (∀ θ' S →
     Signal.unwrap S ∈ Canₛ p θ' →
     Signal.unwrap S ∈ Canₛ q θ') →
  (∀ θ' s →
     SharedVar.unwrap s ∈ Canₛₕ p θ' →
     SharedVar.unwrap s ∈ Canₛₕ q θ') →
  ∀ s →
    SharedVar.unwrap s ∈ Canθₛₕ sigs S'' p θ →
    SharedVar.unwrap s ∈ Canθₛₕ sigs S'' q θ
canθₛₕ-subset sigs S'' p q θ canₛ-p⊆canₛ-q canₛₕ-p⊆canₛₕ-q s s∈canθ-p-θ =
  canθₛₕ-subset-lemma sigs S'' p q θ
    (λ θ' S → canₛ-p⊆canₛ-q θ' (S ₛ)) (λ θ' s → canₛₕ-p⊆canₛₕ-q θ' (s ₛₕ))
    (SharedVar.unwrap s) s∈canθ-p-θ

canθₖ-subset-lemma : ∀ sigs S'' p q θ →
  (∀ θ' S → S ∈ Canₛ p θ' → S ∈ Canₛ q θ') →
  (∀ θ' k → k ∈ Canₖ p θ' → k ∈ Canₖ q θ') →
  ∀ k → k ∈ Canθₖ sigs S'' p θ → k ∈ Canθₖ sigs S'' q θ
canθₖ-subset-lemma [] S'' p q θ
  canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ =
  canₖ-p⊆canₖ-q θ k k∈canθ-p-θ
canθₖ-subset-lemma (nothing ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ =
  canθₖ-subset-lemma sigs (suc S'') p q θ
    canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ
canθₖ-subset-lemma (just Signal.present ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ =
  canθₖ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-present (S'' ₛ))
    canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ
canθₖ-subset-lemma (just Signal.absent ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ =
  canθₖ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ))
    canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ
canθₖ-subset-lemma (just Signal.unknown ∷ sigs) S'' p q θ
  canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ
  with any (_≟_ S'') (Canθₛ sigs (suc S'') p (θ ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs (suc S'') q (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-p-θ' | yes S''∈canθ-q-θ' =
  canθₖ-subset-lemma sigs (suc S'') p q (θ ← [S]-env (S'' ₛ))
    canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ
... | no  S''∉canθ-p-θ' | no  S''∉canθ-q-θ' =
  canθₖ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ))
    canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ
... | yes S''∈canθ-p-θ' | no  S''∉canθ-q-θ' =
  ⊥-elim
    (S''∉canθ-q-θ'
      (canθₛ-subset-lemma sigs (suc S'') p q (θ ← [S]-env (S'' ₛ)) canₛ-p⊆canₛ-q
        S'' S''∈canθ-p-θ'))
... | no  S''∉canθ-p-θ' | yes S''∈canθ-q-θ' =
  canθₖ-add-sig-monotonic sigs (suc S'') q θ (S'' ₛ) Signal.absent k
    (canθₖ-subset-lemma sigs (suc S'') p q (θ ← [S]-env-absent (S'' ₛ))
      canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ)

canθₖ-subset : ∀ sigs S'' p q θ →
  (∀ θ' S →
     Signal.unwrap S ∈ Canₛ p θ' →
     Signal.unwrap S ∈ Canₛ q θ') →
  (∀ θ' k →
     k ∈ Canₖ p θ' →
     k ∈ Canₖ q θ') →
  ∀ k →
    k ∈ Canθₖ sigs S'' p θ →
    k ∈ Canθₖ sigs S'' q θ
canθₖ-subset sigs S'' p q θ canₛ-p⊆canₛ-q canₖ-p⊆canₖ-q k k∈canθ-p-θ =
  canθₖ-subset-lemma sigs S'' p q θ
    (λ θ' S → canₛ-p⊆canₛ-q θ' (S ₛ)) canₖ-p⊆canₖ-q
    k k∈canθ-p-θ

canθₛ-E₁⟦p⟧⊆canθₛ-p : ∀ {pin E₁ E₁⟦nothin⟧ BV FV} sigs S'' θ →
  -- distinct (Dom sigs) (FV (E₁ ⟦ nothin ⟧))
  E₁⟦nothin⟧ ≐ (E₁ ∷ []) ⟦ nothin ⟧e →
  CorrectBinding E₁⟦nothin⟧ BV FV →

  distinct' (map (_+_ S'') (SigMap.keys sigs)) (proj₁ FV) →
  ∀ S' →
    Signal.unwrap S' ∉ proj₁ FV →
    Signal.unwrap S' ∈ Canθₛ sigs S'' ((E₁ ∷ []) ⟦ pin ⟧e) θ →
    Signal.unwrap S' ∈ Canθₛ sigs S'' pin θ
canθₛ-E₁⟦p⟧⊆canθₛ-p {pin} [] S'' θ (depar₁ pin≐E₁⟦nothin⟧) cb@(CBpar {FVp = FVp} cbp cbq _ _ _ _)
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
  with ++⁻ (Canₛ pin θ) S'∈canθ-E₁⟦pin⟧-θ
... | inj₁ S'∈can-pin-θ = S'∈can-pin-θ
... | inj₂ S'∈can-q-θ = ⊥-elim (S'∉FV (++ʳ (proj₁ FVp) (canₛ-⊆-FV θ cbq S' S'∈can-q-θ)))
canθₛ-E₁⟦p⟧⊆canθₛ-p {pin} {epar₂ p} [] S'' θ (depar₂ pin≐E₁⟦nothin⟧) cb@(CBpar cbp cbq _ _ _ _)
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
  with ++⁻ (Canₛ p θ) S'∈canθ-E₁⟦pin⟧-θ
... | inj₂ S'∈can-pin-θ = S'∈can-pin-θ
... | inj₁ S'∈can-p-θ = ⊥-elim (S'∉FV (++ˡ (canₛ-⊆-FV θ cbp S' S'∈can-p-θ)))
canθₛ-E₁⟦p⟧⊆canθₛ-p {pin} [] S'' θ (deloopˢ pin≐E₁⟦nothin⟧) cb@(CBloopˢ {FVp = FVp} cbp cbq _ _) = λ _ S' _ z → z
canθₛ-E₁⟦p⟧⊆canθₛ-p {pin} [] S'' θ (deseq pin≐E₁⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _)
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
  with any (Code._≟_ Code.nothin) (Canₖ pin θ)
... | no  nothin∉can-pin = S'∈canθ-E₁⟦pin⟧-θ
... | yes nothin∈can-pin with ++⁻ (Canₛ pin θ) S'∈canθ-E₁⟦pin⟧-θ
... | inj₁ S∈can-pin-θ = S∈can-pin-θ
... | inj₂ S∈can-q-θ = ⊥-elim (S'∉FV (++ʳ (proj₁ FVp) (canₛ-⊆-FV θ cbq S' S∈can-q-θ)))
canθₛ-E₁⟦p⟧⊆canθₛ-p {pin} [] S'' θ (desuspend pin≐E₁⟦nothin⟧) cb@(CBsusp cb' _)
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ = S'∈canθ-E₁⟦pin⟧-θ
canθₛ-E₁⟦p⟧⊆canθₛ-p {pin} [] S'' θ (detrap pin≐E₁⟦nothin⟧) cb@(CBtrap cb')
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ = S'∈canθ-E₁⟦pin⟧-θ
canθₛ-E₁⟦p⟧⊆canθₛ-p (nothing ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') θ pin≐E₁⟦nothin⟧ cb
      map-S''-+-sigs≠FV
      S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
canθₛ-E₁⟦p⟧⊆canθₛ-p (just Signal.present ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') (θ ← [S]-env-present (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
      S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
canθₛ-E₁⟦p⟧⊆canθₛ-p (just Signal.absent ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)) )
      S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
canθₛ-E₁⟦p⟧⊆canθₛ-p {pin} {E₁} (just Signal.unknown ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
  with any (_≟_ S'') (Canθₛ sigs (suc S'') pin (θ ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs (suc S'') ((E₁ ∷ []) ⟦ pin ⟧e) (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-p-θ←[S] | yes S''∈canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') (θ ← [S]-env (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
      S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
... | no  S''∉canθ-p-θ←[S] | no  S''∉canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
      S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ
... | yes S''∈canθ-p-θ←[S] | no  S''∉canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛ-add-sig-monotonic sigs (suc S'') pin θ (S'' ₛ) Signal.absent (Signal.unwrap S')
      (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
        (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
        S' S'∉FV S'∈canθ-E₁⟦pin⟧-θ)
... | no  S''∉canθ-p-θ←[S] | yes S''∈canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
        | +-comm S'' 0
  = ⊥-elim
      (S''∉canθ-p-θ←[S]
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') (θ ← [S]-env (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
          (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
          (S'' ₛ) (map-S''-+-sigs≠FV S'' (here refl)) S''∈canθ-E₁⟦p⟧-θ←[S]))

canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p : ∀ {pin E₁ E₁⟦nothin⟧ BV FV} sigs S'' θ →
  -- distinct (Dom sigs) (FV (E₁ ⟦ nothin ⟧))
  E₁⟦nothin⟧ ≐ (E₁ ∷ []) ⟦ nothin ⟧e →
  CorrectBinding E₁⟦nothin⟧ BV FV →

  distinct' (map (_+_ S'') (SigMap.keys sigs)) (proj₁ FV) →
  ∀ s →
    SharedVar.unwrap s ∉ proj₁ (proj₂ FV) →
    SharedVar.unwrap s ∈ Canθₛₕ sigs S'' ((E₁ ∷ []) ⟦ pin ⟧e) θ →
    SharedVar.unwrap s ∈ Canθₛₕ sigs S'' pin θ
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p {pin} [] S'' θ (depar₁ pin≐E₁⟦nothin⟧) cb@(CBpar {FVp = FVp} cbp cbq _ _ _ _)
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ
  with ++⁻ (Canₛₕ pin θ) s∈canθ-E₁⟦pin⟧-θ
... | inj₁ s∈can-pin-θ = s∈can-pin-θ
... | inj₂ s∈can-q-θ = ⊥-elim (s∉FV (++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV θ cbq s s∈can-q-θ)))
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p {pin} {epar₂ p} [] S'' θ (depar₂ pin≐E₁⟦nothin⟧) cb@(CBpar cbp cbq _ _ _ _)
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ
  with ++⁻ (Canₛₕ p θ) s∈canθ-E₁⟦pin⟧-θ
... | inj₂ s∈can-pin-θ = s∈can-pin-θ
... | inj₁ s∈can-p-θ = ⊥-elim (s∉FV (++ˡ (canₛₕ-⊆-FV θ cbp s s∈can-p-θ)))
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p {pin} [] S'' θ (deloopˢ pin≐E₁⟦nothin⟧) cb@(CBloopˢ {FVp = FVp} cbp cbq _ _) = λ _ s _ z → z
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p {pin} [] S'' θ (deseq pin≐E₁⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _)
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ
  with any (Code._≟_ Code.nothin) (Canₖ pin θ)
... | no  nothin∉can-pin = s∈canθ-E₁⟦pin⟧-θ
... | yes nothin∈can-pin with ++⁻ (Canₛₕ pin θ) s∈canθ-E₁⟦pin⟧-θ
... | inj₁ s∈can-pin-θ = s∈can-pin-θ
... | inj₂ s∈can-q-θ = ⊥-elim (s∉FV (++ʳ (proj₁ (proj₂ FVp)) (canₛₕ-⊆-FV θ cbq s s∈can-q-θ)))
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p {pin} [] S'' θ (desuspend pin≐E₁⟦nothin⟧) cb@(CBsusp cb' _)
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ = s∈canθ-E₁⟦pin⟧-θ
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p {pin} [] S'' θ (detrap pin≐E₁⟦nothin⟧) cb@(CBtrap cb')
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ = s∈canθ-E₁⟦pin⟧-θ
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (nothing ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p sigs (suc S'') θ pin≐E₁⟦nothin⟧ cb
      map-S''-+-sigs≠FV
      s s∉FV s∈canθ-E₁⟦pin⟧-θ
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (just Signal.present ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p sigs (suc S'') (θ ← [S]-env-present (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
      s s∉FV s∈canθ-E₁⟦pin⟧-θ
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (just Signal.absent ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)) )
      s s∉FV s∈canθ-E₁⟦pin⟧-θ
canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p {pin} {E₁} (just Signal.unknown ∷ sigs) S'' θ pin≐E₁⟦nothin⟧ cb
  map-S''-+-sigs≠FV s s∉FV s∈canθ-E₁⟦pin⟧-θ
  with any (_≟_ S'') (Canθₛ sigs (suc S'') pin (θ ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs (suc S'') ((E₁ ∷ []) ⟦ pin ⟧e) (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-p-θ←[S] | yes S''∈canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p sigs (suc S'') (θ ← [S]-env (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
      s s∉FV s∈canθ-E₁⟦pin⟧-θ
... | no  S''∉canθ-p-θ←[S] | no  S''∉canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
      (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
      s s∉FV s∈canθ-E₁⟦pin⟧-θ
... | yes S''∈canθ-p-θ←[S] | no  S''∉canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
  = canθₛₕ-add-sig-monotonic sigs (suc S'') pin θ (S'' ₛ) Signal.absent (SharedVar.unwrap s)
      (canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
        (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
        s s∉FV s∈canθ-E₁⟦pin⟧-θ)
... | no  S''∉canθ-p-θ←[S] | yes S''∈canθ-E₁⟦p⟧-θ←[S]
  rewrite map-+-compose-suc S'' (SigMap.keys sigs)
        | +-comm S'' 0
  = ⊥-elim
      (S''∉canθ-p-θ←[S]
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs (suc S'') (θ ← [S]-env (S'' ₛ)) pin≐E₁⟦nothin⟧ cb
          (distinct'-sym (dist':: (distinct'-sym map-S''-+-sigs≠FV)))
          (S'' ₛ) (map-S''-+-sigs≠FV S'' (here refl)) S''∈canθ-E₁⟦p⟧-θ←[S]))

canθₛ-p⊆canθₛ-E₁⟦p⟧ : ∀ sigs S'' θ E₁ pin →
  ∀ S' →
    Signal.unwrap S' ∈ Canθₛ sigs S'' pin θ →
    Signal.unwrap S' ∈ Canθₛ sigs S'' ((E₁ ∷ []) ⟦ pin ⟧e) θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ [] S'' θ (epar₁ q) pin S' S'∈canθ-sigs-pin-θ =
  ++ˡ S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ [] S'' θ (epar₂ p) pin S' S'∈canθ-sigs-pin-θ =
  ++ʳ (Canₛ p θ) S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ [] S'' θ (eloopˢ q) pin S' S'∈canθ-sigs-pin-θ = S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ [] S'' θ (eseq q) pin S' S'∈canθ-sigs-pin-θ
  with any (Code._≟_ Code.nothin) (Canₖ pin θ)
... | yes nothin∈can-pin = ++ˡ S'∈canθ-sigs-pin-θ
... | no  nothin∉can-pin = S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ [] S'' θ (esuspend S) pin S' S'∈canθ-sigs-pin-θ =
  S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ [] S'' θ etrap pin S' S'∈canθ-sigs-pin-θ =
  S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ (nothing ∷ sigs) S'' θ E₁ pin S' S'∈canθ-sigs-pin-θ =
  canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') θ E₁ pin S' S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ (just Signal.present ∷ sigs) S'' θ E₁ pin S' S'∈canθ-sigs-pin-θ =
  canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-present (S'' ₛ)) E₁ pin
    S' S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ (just Signal.absent ∷ sigs) S'' θ E₁ pin S' S'∈canθ-sigs-pin-θ =
  canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) E₁ pin
    S' S'∈canθ-sigs-pin-θ
canθₛ-p⊆canθₛ-E₁⟦p⟧ (just Signal.unknown ∷ sigs) S'' θ E₁ pin S' S'∈canθ-sigs-pin-θ
  with any (_≟_ S'') (Canθₛ sigs (suc S'') ((E₁ ∷ []) ⟦ pin ⟧e) (θ ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs (suc S'') pin (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-sigs-E₁⟦pin⟧-θ | yes S''∈canθ-sigs-pin-θ =
  canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env (S'' ₛ)) E₁ pin
    S' S'∈canθ-sigs-pin-θ
... | no  S''∉canθ-sigs-E₁⟦pin⟧   | no  S''∉canθ-sigs-pin-θ =
  canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) E₁ pin
    S' S'∈canθ-sigs-pin-θ
... | yes S''∈canθ-sigs-E₁⟦pin⟧   | no  S''∉canθ-sigs-pin-θ =
  canθₛ-add-sig-monotonic sigs (suc S'') ((E₁ ∷ []) ⟦ pin ⟧e)
    θ (S'' ₛ) Signal.absent (Signal.unwrap S')
    (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) E₁ pin
      S' S'∈canθ-sigs-pin-θ)
... | no  S''∉canθ-sigs-E₁⟦pin⟧   | yes S''∈canθ-sigs-pin-θ =
  ⊥-elim
    (S''∉canθ-sigs-E₁⟦pin⟧
      (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env (S'' ₛ)) E₁ pin
        (S'' ₛ) S''∈canθ-sigs-pin-θ))

canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ : ∀ sigs S'' θ E₁ pin →
  ∀ s →
    SharedVar.unwrap s ∈ Canθₛ sigs S'' pin θ →
    SharedVar.unwrap s ∈ Canθₛ sigs S'' ((E₁ ∷ []) ⟦ pin ⟧e) θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ [] S'' θ (epar₁ q) pin s s∈canθ-sigs-pin-θ =
  ++ˡ s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ [] S'' θ (epar₂ p) pin s s∈canθ-sigs-pin-θ =
  ++ʳ (Canₛ p θ) s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ [] S'' θ (eloopˢ q) pin s s∈canθ-sigs-pin-θ = s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ [] S'' θ (eseq q) pin s s∈canθ-sigs-pin-θ
  with any (Code._≟_ Code.nothin) (Canₖ pin θ)
... | yes nothin∈can-pin = ++ˡ s∈canθ-sigs-pin-θ
... | no  nothin∉can-pin = s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ [] S'' θ (esuspend S) pin s s∈canθ-sigs-pin-θ =
  s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ [] S'' θ etrap pin s s∈canθ-sigs-pin-θ =
  s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ (nothing ∷ sigs) S'' θ E₁ pin s s∈canθ-sigs-pin-θ =
  canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ sigs (suc S'') θ E₁ pin s s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ (just Signal.present ∷ sigs) S'' θ E₁ pin s s∈canθ-sigs-pin-θ =
  canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-present (S'' ₛ)) E₁ pin
    s s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ (just Signal.absent ∷ sigs) S'' θ E₁ pin s s∈canθ-sigs-pin-θ =
  canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) E₁ pin
    s s∈canθ-sigs-pin-θ
canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ (just Signal.unknown ∷ sigs) S'' θ E₁ pin s s∈canθ-sigs-pin-θ
  with any (_≟_ S'') (Canθₛ sigs (suc S'') ((E₁ ∷ []) ⟦ pin ⟧e) (θ ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs (suc S'') pin (θ ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-sigs-E₁⟦pin⟧-θ | yes S''∈canθ-sigs-pin-θ =
  canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env (S'' ₛ)) E₁ pin
    s s∈canθ-sigs-pin-θ
... | no  S''∉canθ-sigs-E₁⟦pin⟧   | no  S''∉canθ-sigs-pin-θ =
  canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) E₁ pin
    s s∈canθ-sigs-pin-θ
... | yes S''∈canθ-sigs-E₁⟦pin⟧   | no  S''∉canθ-sigs-pin-θ =
  canθₛ-add-sig-monotonic sigs (suc S'') ((E₁ ∷ []) ⟦ pin ⟧e)
    θ (S'' ₛ) Signal.absent (SharedVar.unwrap s)
    (canθₛₕ-p⊆canθₛₕ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env-absent (S'' ₛ)) E₁ pin
      s s∈canθ-sigs-pin-θ)
... | no  S''∉canθ-sigs-E₁⟦pin⟧   | yes S''∈canθ-sigs-pin-θ =
  ⊥-elim
    (S''∉canθ-sigs-E₁⟦pin⟧
      (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs (suc S'') (θ ← [S]-env (S'' ₛ)) E₁ pin
        (S'' ₛ) S''∈canθ-sigs-pin-θ))

canθ-shadowing-irr' : ∀ sigs' S'' p S status θ θo →
  S ∈ map (_+_ S'') (SigMap.keys sigs') →
    Canθ sigs' S'' p ((θ ← [ (S ₛ) ↦ status ]) ← θo) ≡
    Canθ sigs' S'' p (θ ← θo)
canθ-shadowing-irr' [] S'' p S status θ θo ()
canθ-shadowing-irr' (nothing ∷ sigs') S'' p S status θ θo S∈map-+-S''-sigs'
  rewrite map-+-compose-suc S'' (SigMap.keys sigs')
  = canθ-shadowing-irr' sigs' (suc S'') p S status θ θo S∈map-+-S''-sigs'
canθ-shadowing-irr' (just Signal.present ∷ sigs') S'' p S status θ θo (here refl)
  rewrite +-comm S'' 0
        | Env.sig-set-inner-clobber θ θo ([S]-env-present (S'' ₛ)) (S'' ₛ) status (Env.sig-∈-single (S'' ₛ) Signal.present)
  = refl
canθ-shadowing-irr' (just Signal.absent ∷ sigs') S'' p S status θ θo (here refl)
  rewrite +-comm S'' 0
        | Env.sig-set-inner-clobber θ θo ([S]-env-absent (S'' ₛ)) (S'' ₛ) status (Env.sig-∈-single (S'' ₛ) Signal.absent)
  = refl
canθ-shadowing-irr' (just Signal.unknown ∷ sigs') S'' p S status θ θo (here refl)
  with any (_≟_ S'') (Canθₛ sigs' (suc S'') p (((θ ← [ (S ₛ) ↦ status ]) ← θo) ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs' (suc S'') p ((θ ← θo) ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-sigs-θ←[S]-absent←θo←[S''] | yes S''∈canθ-sigs-θ←[S]←θo←[S'']
  rewrite +-comm S'' 0
        | Env.sig-set-inner-clobber θ θo ([S]-env (S'' ₛ)) (S'' ₛ) status (Env.sig-∈-single (S'' ₛ) Signal.unknown)
  = refl
... | no  S''∉canθ-sigs-θ←[S]-absent←θo←[S''] | no  S''∉canθ-sigs-θ←[S]←θo←[S'']
  rewrite +-comm S'' 0
        | Env.sig-set-inner-clobber θ θo ([S]-env-absent (S'' ₛ)) (S'' ₛ) status (Env.sig-∈-single (S'' ₛ) Signal.absent)
  = refl
... | yes S''∈canθ-sigs-θ←[S]-absent←θo←[S''] | no  S''∉canθ-sigs-θ←[S]←θo←[S'']
  rewrite +-comm S'' 0
        | Env.sig-set-inner-clobber θ θo ([S]-env (S'' ₛ)) (S'' ₛ) status (Env.sig-∈-single (S'' ₛ) Signal.unknown)
  = ⊥-elim (S''∉canθ-sigs-θ←[S]←θo←[S''] S''∈canθ-sigs-θ←[S]-absent←θo←[S''])
... | no  S''∉canθ-sigs-θ←[S]-absent←θo←[S''] | yes S''∈canθ-sigs-θ←[S]←θo←[S'']
  rewrite +-comm S'' 0
        | Env.sig-set-inner-clobber θ θo ([S]-env (S'' ₛ)) (S'' ₛ) status (Env.sig-∈-single (S'' ₛ) Signal.unknown)
  = ⊥-elim (S''∉canθ-sigs-θ←[S]-absent←θo←[S''] S''∈canθ-sigs-θ←[S]←θo←[S''])
canθ-shadowing-irr' (just Signal.present ∷ sigs') S'' p S status θ θo (there S∈map-+-S''-sigs')
  rewrite map-+-compose-suc S'' (SigMap.keys sigs')
        | sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env-present (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env-present (S'' ₛ)))
  = canθ-shadowing-irr' sigs' (suc S'') p S status θ (θo ← [S]-env-present (S'' ₛ)) S∈map-+-S''-sigs'
canθ-shadowing-irr' (just Signal.absent ∷ sigs') S'' p S status θ θo (there S∈map-+-S''-sigs')
  rewrite map-+-compose-suc S'' (SigMap.keys sigs')
        | sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env-absent (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env-absent (S'' ₛ)))
  = canθ-shadowing-irr' sigs' (suc S'') p S status θ (θo ← [S]-env-absent (S'' ₛ)) S∈map-+-S''-sigs'
canθ-shadowing-irr' (just Signal.unknown ∷ sigs') S'' p S status θ θo (there S∈map-+-S''-sigs')
  with any (_≟_ S'') (Canθₛ sigs' (suc S'') p (((θ ← [ (S ₛ) ↦ status ]) ← θo) ← [S]-env (S'' ₛ)))
     | any (_≟_ S'') (Canθₛ sigs' (suc S'') p ((θ ← θo) ← [S]-env (S'' ₛ)))
... | yes S''∈canθ-sigs-θ←[S]-absent←θo←[S''] | yes S''∈canθ-sigs-θ←[S]←θo←[S'']
  rewrite map-+-compose-suc S'' (SigMap.keys sigs')
        | sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env (S'' ₛ)))
  = canθ-shadowing-irr' sigs' (suc S'') p S status θ (θo ← [S]-env (S'' ₛ)) S∈map-+-S''-sigs'
... | no  S''∉canθ-sigs-θ←[S]-absent←θo←[S''] | no  S''∉canθ-sigs-θ←[S]←θo←[S'']
  rewrite map-+-compose-suc S'' (SigMap.keys sigs')
        | sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env-absent (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env-absent (S'' ₛ)))
  = canθ-shadowing-irr' sigs' (suc S'') p S status θ (θo ← [S]-env-absent (S'' ₛ)) S∈map-+-S''-sigs'
... | yes S''∈canθ-sigs-θ←[S]-absent←θo←[S''] | no  S''∉canθ-sigs-θ←[S]←θo←[S'']
  rewrite map-+-compose-suc S'' (SigMap.keys sigs')
        | sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env (S'' ₛ)))
        | canθ-shadowing-irr' sigs' (suc S'') p S status θ (θo ← [S]-env (S'' ₛ)) S∈map-+-S''-sigs'
  = ⊥-elim (S''∉canθ-sigs-θ←[S]←θo←[S''] S''∈canθ-sigs-θ←[S]-absent←θo←[S''])
... | no  S''∉canθ-sigs-θ←[S]-absent←θo←[S''] | yes S''∈canθ-sigs-θ←[S]←θo←[S'']
  rewrite map-+-compose-suc S'' (SigMap.keys sigs')
        | sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env (S'' ₛ)))
        | canθ-shadowing-irr' sigs' (suc S'') p S status θ (θo ← [S]-env (S'' ₛ)) S∈map-+-S''-sigs'
  = ⊥-elim (S''∉canθ-sigs-θ←[S]-absent←θo←[S''] S''∈canθ-sigs-θ←[S]←θo←[S''])

canθ-shadowing-irr : ∀ sigs' S'' p S status θ →
  Signal.unwrap S ∈ map (_+_ S'') (SigMap.keys sigs') →
    Canθ sigs' S'' p θ ≡
    Canθ sigs' S'' p (θ ← [ S ↦ status ])
canθ-shadowing-irr sigs' S'' p S status θ S∈map-+-S''-sigs'
  rewrite Env.←-comm Env.[]env (θ ← [ S ↦ status ]) distinct-empty-left
        | cong (Canθ sigs' S'' p) (Env.←-comm Env.[]env θ distinct-empty-left)
  = sym (canθ-shadowing-irr' sigs' S'' p (Signal.unwrap S) status
          θ Env.[]env S∈map-+-S''-sigs')

Canθₛunknown->Canₛunknown-help : ∀ S S' p →
  (S + S') ∈ Canθₛ SigMap.[ (S ₛ) ↦ Signal.unknown ] S' p Env.[]env →
  (S + S') ∈ Canₛ p [ ((S + S') ₛ) ↦ Signal.unknown ]
Canθₛunknown->Canₛunknown-help zero    S' p S+S'∈canθ-[S↦unknown]-S'
  with any (S' ≟_) (Canₛ p [ (S' ₛ) ↦ Signal.unknown ])
... | yes S'∈can-p-[S↦unknown] = S+S'∈canθ-[S↦unknown]-S'
... | no  S'∉can-p-[S↦unknown] =
  Data.Empty.⊥-elim
    (S'∉can-p-[S↦unknown]
      (Esterel.Lang.CanFunction.SetSigMonotonic.canθₛ-add-sig-monotonic
       [] 0 p Env.[]env (S' ₛ) Signal.absent S'
       S+S'∈canθ-[S↦unknown]-S'))
Canθₛunknown->Canₛunknown-help (suc S) S' p S+S'∈canθ-[S↦unknown]-S'
  -- trans (cong suc (+-comm S S')) (+-comm (suc S') S) : suc (S + S') ≡ S + (suc S')
  rewrite cong (λ n → Canₛ p [ (n ₛ) ↦ Signal.unknown ])
               (trans (cong suc (+-comm S S')) (+-comm (suc S') S))
        |       trans (cong suc (+-comm S S')) (+-comm (suc S') S)
  = Canθₛunknown->Canₛunknown-help S (suc S') p S+S'∈canθ-[S↦unknown]-S'

Canθₛunknown->Canₛunknown : ∀ S p ->
  (Signal.unwrap S) ∈ Canθₛ SigMap.[ S ↦ Signal.unknown ] 0 p Env.[]env →
  (Signal.unwrap S) ∈ Canₛ p [ S ↦ Signal.unknown ]
Canθₛunknown->Canₛunknown S p fact
  rewrite +-right-identity (Signal.unwrap S)
  with Canθₛunknown->Canₛunknown-help
          (Signal.unwrap S) zero p (add-zero (Signal.unwrap S) _ fact)
    where
    add-zero : ∀ s x -> s ∈ x -> (s + 0) ∈ x
    add-zero s x s+0∈x rewrite +-right-identity s = s+0∈x
... | thing rewrite +-right-identity (Signal.unwrap S) = thing

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --allow-unsolved-metas #-}

-- Andreas, 2014-12-06
-- Reported by sanzhiyan, Dec 4 2014

open import Data.Vec
open import Data.Fin
open import Data.Nat renaming (_+_ to _+N_)
open import Data.Nat.Solver
open import Relation.Binary.PropositionalEquality hiding ([_])
open +-*-Solver using (prove; solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_)

data prop : Set where
  F T   : prop
  _∧_ _∨_ : prop → prop → prop

infixl 4 _∧_ _∨_

Γ : (n : ℕ) → Set
Γ n = Vec prop n

infix 1 _⊢_

data _⊢_ : ∀ {n} → Γ n → prop → Set  where
  hyp     : ∀ {n}(C : Γ n)(v : Fin n) → C ⊢ (lookup v C)
  andI    : ∀ {n}{C : Γ n}{p p' : prop} → C ⊢ p → C ⊢ p' → C ⊢ p ∧ p'
  andEL   : ∀ {n}{C : Γ n}{p p' : prop} → C ⊢ p ∧ p' → C ⊢ p
  andER   : ∀ {n}{C : Γ n}{p p' : prop} → C ⊢ p ∧ p' → C ⊢ p'
  orIL    : ∀ {n}{C : Γ n}{p : prop}(p' : prop) → C ⊢ p → C ⊢ p ∨ p'
  orIR    : ∀ {n}{C : Γ n}{p' : prop}(p : prop) → C ⊢ p' → C ⊢ p ∨ p'
  orE     : ∀ {n}{C : Γ n}{p p' c : prop} → C ⊢ p ∨ p' → p ∷ C ⊢ c → p' ∷ C ⊢ c →  C ⊢ c

-- WAS:
-- The first two _ could not be solved before today's (2014-12-06) improvement of pruning.
-- Except for variables, they were applied to a huge neutral proof term coming from the ring solver.
-- Agda could not prune before the improved neutrality check implemented by Andrea(s) 2014-12-05/06.
--
-- As a consequence, Agda would often reattempt solving, each time doing the expensive
-- occurs check.  This would extremely slow down Agda.

weakening : ∀ {n m p p'}(C : Γ n)(C' : Γ m) → C ++ C' ⊢ p → C ++ [ p' ] ++ C' ⊢ p
weakening {n} {m} {p' = p'} C C' (hyp .(C ++ C') v) = subst (λ R → C ++ (_ ∷ C') ⊢ R) {!!}
          (hyp (C ++ (_ ∷ C')) (subst (λ x → Fin x) proof (inject₁ v))) where
        proof : suc (n +N m) ≡ n +N suc m
        proof = (solve 2 (λ n₁ m₁ → con 1 :+ (n₁ :+ m₁) := n₁ :+ (con 1 :+ m₁)) refl n m)
weakening C C' (andI prf prf') = andI (weakening C C' prf) (weakening C C' prf')
weakening C C' (andEL prf) = andEL (weakening C C' prf)
weakening C C' (andER prf) = andER (weakening C C' prf)
weakening C C' (orIL p'' prf) = orIL p'' (weakening C C' prf)
weakening C C' (orIR p prf) = orIR p (weakening C C' prf)
weakening C C' (orE prf prf₁ prf₂) = orE (weakening C C' prf) (weakening (_ ∷ C) C' prf₁) (weakening (_ ∷ C) C' prf₂)

-- Should check fast now and report the ? as unsolved meta.

ext: agda

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

-- Inspired by Thorsten Altenkirch's definition of Groupoids
-- see his OmegaCats repo on github.  And copumpkin's definition of
-- Category (see his categories repo, also on github).

module Groupoid where

open import Level using (zero)
open import Data.Empty using (⊥)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; proj₁; proj₂; _,_)
open import Function using (flip)
open import Relation.Binary
  using (Rel; IsEquivalence; Reflexive; Symmetric; Transitive;
         module IsEquivalence)

------------------------------------------------------------------------------
-- Useful

Rel0 : Set → Set₁
Rel0 A = Rel A zero

-- 1-groupoids are those where the various laws hold up to ≈.

record 1Groupoid : Set₁ where
  infixr 9 _∘_
  infixr 5 _↝_
  infix  4 _≈_
  field
    set      : Set₀
    _↝_      : set → set → Set
    _≈_      : ∀ {A B} → A ↝ B → A ↝ B → Set
    id       : ∀ {x} → x ↝ x
    _∘_      : ∀ {x y z} → y ↝ z → x ↝ y → x ↝ z
    _⁻¹      : ∀ {x y} → x ↝ y → y ↝ x
    lneutr   : ∀ {x y} (α : x ↝ y) → id ∘ α ≈ α
    rneutr   : ∀ {x y} (α : x ↝ y) → α ∘ id ≈ α
    assoc    : ∀ {w x y z} (α : y ↝ z) (β : x ↝ y) (δ : w ↝ x) →
               (α ∘ β) ∘ δ ≈ α ∘ (β ∘ δ)
    equiv    : ∀ {x y} → IsEquivalence (_≈_ {x} {y})
    linv     : ∀ {x y}(α : x ↝ y) → α ⁻¹ ∘ α ≈ id {x}
    rinv     : ∀ {x y}(α : x ↝ y) → α ∘ α ⁻¹ ≈ id {y}
    ∘-resp-≈ : ∀ {x y z} {f h : y ↝ z} {g i : x ↝ y} → f ≈ h → g ≈ i →
               f ∘ g ≈ h ∘ i

_[_,_] : (C : 1Groupoid) → 1Groupoid.set C → 1Groupoid.set C → Set
_[_,_] = 1Groupoid._↝_

open 1Groupoid

_⊎G_ : 1Groupoid → 1Groupoid → 1Groupoid
A ⊎G B = record
  { set      = A.set ⊎ B.set
  ; _↝_      =  _⇛_
  ; _≈_      = λ {x} → mk≈ {x}
  ; id       = λ {x} → id⇛ {x}
  ; _∘_      = λ {x} → _∙G_ {x = x}
  ; _⁻¹      = λ {x} → inv {x = x}
  ; lneutr   = λ {x} → lid⇛ {x}
  ; rneutr   = λ {x} → rid⇛ {x}
  ; assoc    = λ {x} a b g → assoc∙ {x} a b g
  ; equiv    = λ {x} → equiv≈ {x}
  ; linv     = λ {x} → linv⇛ {x}
  ; rinv     = λ {x} → rinv⇛ {x}
  ; ∘-resp-≈ = λ {x} → resp {x} }
  where
    module A = 1Groupoid A
    module B = 1Groupoid B
    C : Set
    C = set A ⊎ set B

    _⇛_ : set A ⊎ set B → set A ⊎ set B → Set
    _⇛_ (inj₁ x) (inj₁ y) = A._↝_ x y
    _⇛_ (inj₁ _) (inj₂ _) = ⊥
    _⇛_ (inj₂ _) (inj₁ _) = ⊥
    _⇛_ (inj₂ x) (inj₂ y) = B._↝_ x y

    mk≈ : {x y : set A ⊎ set B} → x ⇛ y → x ⇛ y → Set
    mk≈ {inj₁ z} {inj₁ z'} a b = A._≈_ a b
    mk≈ {inj₁ x} {inj₂ y}  () ()
    mk≈ {inj₂ y} {inj₁ x}  () ()
    mk≈ {inj₂ y} {inj₂ y'} a b = B._≈_ a b

    id⇛ : {x : set A ⊎ set B} → x ⇛ x
    id⇛ {inj₁ _} = id A
    id⇛ {inj₂ _} = id B

    _∙G_ : {x y z : set A ⊎ set B} → y ⇛ z → x ⇛ y → x ⇛ z
    _∙G_ {inj₁ _} {inj₁ _} {inj₁ _} a b = A._∘_ a b
    _∙G_ {inj₁ _} {inj₁ _} {inj₂ _} () b
    _∙G_ {inj₁ x} {inj₂ y} a ()
    _∙G_ {inj₂ y} {inj₁ x} a ()
    _∙G_ {inj₂ y} {inj₂ y₁} {inj₁ x} () b
    _∙G_ {inj₂ _} {inj₂ _} {inj₂ _} a b = B._∘_ a b

    inv : {x y : set A ⊎ set B} → x ⇛ y → y ⇛ x
    inv {inj₁ _} {inj₁ _} a = A._⁻¹ a
    inv {inj₁ _} {inj₂ _} ()
    inv {inj₂ _} {inj₁ _} ()
    inv {inj₂ _} {inj₂ _} a = B._⁻¹ a

    lid⇛ : {x y : C} (α : x ⇛ y) → mk≈ {x} (_∙G_ {x} (id⇛ {y}) α) α
    lid⇛ {inj₁ _} {inj₁ _} a = A.lneutr a
    lid⇛ {inj₁ _} {inj₂ _} ()
    lid⇛ {inj₂ _} {inj₁ _} ()
    lid⇛ {inj₂ _} {inj₂ _} a = B.lneutr a

    rid⇛ : {x y : A.set ⊎ B.set} (α : x ⇛ y) → mk≈ {x} (_∙G_ {x} α (id⇛ {x})) α
    rid⇛ {inj₁ _} {inj₁ _} α = A.rneutr α
    rid⇛ {inj₁ _} {inj₂ _} ()
    rid⇛ {inj₂ _} {inj₁ _} ()
    rid⇛ {inj₂ _} {inj₂ _} α = B.rneutr α

    assoc∙ : {w x y z : C} (α : y ⇛ z) (β : x ⇛ y) (δ : w ⇛ x) →
           mk≈ {w} {z} (_∙G_ {w} (_∙G_ {x} α β) δ) (_∙G_ {w} α (_∙G_ {w} β δ))
    assoc∙ {inj₁ x} {inj₁ x₁} {inj₁ x₂} {inj₁ x₃} α β γ = A.assoc α β γ
    assoc∙ {inj₁ x} {inj₁ x₁} {inj₁ x₂} {inj₂ y} () _ _
    assoc∙ {inj₁ x} {inj₁ x₁} {inj₂ y} _ () _
    assoc∙ {inj₁ x} {inj₂ y} _ _ ()
    assoc∙ {inj₂ y} {inj₁ x} _ _ ()
    assoc∙ {inj₂ y} {inj₂ y₁} {inj₁ x} _ () _
    assoc∙ {inj₂ y} {inj₂ y₁} {inj₂ y₂} {inj₁ x} () _ _
    assoc∙ {inj₂ y} {inj₂ y₁} {inj₂ y₂} {inj₂ y₃}  α β γ = B.assoc α β γ

    linv⇛ : {x y : C} (α : x ⇛ y) → mk≈ {x} (_∙G_ {x} (inv {x} α) α) (id⇛ {x})
    linv⇛ {inj₁ _} {inj₁ _} α = A.linv α
    linv⇛ {inj₁ x} {inj₂ y} ()
    linv⇛ {inj₂ y} {inj₁ x} ()
    linv⇛ {inj₂ _} {inj₂ _} α = B.linv α

    rinv⇛ : {x y : C} (α : x ⇛ y) → mk≈ {y} (_∙G_ {y} α (inv {x} α)) (id⇛ {y})
    rinv⇛ {inj₁ _} {inj₁ _} α = A.rinv α
    rinv⇛ {inj₁ x} {inj₂ y} ()
    rinv⇛ {inj₂ y} {inj₁ x} ()
    rinv⇛ {inj₂ _} {inj₂ _} α = B.rinv α

    refl≈ : {x y : C} → Reflexive (mk≈ {x} {y})
    refl≈ {inj₁ _} {inj₁ _} = IsEquivalence.refl A.equiv
    refl≈ {inj₁ _} {inj₂ _} {()}
    refl≈ {inj₂ _} {inj₁ _} {()}
    refl≈ {inj₂ y} {inj₂ y₁} = IsEquivalence.refl B.equiv

    sym≈ : {x y : C} → Symmetric (mk≈ {x} {y})
    sym≈ {inj₁ _} {inj₁ _} = IsEquivalence.sym A.equiv
    sym≈ {inj₁ _} {inj₂ _} {()}
    sym≈ {inj₂ _} {inj₁ _} {()}
    sym≈ {inj₂ y} {inj₂ y₁} = IsEquivalence.sym B.equiv

    trans≈ : {x y : C} → Transitive (mk≈ {x} {y})
    trans≈ {inj₁ _} {inj₁ _} = IsEquivalence.trans A.equiv
    trans≈ {inj₁ _} {inj₂ _} {()}
    trans≈ {inj₂ _} {inj₁ _} {()}
    trans≈ {inj₂ _} {inj₂ _} = IsEquivalence.trans B.equiv

    equiv≈ : {x y : C} → IsEquivalence (mk≈ {x} {y})
    equiv≈ {x} =
      record { refl = refl≈ {x}; sym = sym≈ {x}; trans = trans≈ {x} }

    resp : {x y z : C} {f h : y ⇛ z} {g i : x ⇛ y} →
           mk≈ {y} f h → mk≈ {x} g i → mk≈ {x} (_∙G_ {x} f g) (_∙G_ {x} h i)
    resp {inj₁ _} {inj₁ _} {inj₁ _} = A.∘-resp-≈
    resp {inj₁ _} {inj₁ _} {inj₂ _} {()}
    resp {inj₁ _} {inj₂ _} {_} {_} {_} {()}
    resp {inj₂ _} {inj₁ _} {_} {_} {_} {()}
    resp {inj₂ _} {inj₂ _} {inj₁ _} {()}
    resp {inj₂ _} {inj₂ _} {inj₂ _} = B.∘-resp-≈

_×G_ : 1Groupoid → 1Groupoid → 1Groupoid
A ×G B = record
  { set      = A.set × B.set
  ; _↝_      =  liftG A._↝_ B._↝_
  ; _≈_      = liftG A._≈_ B._≈_
  ; id       = A.id , B.id
  ; _∘_      = liftOp2 {Z₁ = A._↝_} {B._↝_} A._∘_ B._∘_
  ; _⁻¹      = λ x₁ → A._⁻¹ (proj₁ x₁) , B._⁻¹ (proj₂ x₁)
  ; lneutr   = λ α → A.lneutr (proj₁ α) , B.lneutr (proj₂ α)
  ; rneutr   = λ α → A.rneutr (proj₁ α) , B.rneutr (proj₂ α)
  ; assoc    = λ α β δ →
                 A.assoc (proj₁ α) (proj₁ β) (proj₁ δ) ,
                 B.assoc (proj₂ α) (proj₂ β) (proj₂ δ)
  ; equiv    = λ {x} {y} →
                 let module W = IsEquivalence (A.equiv {proj₁ x} {proj₁ y})
                     module Z = IsEquivalence (B.equiv {proj₂ x} {proj₂ y}) in
                 record { refl = W.refl , Z.refl
                        ; sym = λ i≈j → W.sym (proj₁ i≈j) , Z.sym (proj₂ i≈j)
                        ; trans = λ i≈j j≈k →
                                    (W.trans (proj₁ i≈j) (proj₁ j≈k)) ,
                                    ((Z.trans (proj₂ i≈j) (proj₂ j≈k))) }
  ; linv     = λ α → A.linv (proj₁ α) , B.linv (proj₂ α)
  ; rinv     = λ α → A.rinv (proj₁ α) , B.rinv (proj₂ α)
  ; ∘-resp-≈ = λ x₁ x₂ →
                 (A.∘-resp-≈ (proj₁ x₁) (proj₁ x₂)) ,
                  B.∘-resp-≈ (proj₂ x₁) (proj₂ x₂) }
  where
    module A = 1Groupoid A
    module B = 1Groupoid B
    C : Set
    C = A.set × B.set

    liftG : {X Y : Set} → Rel0 X → Rel0 Y → X × Y → X × Y → Set
    liftG F G =  λ x y → F (proj₁ x) (proj₁ y) × G (proj₂ x) (proj₂ y)

    liftOp2 : {A₁ A₂ : Set} {x y z : A₁ × A₂} {Z₁ : Rel0 A₁} {Z₂ : Rel0 A₂} →
             let _⇛_ = liftG Z₁ Z₂ in
             let _↝₁_ : (a b : A₁ × A₂) → Set
                 _↝₁_ = λ a b → Z₁ (proj₁ a) (proj₁ b)
                 _↝₂_ : (a b : A₁ × A₂) → Set
                 _↝₂_ = λ a b → Z₂ (proj₂ a) (proj₂ b) in
                   (y ↝₁ z → x ↝₁ y → x ↝₁ z) → (y ↝₂ z → x ↝₂ y → x ↝₂ z)
                → y ⇛ z → x ⇛ y → x ⇛ z
    liftOp2 F G = λ x y → F (proj₁ x) (proj₁ y) , G (proj₂ x) (proj₂ y)

-- Discrete paths.  Essentially ≡.

data DPath {A : Set} (x : A) : A → Set where
  reflD : DPath x x

transD : {A : Set} {x y z : A} → DPath y z → DPath x y → DPath x z
transD reflD reflD = reflD

symD : {A : Set} {x y : A} → DPath x y → DPath y x
symD reflD = reflD

lidD : {A : Set} {x y : A} (α : DPath x y) → DPath (transD reflD α) α
lidD reflD = reflD

ridD : {A : Set} {x y : A} (α : DPath x y) → DPath (transD α reflD) α
ridD reflD = reflD

assocD : {A : Set} {w x y z : A}
         (α : DPath y z) (β : DPath x y) (δ : DPath w x) →
         DPath (transD (transD α β) δ) (transD α (transD β δ))
assocD reflD reflD reflD = reflD

linvD : {A : Set} {x y : A} (α : DPath x y) → DPath (transD (symD α) α) reflD
linvD reflD = reflD

rinvD : {A : Set} {x y : A} (α : DPath x y) → DPath (transD α (symD α)) reflD
rinvD reflD = reflD

equivD : {A : Set} {x y : A} → IsEquivalence {_} {_} {DPath x y} DPath
equivD = λ {A} {x} {y} → record
  { refl = reflD
  ; sym = symD
  ; trans = flip transD }

respD : {A : Set} {x y z : A} {f h : DPath y z} {g i : DPath x y} →
        DPath f h → DPath g i → DPath (transD f g) (transD h i)
respD reflD reflD = reflD

discrete : Set → 1Groupoid
discrete a =  record
    { set       = a
    ; _↝_       = DPath
    ; _≈_       = DPath -- or could use _≡_ .
    ; id        = reflD
    ; _∘_       = transD
    ; _⁻¹       = symD
    ; lneutr    = lidD
    ; rneutr    = ridD
    ; assoc     = assocD
    ; linv      = linvD
    ; rinv      = rinvD
    ; equiv     = equivD
    ;  ∘-resp-≈ = respD }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Instance.Discrete where

-- Discrete Functor
--   from Sets to Cats. This works, unlike in the previous version of the library,
--   because the equality in Cats is properly NaturalIsomorphism instead of something stricter,
--   no need for that pesky Heterogeneous anything.

open import Categories.Category
open import Categories.Functor
open import Categories.Category.Instance.Sets
open import Categories.Category.Instance.Cats
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism
import Categories.Category.Discrete as D

import Relation.Binary.PropositionalEquality as ≡
open import Function renaming (id to idf; _∘_ to _●_)

Discrete : ∀ {o} → Functor (Sets o) (Cats o o o)
Discrete {o} = record
   { F₀ = D.Discrete
   ; F₁ = DiscreteFunctor
   ; identity = DiscreteId
   ; homomorphism = PointwiseHom
   ; F-resp-≈ = ExtensionalityNI
   }
   where
     DiscreteFunctor : {A B : Set o} → (A → B) → Cats o o o [ D.Discrete A , D.Discrete B ]
     DiscreteFunctor f = record
       { F₀ = f
       ; F₁ = ≡.cong f
       ; identity = ≡.refl
       ; homomorphism = λ { {_} {_} {_} {≡.refl} {≡.refl} → ≡.refl}
       ; F-resp-≈ = λ g≡h → ≡.cong (≡.cong f) g≡h -- marvel at the weirdness involved
       }
     DiscreteId : {A : Set o} → NaturalIsomorphism (DiscreteFunctor {A} idf) id
     DiscreteId = record
       { F⇒G = record { η = λ X → ≡.refl ; commute = λ { ≡.refl → ≡.refl } ; sym-commute = λ { ≡.refl → ≡.refl} }
       ; F⇐G = record { η = λ _ → ≡.refl ; commute = λ { ≡.refl → ≡.refl } ; sym-commute = λ { ≡.refl → ≡.refl} }
       ; iso = λ X → record { isoˡ = ≡.refl ; isoʳ = ≡.refl }
       }
     PointwiseHom : {X Y Z : Set o} {g : X → Y} {h : Y → Z} →
       NaturalIsomorphism (DiscreteFunctor (h ● g)) (DiscreteFunctor h ∘F DiscreteFunctor g)
     PointwiseHom = record
       { F⇒G = record { η = λ _ → ≡.refl ; commute = λ { ≡.refl → ≡.refl} ; sym-commute = λ { ≡.refl → ≡.refl} }
       ; F⇐G = record { η = λ _ → ≡.refl ; commute = λ { ≡.refl → ≡.refl} ; sym-commute = λ { ≡.refl → ≡.refl} }
       ; iso = λ X → record { isoˡ = ≡.refl ; isoʳ = ≡.refl }
       }
     ExtensionalityNI : {A B : Set o} {g h : A → B} →
      ({x : A} → g x ≡.≡ h x) → NaturalIsomorphism (DiscreteFunctor g) (DiscreteFunctor h)
     ExtensionalityNI g≡h = record
       { F⇒G = ntHelper record { η = λ X → g≡h {X} ; commute = λ { ≡.refl → ≡.sym (≡.trans-reflʳ g≡h)} }
       ; F⇐G = ntHelper record { η = λ X → ≡.sym (g≡h {X}) ; commute = λ { ≡.refl → ≡.sym (≡.trans-reflʳ _)} }
       ; iso = λ X → record { isoˡ = ≡.trans-symʳ g≡h ; isoʳ = ≡.trans-symˡ g≡h }
       }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
-- Andreas, 2018-06-14, issue #2513, surviving shape-irrelevance annotations.

data Wrap (A : Set) : Set where
  @shape-irrelevant wrap : A → Wrap A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Lec2 where

data Zero : Set where

{-
cannaeMake : Zero
cannaeMake = cannaeMake
-}

magic : {X : Set} -> Zero -> X
magic ()

record One : Set where
  constructor <>

tryit : One
tryit = <>

tryit2 : One
tryit2 = record {}

data List (X : Set) : Set where
  [] : List X
  _::_ : X -> List X -> List X

NonEmpty : {X : Set} -> List X -> Set
NonEmpty [] = Zero
NonEmpty (x :: xs) = One

head : {X : Set} -> (xs : List X) -> NonEmpty xs -> X
head [] ()
head (x :: xs) _ = x

{-
examples : List Zero
examples = {!-l!}

examples2 : List One
examples2 = {!-l!}
-}

data Two : Set where
  tt : Two
  ff : Two

if_then_else_ : {X : Set} -> Two -> X -> X -> X
if b then t else e = e
-- if ff then t else e = t

caseTwo : {P : Two -> Set} -> P tt -> P ff -> (b : Two) -> P b
caseTwo pt pf tt = pt
caseTwo pt pf ff = pf

not : Two -> Two
not tt = ff
not ff = tt

xor : Two -> Two -> Two
xor x y with not y
xor tt y | tt = tt
xor ff y | tt = ff
xor tt y | ff = ff
xor ff y | ff = tt


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.DirectSum.DirectSumHIT.UniversalProperty where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.DirectSumHIT
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base

private variable
  ℓ ℓ' ℓ'' : Level

open AbGroupStr
open IsGroupHom

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

module _
  (Idx              : Type ℓ)
  (G                : (k : Idx) → Type ℓ')
  (Gstr             : (k : Idx) → AbGroupStr (G k))
  (HAbGr@(H , Hstr) : AbGroup ℓ'')
  (fHhom            : (k : Idx) → AbGroupHom ((G k) , (Gstr k)) HAbGr)
  where

  private
    fH : (k : Idx) → G k → H
    fH = λ k → fst (fHhom k)
    fHstr : (k : Idx) → _
    fHstr = λ k → snd (fHhom k)

  injₖ : (k : Idx) → G k → ⊕HIT Idx G Gstr
  injₖ k a = base k a

  injₖ-hom : (k : Idx) → AbGroupHom ((G k) , (Gstr k)) (⊕HIT-AbGr Idx G Gstr)
  injₖ-hom k = injₖ k , (makeIsGroupHom λ a b → sym (base-add _ _ _) )

  -- universalProperty :
  ⊕HIT→H : ⊕HIT Idx G Gstr → H
  ⊕HIT→H = DS-Rec-Set.f _ _ _ _ (is-set Hstr)
            (0g Hstr)
            (λ k a → fH k a)
            (Hstr ._+_)
            (+Assoc Hstr)
            (+IdR Hstr)
            (+Comm Hstr)
            (λ k → pres1 (fHstr k))
            λ k a b → sym (pres· (fHstr k) _ _)

  ⊕HIT→H-hom : AbGroupHom (⊕HIT-AbGr Idx G Gstr) HAbGr
  ⊕HIT→H-hom = ⊕HIT→H , (makeIsGroupHom (λ _ _ → refl))

  -- Universal Property
  up∃⊕HIT : (k : Idx) → fHhom k ≡ compGroupHom (injₖ-hom k) ⊕HIT→H-hom
  up∃⊕HIT k = ΣPathTransport→PathΣ _ _
             ((funExt (λ _ → refl))
             , isPropIsGroupHom _ _ _ _)

  upUnicity⊕HIT : (hhom : AbGroupHom (⊕HIT-AbGr Idx G Gstr) HAbGr) →
                  (eqInj : (k : Idx) → fHhom k ≡ compGroupHom (injₖ-hom k) hhom)
                  → hhom ≡ ⊕HIT→H-hom
  upUnicity⊕HIT (h , hstr) eqInj = ΣPathTransport→PathΣ _ _
                             (helper , isPropIsGroupHom _ _ _ _)
    where

    helper : _
    helper = funExt (DS-Ind-Prop.f _ _ _ _ (λ _ → is-set Hstr _ _)
                    (pres1 hstr)
                    (λ k a → sym (funExt⁻ (cong fst (eqInj k)) a))
                    λ {U V} ind-U ind-V → pres· hstr _ _ ∙ cong₂ (_+_ Hstr) ind-U ind-V)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Nat where

open import Eq

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

infixl 6 _+_
infixl 7 _×_

_+_ : ℕ → ℕ → ℕ
Z + n     = n
(S k) + n = S(k + n)

{-# BUILTIN NATPLUS _+_ #-}

_×_ : ℕ → ℕ → ℕ
Z  × n = Z
S m × n = n + m × n

{-# BUILTIN NATTIMES _×_ #-}

*-right-zero : ∀ (n : ℕ) → n × Z ≡ Z
*-right-zero Z = Refl
*-right-zero (S n) = *-right-zero n

testEq : (x : ℕ) → (y : ℕ) → (p : x ≡ y) → ℕ
testEq x _ Refl = x

max_stars_repo_name: mjhopkins/PowerOfPi

max_issues_repo_name: mjhopkins/PowerOfPi

max_forks_repo_name: mjhopkins/PowerOfPi


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Monoid.Instances.NatVec where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ ; isSetℕ)
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat

open import Cubical.Algebra.Monoid

NatVecMonoid : (n : ℕ) → Monoid ℓ-zero
fst (NatVecMonoid n) = Vec ℕ n
MonoidStr.ε (snd (NatVecMonoid n)) = replicate 0
MonoidStr._·_ (snd (NatVecMonoid n)) = _+n-vec_
MonoidStr.isMonoid (snd (NatVecMonoid n)) = makeIsMonoid (VecPath.isOfHLevelVec 0 n isSetℕ)
                                                       +n-vec-assoc +n-vec-rid +n-vec-lid


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Coproduct

open import Graphs.Definition

open import Coequalizers.Definition

module Coequalizers.TrivialExtension where

module TExtensionCoeq-l {i : ULevel} {V : Type i} (v : V) where
  instance
    tegph : Graph ⊤ (V ⊔ ⊤)
    tegph = record { π₀ = λ _ → inl v ; π₁ = λ _ → inr unit }

  extn-equiv : V ≃ ((V ⊔ ⊤) / ⊤)
  extn-equiv = equiv ((c[_] ∘ inl)) (((Coeq-rec (⊔-rec (idf V) (λ _ → v)) λ e → idp))) ((Coeq-elim _ (λ { (inl v') → idp ; (inr x) → quot x}) λ {unit → ↓-app=idf-in (∙'-unit-l _ ∙ ! lem ∙ᵣ quot unit)}))
                      λ _ → idp
    where
      lem : ap (c[_] ∘ inl ∘ (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp ))) (quot unit) == idp
      lem =
        ap (c[_] ∘ inl ∘ (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp ))) (quot unit)
          =⟨ ap-∘ (c[_] ∘ inl) (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp )) (quot unit) ⟩
        ap (c[_] ∘ inl) (ap (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp )) (quot unit))
          =⟨ ap (ap (c[_] ∘ inl)) (Coeq-rec-β= _ _ _) ⟩
        ap (c[_] ∘ inl)  idp
          =⟨ idp ⟩
        idp
          =∎

module TExtensionCoeq-r {i : ULevel} {V : Type i} (v : V) where
  instance
    tegph : Graph ⊤ (V ⊔ ⊤)
    tegph = record { π₀ = λ _ → inr unit ; π₁ = λ _ → inl v }

  extn-equiv : V ≃ ((V ⊔ ⊤) / ⊤)
  extn-equiv = equiv ((c[_] ∘ inl)) (((Coeq-rec (⊔-rec (idf V) (λ _ → v)) λ e → idp))) ((Coeq-elim _ (λ { (inl v') → idp ; (inr x) → ! (quot x)}) λ {unit → ↓-app=idf-in ((!-inv'-l (quot unit) ∙ ! lem ∙ ! (∙-unit-r _)))}))
                      λ _ → idp
    where
      lem : ap (c[_] ∘ inl ∘ (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp ))) (quot unit) == idp
      lem =
        ap (c[_] ∘ inl ∘ (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp ))) (quot unit)
          =⟨ ap-∘ (c[_] ∘ inl) (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp )) (quot unit) ⟩
        ap (c[_] ∘ inl) (ap (Coeq-rec (⊔-rec (λ x → x) (λ _ → v)) (λ e → idp )) (quot unit))
          =⟨ ap (ap (c[_] ∘ inl)) (Coeq-rec-β= _ _ _) ⟩
        ap (c[_] ∘ inl)  idp
          =⟨ idp ⟩
        idp
          =∎

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


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

module Categories.Category.Instance.Properties.Setoids.Exact where

open import Categories.Category using (Category)
open import Categories.Category.Exact using (Exact)
open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical using (pullback; FiberProduct; mk-×; FP-≈)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
open import Categories.Category.Regular using (Regular)
open import Categories.Diagram.Coequalizer using (Coequalizer; IsCoequalizer; Coequalizer⇒Epi)
open import Categories.Diagram.Coequalizer.Properties
open import Categories.Diagram.KernelPair using (KernelPair)
open import Categories.Diagram.Pullback using (Pullback; up-to-iso)
open import Categories.Diagram.Pullback.Properties
open import Categories.Morphism using (_≅_; Epi)
open import Categories.Morphism.Regular using (RegularEpi)
open import Categories.Object.InternalRelation using (Equivalence; EqSpan; KP⇒Relation; KP⇒EqSpan; KP⇒Equivalence; module Relation; rel)

open import Data.Bool.Base using (Bool; true; false; T)
open import Data.Empty.Polymorphic using (⊥)
open import Data.Fin using (Fin; zero) renaming (suc to nzero)
open import Data.Product using (∃; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_; map; zip; swap; map₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit.Polymorphic.Base using (⊤; tt)
open import Function using (flip) renaming (id to id→; _∘′_ to _∘→_)
open import Function.Equality as SΠ using (Π; _⇨_) renaming (id to ⟶-id; _∘_ to _∘⟶_)
open import Function.Definitions using (Surjective)
open import Level
open import Relation.Binary using (Setoid; Rel; IsEquivalence)
import Relation.Binary.Reasoning.Setoid as SR

open import Categories.Category.Instance.SingletonSet

open Setoid renaming (_≈_ to [_][_≈_]; Carrier to ∣_∣) using (isEquivalence; refl; sym; trans)
open Π using (_⟨$⟩_; cong)

module _ ℓ where
  private
    S = Setoids ℓ ℓ
    open Category S hiding (_≈_)
    module S = Category S

  open Pullback using (P; p₁; p₂)

  -- the next bits all depend on a Setoid X and an Equivalence E, factor those out
  module _ {X : Setoid ℓ ℓ} (E : Equivalence S X) where
    -- let some things have short names
    open Equivalence E using (R; module R; eqspan)
    module ES = EqSpan eqspan

    private
      module X = Setoid X using (refl; sym; trans; _≈_)
    -- convenient inline versions
    infix 2 ⟺
    infixr 3 _○_
    ⟺ : {x₁ x₂ : ∣ X ∣} → x₁ X.≈ x₂ → x₂ X.≈ x₁
    ⟺ = Setoid.sym X
    _○_ : {x₁ x₂ x₃ : ∣ X ∣} → x₁ X.≈ x₂ → x₂ X.≈ x₃ → x₁ X.≈ x₃
    _○_ = Setoid.trans X

    record Equation (x₁ x₂ : ∣ X ∣) : Set ℓ where
      constructor eqn
      open Setoid X using (_≈_)
      field
        name : ∣ R.dom ∣
        x₁≈  : R.p₁ ⟨$⟩ name ≈ x₁
        ≈x₂  : R.p₂ ⟨$⟩ name ≈ x₂

    open Equation

    -- is re-used below, so make it easier to do so by exposing directly
    quotient-trans : {x₁ x₂ y₁ y₂ : ∣ X ∣} →
      (p : Equation x₁ y₁) → (q : Equation x₂ y₂) →
      [ X ][ x₁ ≈ x₂ ] → [ X ][ y₁ ≈ y₂ ] → [ R.dom ][ name p ≈ name q ]

    quotient-trans {x₁} {x₂} {y₁} {y₂} (eqn eq x₁≈ ≈y₁) (eqn eq′ x₂≈ ≈y₂) x₁≈x₂ y₁≈y₂ =
      R.relation {SingletonSetoid}
      (record { _⟨$⟩_ = λ _ → eq  ; cong = λ _ → refl R.dom})
      (record { _⟨$⟩_ = λ _ → eq′ ; cong = λ _ → refl R.dom})
      (λ { zero      _ → x₁≈ ○ x₁≈x₂ ○ ⟺ x₂≈
         ; (nzero _) _ → ≈y₁ ○ y₁≈y₂ ○ ⟺ ≈y₂}) tt

    Quotient-Equivalence : IsEquivalence Equation
    Quotient-Equivalence = record
        {
          refl  = eqn _ (ES.is-refl₁ X.refl) (ES.is-refl₂ X.refl)
        ; sym   = λ { (eqn r eq₁ eq₂) → eqn (ES.sym ⟨$⟩ r) (ES.is-sym₁ D.refl ○ eq₂) (ES.is-sym₂ D.refl ○ eq₁) }
        ; trans = λ { (eqn r x≈ ≈y) (eqn s y≈ ≈z) →
           let t = record { elem₁ = _ ; elem₂ = _ ; commute = y≈ ○ ⟺ ≈y } in
             eqn
               (ES.trans ∘⟶ P₀⇒P₁ ⟨$⟩ t)
               (ES.is-trans₁ R×R.refl ○ (cong R.p₁ (p₂-≈ {t} {t} (D.refl , D.refl)) ○ x≈))
               (ES.is-trans₂ R×R.refl ○ (cong R.p₂ (p₁-≈ {t} {t} (D.refl , D.refl)) ○ ≈z))
           }
        }
          where
            module D = Setoid R.dom         using (refl)
            module R×R = Setoid ES.R×R.dom  using (refl)

            fp : Pullback S R.p₁ R.p₂
            fp = pullback ℓ ℓ R.p₁ R.p₂
            open IsoPb S fp ES.R×R using (P₀⇒P₁; p₁-≈; p₂-≈)

    Quotient-Setoid : Setoid ℓ ℓ
    Quotient-Setoid = record { Carrier = ∣ X ∣ ; _≈_ = Equation; isEquivalence = Quotient-Equivalence }

    Quotient-Coequalizer : Coequalizer S (Equivalence.R.p₁ E) (Equivalence.R.p₂ E)
    Quotient-Coequalizer = record
      { obj = X∼
      ; arr = inj
      ; isCoequalizer = record
         { equality   = inj-≈
         ; coequalize = λ {_}{h} → quotient h
         ; universal  = λ {_}{h} → cong h
         ; unique     = λ {_}{h}{i}{eq′} → unique {_}{h}{i}{eq′}
         }
      }
      where
        X∼ : Setoid ℓ ℓ
        X∼ = Quotient-Setoid

        inj : X ⇒ X∼
        inj = record
         { _⟨$⟩_ = id→
         ; cong = λ {x₁} eq → eqn (ES.refl ⟨$⟩ x₁) (ES.is-refl₁ X.refl) (ES.is-refl₂ X.refl ○ eq)
         }

        inj-≈ : inj ∘ R.p₁ S.≈ inj ∘ R.p₂
        inj-≈ {x} x≈y = eqn x X.refl (cong R.p₂ x≈y)

        -- coEqualizer wants the 'h' to be implicit, but can't figure it out, so make it explicit here
        quotient : {C : Obj} (h : X ⇒ C) → h ∘ R.p₁ S.≈ h ∘ R.p₂ → X∼ ⇒ C
        quotient {C} h eq = record
          { _⟨$⟩_ = h ⟨$⟩_
          ; cong = λ { (eqn r x≈ ≈y) → trans C (cong h (X.sym x≈)) (trans C (eq (refl R.dom)) (cong h ≈y))}
          }

        unique : {C : Obj} {h : X ⇒ C} {i : X∼ ⇒ C} {eq : h ∘ R.p₁ S.≈ h ∘ R.p₂} → h S.≈ i ∘ inj → i S.≈ quotient h eq
        unique {C} {h} {i} {eq′} eq {x} {y} (eqn r x≈ ≈y) = begin
          i ⟨$⟩ x           ≈˘⟨ eq X.refl ⟩
          h ⟨$⟩ x           ≈˘⟨ cong h x≈ ⟩
          h ⟨$⟩ (R.p₁ ⟨$⟩ r) ≈⟨ eq′ (refl R.dom) ⟩
          h ⟨$⟩ (R.p₂ ⟨$⟩ r) ≈⟨ cong h ≈y ⟩
          h ⟨$⟩ y ∎
          where open SR C

  -- Setoid Surjectivity
  SSurj : {A B : Setoid ℓ ℓ} (f : A ⇒ B) → Set ℓ
  SSurj {A} {B} f = Surjective (Setoid._≈_ A) (Setoid._≈_ B) (f ⟨$⟩_)

  -- Proposition 1 from "Olov Wilander, Setoids and universes"
  Epi⇒Surjective : ∀ {A B : Setoid ℓ ℓ} (f : A ⇒ B) → Epi S f → SSurj f
  Epi⇒Surjective {A}{B} f epi y = g≈h (refl B {y}) .proj₁ (λ ()) _

    where
      infix 3 _↔_

      _↔_ : Set ℓ → Set ℓ → Set ℓ
      A ↔ B = (A → B) × (B → A)

      B′ : Setoid ℓ ℓ
      B′ = record
        { Carrier =  Bool × ∣ B ∣
        ; _≈_ = λ { (a , x)  (b , y) → ((T a → Σ[ z ∈ ∣ A ∣ ] [ B ][ f ⟨$⟩ z ≈ x ]) ↔ (T b → Σ[ z ∈ ∣ A ∣ ] [ B ][ f ⟨$⟩ z ≈ y ])) }
        ; isEquivalence = record
            { refl  = id→ , id→
            ; sym   = swap
            ; trans = zip (flip _∘→_) _∘→_
            }
        }

      g : B ⇒ B′
      g = record { _⟨$⟩_ = λ x → false , x ; cong = λ _ → (λ _ ()) , (λ _ ()) }

      h : B ⇒ B′
      h = record
          { _⟨$⟩_ = true ,_
          ; cong = λ x≈y →
                (λ eq _ → map₂ (λ z → trans B z x≈y) (eq _))
              , (λ eq _ → let (a , eq′) = eq _ in a , (trans B eq′ (sym B x≈y)))
          }

      g≈h : [ B ⇨ B′ ][ g ≈ h ]
      g≈h = epi g h λ {x}{y} x≈y → (λ u _ → x , cong f x≈y) , λ _ ()

  -- not needed for exactness, but worthwhile
  Surjective⇒RegularEpi : ∀ {A B : Setoid ℓ ℓ} (f : A ⇒ B) → ((y : ∣ B ∣) → Σ[ x ∈ ∣ A ∣ ] [ B ][ f ⟨$⟩ x ≈ y ]) → RegularEpi S f
  Surjective⇒RegularEpi {A}{B} f surj = record
    { h = p₁ kp
    ; g = p₂ kp
    ; coequalizer = record
        { equality   = λ {x} {y} → commute kp {x} {y}
        ; coequalize = λ {_} {h} → Coeq.coeq {h = h}
        ; universal = λ {C} {h} {eq} → Coeq.universal′ {C} {h} (λ {x} {y} → eq {x} {y})
        ; unique = λ {_}{h}{i}{eq} h≈i∘f x≈y → Coeq.unique″ {_} {h} (λ {x} {y} → eq {x} {y}) {i} h≈i∘f x≈y
        }
    }
    where
      kp = pullback ℓ ℓ f f
      open Pullback
      module Coeq {C : S.Obj} {h : A S.⇒ C} where
        open SR C
        f⁻¹∘h : ∣ B ∣ → ∣ C ∣
        f⁻¹∘h b = h ⟨$⟩ proj₁ (surj b)
        module _ (h∘p₁≈h∘p₂ : h S.∘ p₁ kp S.≈ h S.∘ p₂ kp) where
          cong′ : {i j : ∣ B ∣} → [ B ][ i ≈ j ] → [ C ][ h ⟨$⟩ proj₁ (surj i) ≈ h ⟨$⟩ proj₁ (surj j) ]
          cong′ {y₁}{y₂} y₁≈y₂ = h∘p₁≈h∘p₂ {pt₁} {pt₁} (refl A , refl A)
            where
              x₁ x₂ : ∣ A ∣
              x₁ = surj y₁ .proj₁
              x₂ = surj y₂ .proj₁
              eq₁ : [ B ][ f ⟨$⟩ x₁ ≈ y₁ ]
              eq₁ = surj y₁ .proj₂
              eq₂ : [ B ][ f ⟨$⟩ x₂ ≈ y₂ ]
              eq₂ = surj y₂ .proj₂
              pt₁ : FiberProduct f f
              pt₁ = mk-× x₁ x₂ (trans B eq₁ (trans B y₁≈y₂ (sym B eq₂)))
          coeq : B S.⇒ C
          coeq = record { _⟨$⟩_ = f⁻¹∘h ; cong = cong′ }
          universal′ : h S.≈ coeq S.∘ f
          universal′ {x} {y} x≈y = begin
            h ⟨$⟩ x                     ≈⟨ cong h x≈y ⟩
            h ⟨$⟩ y                     ≈⟨ h∘p₁≈h∘p₂ {mk-× y x₁ (sym B eq₁)} {mk-× x x₁ (trans B (cong f x≈y) (sym B eq₁))} (sym A x≈y , refl A) ⟩
            h ⟨$⟩ proj₁ (surj (f ⟨$⟩ y)) ≡⟨⟩ -- by definition of f⁻¹∘h
            f⁻¹∘h (f ⟨$⟩ y)             ≡⟨⟩ -- by definition of coeq
            coeq S.∘ f ⟨$⟩ y            ∎
            where
              x₁ : ∣ A ∣
              x₁ = surj (f ⟨$⟩ y) .proj₁
              eq₁ : [ B ][ f ⟨$⟩ x₁ ≈ f ⟨$⟩ y ]
              eq₁ = surj (f ⟨$⟩ y) .proj₂
          unique″ : {i : B S.⇒ C} → h S.≈ i S.∘ f → i S.≈ coeq
          unique″ {i} h≈i∘f {x} {y} x≈y = begin
            i ⟨$⟩ x              ≈⟨ cong i x≈y ⟩
            i ⟨$⟩ y              ≈⟨ cong i (sym B eq₁) ⟩
            i ∘ f ⟨$⟩ x₁         ≈⟨ sym C (h≈i∘f (refl A)) ⟩
            h ⟨$⟩ x₁             ≡⟨⟩ -- by definition of f⁻¹∘h
            f⁻¹∘h y             ∎
            where
              x₁ : ∣ A ∣
              x₁ = surj y .proj₁
              eq₁ : [ B ][ f ⟨$⟩ x₁ ≈ y ]
              eq₁ = surj y .proj₂

  Setoids-Regular : Regular (Setoids ℓ ℓ)
  Setoids-Regular = record
    { finitely-complete = record
       { cartesian = Setoids-Cartesian
       ; equalizer = λ _ _ → pullback×cartesian⇒equalizer S (pullback ℓ ℓ) Setoids-Cartesian
       }
    ; coeq-of-kernelpairs = λ f kp → Quotient-Coequalizer record
       { R = KP⇒Relation S f kp
       ; eqspan = KP⇒EqSpan S f kp (pb kp)
       }
    ; pullback-of-regularepi-is-regularepi = pb-of-re-is-re
    }
    where
      pb : ∀ {A B} {f : A ⇒ B} (kp : KernelPair S f) → Pullback S (p₁ kp) (p₂ kp)
      pb kp = pullback ℓ ℓ (p₁ kp) (p₂ kp)

      pb-of-re-is-re : {A B D : Setoid ℓ ℓ} (f : B ⇒ A) {u : D ⇒ A} →
        RegularEpi S f → (pb : Pullback S f u) → RegularEpi S (p₂ pb)
      pb-of-re-is-re {A}{B}{D} f {u} record { C = C ; h = _ ; g = _ ; coequalizer = coeq } pb =
        Surjective⇒RegularEpi (p₂ pb) λ y →
          let (x , eq) = Epi⇒Surjective f (Coequalizer⇒Epi S record { arr = f ; isCoequalizer = coeq }) (u ⟨$⟩ y) in
          let pt = mk-× x y eq in
          P₀⇒P₁ ⟨$⟩ pt , p₂-≈ {pt} {pt} (refl B , refl D)
         where

           pb-fu : Pullback S f u
           pb-fu = pullback ℓ ℓ f u
           pb-ff : Pullback S f f
           pb-ff = pullback ℓ ℓ f f
           module B = Setoid B
           module C = Setoid C
           module D = Setoid D
           open IsoPb S pb-fu pb

  Setoids-Exact : Exact (Setoids ℓ ℓ)
  Setoids-Exact = record
    { regular   = Setoids-Regular
    ; quotient  = Quotient-Coequalizer
    ; effective = λ {X} E → record
        { commute   = λ eq → eqn _ (refl X) (cong (Relation.p₂ (R E)) eq)
        ; universal = λ { {Z}{h₁}{h₂} → universal E h₁ h₂ }
        ; unique    = λ {Z}{h₁}{h₂}{u}{eq} eq₁ eq₂ {x}{y} → Relation.relation (R E) u (universal E h₁ h₂ eq)
            λ { zero {x}{y} eq′      → trans X (eq₁ eq′) (sym X (p₁∘universal≈h₁ E h₁ h₂ eq (refl Z)))
              ; (nzero _) {x}{y} eq′ → trans X (eq₂ eq′) (sym X (p₂∘universal≈h₂ E h₁ h₂ eq (refl Z)))
              }
        ; p₁∘universal≈h₁ = λ {Z}{h₁}{h₂}{eq} → p₁∘universal≈h₁ E h₁ h₂ eq
        ; p₂∘universal≈h₂ = λ {Z}{h₁}{h₂}{eq} → p₂∘universal≈h₂ E h₁ h₂ eq
        }
    }
      where
        open Equivalence
        open Setoid
        open Coequalizer using (arr)

        universal : {X Z : Setoid ℓ ℓ} → (E : Equivalence S X) → (h₁ h₂ : Z ⇒ X) →
          (eq : [ Z ⇨ Quotient-Setoid E ][ arr (Quotient-Coequalizer E) ∘ h₁ ≈ arr (Quotient-Coequalizer E) ∘ h₂ ]) →
          Z ⇒ Relation.dom (R E)
        universal {X}{Z} E h₁ h₂ eq = record
          { _⟨$⟩_ = λ z → let (eqn eq _ _) = eq {z}{z} (refl Z) in eq
          ; cong = λ {z}{z′} z≈z′ → quotient-trans E (eq {z}{z} (refl Z)) (eq {z′}{z′} (refl Z)) (cong h₁ z≈z′) (cong h₂ z≈z′)
          }
        p₁∘universal≈h₁ : {X Z : Setoid ℓ ℓ} → (E : Equivalence S X) → (h₁ h₂ : Z ⇒ X) →
          (eq : [ Z ⇨ Quotient-Setoid E ][ arr (Quotient-Coequalizer E) ∘ h₁ ≈ arr (Quotient-Coequalizer E) ∘ h₂ ]) →
          [ Z ⇨ X ][ Relation.p₁ (R E) ∘ (universal E h₁ h₂ eq) ≈ h₁ ]
        p₁∘universal≈h₁ {X}{Z} _ h₁ h₂ eq x≈y = let (eqn _ p₁z≈ _) = eq (refl Z) in trans X p₁z≈ (cong h₁ x≈y)

        p₂∘universal≈h₂ : {X Z : Setoid ℓ ℓ} → (E : Equivalence S X) → (h₁ h₂ : Z ⇒ X) →
          (eq : [ Z ⇨ Quotient-Setoid E ][ arr (Quotient-Coequalizer E) ∘ h₁ ≈ arr (Quotient-Coequalizer E) ∘ h₂ ]) →
          [ Z ⇨ X ][ Relation.p₂ (R E) ∘ (universal E h₁ h₂ eq) ≈ h₂ ]
        p₂∘universal≈h₂ {X}{Z} _ h₁ h₂ eq x≈y = let (eqn _ _ p₂z≈) = eq (refl Z) in trans X p₂z≈ (cong h₂ x≈y)

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories