text:
open import Coinduction using ( ♭ ; ♯_ )
open import Data.Empty using ( ⊥-elim )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality
  using ( _≡_ ; _≢_ ; refl ; sym ; cong ; cong₂ )
open import Relation.Nullary using ( ¬_ ; Dec ; yes ; no )
open import System.IO.Transducers.Lazy
  using ( _⇒_ ; inp ; out ; done ; _⟫_ ;
     equiv ; assoc ; assoc⁻¹ ; unit₁ ; unit₁⁻¹ ; unit₂ ; unit₂⁻¹ ;
     _[&]_ ; ⟦_⟧ ; _≃_ )
open import System.IO.Transducers.Reflective using ( Reflective )
open import System.IO.Transducers.Strict using ( Strict )
open import System.IO.Transducers.Session
  using ( I ; Σ ; IsΣ ; _∼_ ; ∼-refl ; ∼-trans ; ∼-sym ; _&_ )
  renaming ( unit₁ to ∼-unit₁ ; unit₂ to ∼-unit₂ ; assoc to ∼-assoc )
open import System.IO.Transducers.Trace using ( Trace ; _✓ ; [] ; _∷_ )
open import System.IO.Transducers.Properties.Category
  using ( ⟦done⟧ ; done-semantics ; _⟦⟫⟧_ ; ⟫-semantics ; ⟫-≃-⟦⟫⟧ ; ⟫-resp-≃ ; done-isEquiv ; ⟫-isEquiv ; equiv-is-iso )
open import System.IO.Transducers.Properties.Lemmas
  using ( ≃-refl ; ≃-sym ; ✓-tl ; ✓? ; ⟦⟧-resp-✓ ; ⟦⟧-refl-✓ ; ⟦⟧-resp-[] ;
    IsEquiv ; isEquiv ; ≃-equiv ; I-η)

module System.IO.Transducers.Properties.Monoidal where

open Relation.Binary.PropositionalEquality.≡-Reasoning

infixr 8 _++_ _⟦[&]⟧_

-- Concatenation of traces

_++_ : ∀ {S T} → (Trace S) → (Trace T) → (Trace (S & T))
_++_ {I}     []        bs = bs
_++_ {Σ V F} []        bs = []
_++_ {Σ V F} (a ∷ as)  bs = a ∷ (as ++ bs)
_++_ {I}     (() ∷ as) bs

-- Projection of traces

front : ∀ {S T} → (Trace (S & T)) → (Trace S)
front {I}     as       = []
front {Σ V F} []       = []
front {Σ V F} (a ∷ as) = a ∷ front as

back : ∀ {S T} → (Trace (S & T)) → (Trace T)
back {I}     as       = as
back {Σ V F} []       = []
back {Σ V F} (a ∷ as) = back {♭ F a} as

-- Semantics of tensor

_⟦[&]⟧_ : ∀ {S T U V} →
  (f : Trace S → Trace T) → (g : Trace U → Trace V) →
    (Trace (S & U)) → (Trace (T & V))
_⟦[&]⟧_ {S} f g as = f (front as) ++ g (back {S} as)

[&]-semantics : ∀ {S T U V} (P : S ⇒ T) (Q : U ⇒ V) →
  ⟦ P [&] Q ⟧ ≃ ⟦ P ⟧ ⟦[&]⟧ ⟦ Q ⟧
[&]-semantics (inp {I} P) (inp Q) [] = refl
[&]-semantics (inp {I} P) (inp Q) (a ∷ as) = [&]-semantics (♭ P a) (inp Q) as
[&]-semantics (inp {I} P) done [] = refl
[&]-semantics (inp {I} P) done (a ∷ as) = [&]-semantics (♭ P a) done as
[&]-semantics (inp {Σ V F} P) Q [] = refl
[&]-semantics (inp {Σ V F} P) Q (a ∷ as) = [&]-semantics (♭ P a) Q as
[&]-semantics (out b P) Q as = cong (_∷_ b) ([&]-semantics P Q as)
[&]-semantics (done {I}) Q as = refl
[&]-semantics (done {Σ V F}) Q [] = refl
[&]-semantics (done {Σ V F}) Q (a ∷ as) = cong (_∷_ a) ([&]-semantics (done {♭ F a}) Q as)
[&]-semantics (inp {I} P) (out c Q) as =
  begin
    c ∷ ⟦ inp P [&] Q ⟧ as
  ≡⟨ cong (_∷_ c) ([&]-semantics (inp P) Q as) ⟩
    c ∷ (⟦ inp P ⟧ ⟦[&]⟧ ⟦ Q ⟧) as
  ≡⟨ cong (_∷_ c) (cong₂ _++_ (I-η (⟦ inp P ⟧ (front as))) refl) ⟩
    c ∷ ⟦ Q ⟧ _
  ≡⟨ cong₂ _++_ (sym (I-η (⟦ inp P ⟧ (front as)))) refl ⟩
    (⟦ inp P ⟧ ⟦[&]⟧ ⟦ out c Q ⟧) as
  ∎

[&]-≃-⟦[&]⟧ : ∀ {S T U V}
  {P : S ⇒ T} {f : Trace S → Trace T} {Q : U ⇒ V} {g : Trace U → Trace V} →
    (⟦ P ⟧ ≃ f) → (⟦ Q ⟧ ≃ g) → (⟦ P [&] Q ⟧ ≃ f ⟦[&]⟧ g)
[&]-≃-⟦[&]⟧ {S} {T} {U} {V} {P} {f} {Q} {g} P≃f Q≃g as =
  begin
    ⟦ P [&] Q ⟧ as
  ≡⟨ [&]-semantics P Q as ⟩
    (⟦ P ⟧ ⟦[&]⟧ ⟦ Q ⟧) as
  ≡⟨ cong₂ _++_ (P≃f (front as)) (Q≃g (back {S} as)) ⟩
    (f ⟦[&]⟧ g) as
  ∎

-- Semantics of units

⟦unit₁⟧ : ∀ {S} → (Trace (I & S)) → (Trace S)
⟦unit₁⟧ as = as

unit₁-semantics : ∀ {S} → ⟦ unit₁ {S} ⟧ ≃ ⟦unit₁⟧ {S}
unit₁-semantics {I}     as        = refl
unit₁-semantics {Σ V F} []        = refl
unit₁-semantics {Σ V F} (a ∷ as)  = cong (_∷_ a) (unit₁-semantics as)

⟦unit₁⁻¹⟧ : ∀ {S} → (Trace (I & S)) → (Trace S)
⟦unit₁⁻¹⟧ as = as

unit₁⁻¹-semantics : ∀ {S} → ⟦ unit₁⁻¹ {S} ⟧ ≃ ⟦unit₁⁻¹⟧ {S}
unit₁⁻¹-semantics {I}     as        = refl
unit₁⁻¹-semantics {Σ V F} []        = refl
unit₁⁻¹-semantics {Σ V F} (a ∷ as)  = cong (_∷_ a) (unit₁⁻¹-semantics as)

⟦unit₂⟧ : ∀ {S} → (Trace (S & I)) → (Trace S)
⟦unit₂⟧ = front

unit₂-semantics : ∀ {S} → ⟦ unit₂ {S} ⟧ ≃ ⟦unit₂⟧ {S}
unit₂-semantics {I}     []        = refl
unit₂-semantics {Σ V F} []        = refl
unit₂-semantics {Σ V F} (a ∷ as)  = cong (_∷_ a) (unit₂-semantics as)
unit₂-semantics {I}     (() ∷ as)

⟦unit₂⁻¹⟧ : ∀ {S} → (Trace S) → (Trace (S & I))
⟦unit₂⁻¹⟧ as = as ++ []

unit₂⁻¹-semantics : ∀ {S} → ⟦ unit₂⁻¹ {S} ⟧ ≃ ⟦unit₂⁻¹⟧
unit₂⁻¹-semantics {I}     []       = refl
unit₂⁻¹-semantics {Σ W F} []       = refl
unit₂⁻¹-semantics {Σ W F} (a ∷ as) = cong (_∷_ a) (unit₂⁻¹-semantics as)
unit₂⁻¹-semantics {I}     (() ∷ as)

-- Semantics of associativity

⟦assoc⟧ : ∀ {S T U} → (Trace (S & (T & U))) → (Trace ((S & T) & U))
⟦assoc⟧ {S} {T} {U} as =
  (front {S} as ++ front {T} (back {S} as)) ++ back {T} (back {S} as)

assoc-semantics : ∀ {S T U} → ⟦ assoc {S} {T} {U} ⟧ ≃ ⟦assoc⟧ {S} {T} {U}
assoc-semantics {I}     {I}     {I}     []        = refl
assoc-semantics {I}     {I}     {Σ X H} []        = refl
assoc-semantics {I}     {Σ W G}         []        = refl
assoc-semantics {I}     {I}     {Σ X H} (a ∷ as)  = cong (_∷_ a) (assoc-semantics {I} {I} as)
assoc-semantics {I}     {Σ W G}         (a ∷ as)  = cong (_∷_ a) (assoc-semantics {I} {♭ G a} as)
assoc-semantics {Σ V F}                 []        = refl
assoc-semantics {Σ V F}                 (a ∷ as)  = cong (_∷_ a) (assoc-semantics {♭ F a} as)
assoc-semantics {I}     {I}     {I}     (() ∷ as)

⟦assoc⁻¹⟧ : ∀ {S T U} → (Trace ((S & T) & U)) → (Trace (S & (T & U)))
⟦assoc⁻¹⟧ {S} {T} {U} as =
  front {S} (front {S & T} as) ++ back {S} (front {S & T} as) ++ back {S & T} as

assoc⁻¹-semantics : ∀ {S T U} → ⟦ assoc⁻¹ {S} {T} {U} ⟧ ≃ ⟦assoc⁻¹⟧ {S} {T} {U}
assoc⁻¹-semantics {I}     {I}     {I}     []        = refl
assoc⁻¹-semantics {I}     {I}     {Σ X H} []        = refl
assoc⁻¹-semantics {I}     {Σ W G}         []        = refl
assoc⁻¹-semantics {I}     {I}     {Σ X H} (a ∷ as)  = cong (_∷_ a) (assoc⁻¹-semantics {I} {I} as)
assoc⁻¹-semantics {I}     {Σ W G}         (a ∷ as)  = cong (_∷_ a) (assoc⁻¹-semantics {I} {♭ G a} as)
assoc⁻¹-semantics {Σ V F}                 []        = refl
assoc⁻¹-semantics {Σ V F}                 (a ∷ as)  = cong (_∷_ a) (assoc⁻¹-semantics {♭ F a} as)
assoc⁻¹-semantics {I}     {I}     {I}     (() ∷ as)

-- Congruence for concatenation, where the rhs can assume the lhs has terminated

++-cong : ∀ {S T} {as₁ as₂ : Trace S} {bs₁ bs₂ : Trace T} →
  (as₁ ≡ as₂) → (as₁ ✓ → bs₁ ≡ bs₂) → (as₁ ++ bs₁) ≡ (as₂ ++ bs₂)
++-cong {I}     {T} {[]}      refl bs₁≡bs₂ = bs₁≡bs₂ []
++-cong {Σ V F} {T} {[]}      refl bs₁≡bs₂ = refl
++-cong {Σ V F} {T} {a ∷ as}  refl bs₁≡bs₂ = cong (_∷_ a) (++-cong refl (λ ✓as → bs₁≡bs₂ (a ∷ ✓as)))
++-cong {I}     {T} {() ∷ as} refl bs₁≡bs₂

-- Concatenation respects and reflects termination

++-resp-✓ : ∀ {S T} {as : Trace S} {bs : Trace T} → (as ✓) → (bs ✓) → (as ++ bs ✓)
++-resp-✓         []         ✓bs = ✓bs
++-resp-✓ {Σ V F} (a ∷ ✓as)  ✓bs = a ∷ ++-resp-✓ ✓as ✓bs
++-resp-✓ {I}     (() ∷ ✓as) ✓bs

++-refl-✓₁ : ∀ {S T} {as : Trace S} {bs : Trace T} → (as ++ bs ✓) → (as ✓)
++-refl-✓₁ {I}     {T} {[]}      ✓cs        = []
++-refl-✓₁ {Σ V F} {T} {a ∷ as}  (.a ∷ ✓cs) = a ∷ ++-refl-✓₁ ✓cs
++-refl-✓₁ {I}     {T} {() ∷ as} ✓cs
++-refl-✓₁ {Σ V F} {T} {[]}      ()

++-refl-✓₂ : ∀ {S T} {as : Trace S} {bs : Trace T} → (as ++ bs ✓) → (bs ✓)
++-refl-✓₂ {I}     {T} {[]}      ✓cs        = ✓cs
++-refl-✓₂ {Σ W F} {T} {a ∷ as}  (.a ∷ ✓cs) = ++-refl-✓₂ {♭ F a} {T} {as} ✓cs
++-refl-✓₂ {I}     {T} {() ∷ as} cs
++-refl-✓₂ {Σ V F} {T} {[]}      ()

-- Concatenaton respects emptiness

++-resp-[] : ∀ {S T} {as : Trace S} {bs : Trace T} →
  (as ≡ []) → (bs ≡ []) → (as ++ bs ≡ [])
++-resp-[] {I}     refl refl = refl
++-resp-[] {Σ V F} refl refl = refl

-- Beta and eta equivalence for concatenation.
-- Note that β₂ only holds when as is complete.

++-β₁ : ∀ {S T} (as : Trace S) → (bs : Trace T) → (front (as ++ bs) ≡ as)
++-β₁ {I}     []        bs = refl
++-β₁ {I}     (() ∷ as) bs
++-β₁ {Σ V F} []        bs = refl
++-β₁ {Σ V F} (a ∷ as)  bs = cong (_∷_ a) (++-β₁ as bs)

++-β₂ : ∀ {S T} {as : Trace S} → (as ✓) → (bs : Trace T) → (back {S} (as ++ bs) ≡ bs)
++-β₂ {I}     []        bs = refl
++-β₂ {Σ V F} (a ∷ as)  bs = ++-β₂ as bs
++-β₂ {I}     (() ∷ as) bs

++-η : ∀ {S T} (as : Trace (S & T)) → (front {S} as ++ back {S} as ≡ as)
++-η {I}     []       = refl
++-η {I}     (a ∷ as) = refl
++-η {Σ V F} []       = refl
++-η {Σ V F} (a ∷ as) = cong (_∷_ a) (++-η {♭ F a} as)

-- Beta for concatenation with an incomplete trace

++-β₂-[] : ∀ {S T} {as : Trace S} → (¬ (as ✓)) → (bs : Trace T) → (back {S} (as ++ bs) ≡ [])
++-β₂-[] {I}     {T} {[]}      ¬✓[]   bs = ⊥-elim (¬✓[] [])
++-β₂-[] {Σ V F} {T} {[]}      ¬✓[]   bs = refl
++-β₂-[] {Σ V F} {T} {a ∷ as}  ¬✓a∷as bs = ++-β₂-[] (λ ✓as → ¬✓a∷as (a ∷ ✓as)) bs
++-β₂-[] {I}     {T} {() ∷ as} ¬✓a∷as bs

-- If the front of a trace is incomplete then its back is empty

back≡[] : ∀ {S T as} → (¬ (front {S} {T} as ✓)) → (back {S} {T} as ≡ [])
back≡[] {I}     {T} {as}     ¬✓as₁   = ⊥-elim (¬✓as₁ [])
back≡[] {Σ V F} {T} {[]}     ¬✓as₁   = refl
back≡[] {Σ V F} {T} {a ∷ as} ¬✓a∷as₁ = back≡[] (λ ✓as₁ → ¬✓a∷as₁ (a ∷ ✓as₁))

-- Front respects completion, but only reflects it when T = I.

front-resp-✓ :  ∀ {S T} {as : Trace (S & T)} → (as ✓) → (front {S} as ✓)
front-resp-✓ {I}     ✓as       = []
front-resp-✓ {Σ V F} (a ∷ ✓as) = a ∷ front-resp-✓ ✓as

front-refl-✓ :  ∀ {S} (as : Trace (S & I)) → (front {S} as ✓) → (as ✓)
front-refl-✓ {I}     []        ✓as₁        = []
front-refl-✓ {Σ V F} (a ∷ as)  (.a ∷ ✓as₁) = a ∷ front-refl-✓ as ✓as₁
front-refl-✓ {I}     (() ∷ as) ✓as₁
front-refl-✓ {Σ V F} []        ()

-- Back respects emptiness

back-resp-[] : ∀ {S T as} → (as ≡ []) → (back {S} {T} as ≡ [])
back-resp-[] {I}     refl = refl
back-resp-[] {Σ V F} refl = refl

-- Back reflects completion for non-trivial T

back-refl-✓ :  ∀ {S T} {isΣ : IsΣ T} (as : Trace (S & T)) → (back {S} as ✓) → (as ✓)
back-refl-✓ {I}             as       ✓as₂ = ✓as₂
back-refl-✓ {Σ V F} {Σ W G} (a ∷ as) ✓as₂ = a ∷ back-refl-✓ {♭ F a} as ✓as₂
back-refl-✓ {Σ V F} {I}  {} as       ✓as₂
back-refl-✓ {Σ V F} {Σ W G} []       ()

-- Back respects completion

back-resp-✓ :  ∀ {S} {T} {as : Trace (S & T)} → (as ✓) → (back {S} as ✓)
back-resp-✓ {I}     ✓as       = ✓as
back-resp-✓ {Σ W F} (a ∷ ✓as) = back-resp-✓ {♭ F a} ✓as

-- Tensor plays nicely with concatenation when f reflects completion

⟦[&]⟧-++ : ∀ {S T U V} (f : Trace S → Trace T) (g : Trace U → Trace V) →
  (∀ cs → (f cs ✓) → (cs ✓)) → ∀ as bs →
    (f ⟦[&]⟧ g) (as ++ bs) ≡ (f as ++ g bs)
⟦[&]⟧-++ {S} {T} {U} {V} f g f-refl-✓ as bs =
  begin
    f (front {S} (as ++ bs)) ++ g (back {S} (as ++ bs))
  ≡⟨ cong₂ _++_ (cong f (++-β₁ as bs)) refl ⟩
    f as ++ g (back {S} (as ++ bs))
  ≡⟨ ++-cong refl (λ ✓fas → cong g (++-β₂ (f-refl-✓ as ✓fas) bs)) ⟩
    f as ++ g bs
  ∎

-- Tensor respects ≃

[&]-resp-≃ : ∀ {S T U V} {P₁ P₂ : S ⇒ T} {Q₁ Q₂ : U ⇒ V} →
  (⟦ P₁ ⟧ ≃ ⟦ P₂ ⟧) → (⟦ Q₁ ⟧ ≃ ⟦ Q₂ ⟧) →
    (⟦ P₁ [&] Q₁ ⟧ ≃ ⟦ P₂ [&] Q₂ ⟧)
[&]-resp-≃ {S} {T} {U} {V} {P₁} {P₂} {Q₁} {Q₂} P₁≃P₂ Q₁≃Q₂ as =
  begin
    ⟦ P₁ [&] Q₁ ⟧ as
  ≡⟨ [&]-≃-⟦[&]⟧ P₁≃P₂ Q₁≃Q₂ as ⟩
    (⟦ P₂ ⟧ ⟦[&]⟧ ⟦ Q₂ ⟧) as
  ≡⟨ sym ([&]-semantics P₂ Q₂ as) ⟩
    ⟦ P₂ [&] Q₂ ⟧ as
  ∎

-- Tensor respects identity

[&]-resp-done : ∀ S T → ⟦ done {S} [&] done {T} ⟧ ≃ ⟦ done {S & T} ⟧
[&]-resp-done S T as =
  begin
    ⟦ done {S} [&] done {T} ⟧ as
  ≡⟨ [&]-semantics (done {S}) (done {T}) as ⟩
    front {S} as ++ back {S} as
  ≡⟨ ++-η {S} as ⟩
    as
  ∎

-- Tensor respects composition when g₁ reflects completion

⟦[&]⟧-resp-⟦⟫⟧ : ∀ {S₁ S₂ T₁ T₂ U₁ U₂} →
  (f₁ : Trace S₁ → Trace T₁) → (g₁ : Trace T₁ → Trace U₁) →
    (f₂ : Trace S₂ → Trace T₂) → (g₂ : Trace T₂ → Trace U₂) →
      (∀ as → (g₁ as ✓) → (as ✓)) →
        (((f₁ ⟦⟫⟧ g₁) ⟦[&]⟧ (f₂ ⟦⟫⟧ g₂)) ≃ (f₁ ⟦[&]⟧ f₂) ⟦⟫⟧ (g₁ ⟦[&]⟧ g₂))
⟦[&]⟧-resp-⟦⟫⟧ {S₁} f₁ g₁ f₂ g₂ g₁-refl-✓ as =
  sym (⟦[&]⟧-++ g₁ g₂ g₁-refl-✓ (f₁ (front {S₁} as)) (f₂ (back {S₁} as)))

-- Tensor respects composition when f₁ respects completion and f₂ is strict

⟦[&]⟧-resp-⟦⟫⟧' : ∀ {S₁ S₂ T₁ T₂ U₁ U₂} →
  (f₁ : Trace S₁ → Trace T₁) → (g₁ : Trace T₁ → Trace U₁) →
    (f₂ : Trace S₂ → Trace T₂) → (g₂ : Trace T₂ → Trace U₂) →
       (∀ as → as ✓ → f₁ as ✓) → (f₂ [] ≡ []) →
        (((f₁ ⟦⟫⟧ g₁) ⟦[&]⟧ (f₂ ⟦⟫⟧ g₂)) ≃ (f₁ ⟦[&]⟧ f₂) ⟦⟫⟧ (g₁ ⟦[&]⟧ g₂))
⟦[&]⟧-resp-⟦⟫⟧' {S₁} {S₂} {T₁} {T₂} f₁ g₁ f₂ g₂ f₁-resp-✓ f₂[]≡[] as with ✓? (f₁ (front as))
⟦[&]⟧-resp-⟦⟫⟧' {S₁} {S₂} {T₁} {T₂} f₁ g₁ f₂ g₂ f₁-resp-✓ f₂[]≡[] as | yes ✓bs₁ =
  cong₂ _++_ (cong g₁ (sym (++-β₁ _ _))) (cong g₂ (sym (++-β₂ ✓bs₁ _)))
⟦[&]⟧-resp-⟦⟫⟧' {S₁} {S₂} {T₁} {T₂} f₁ g₁ f₂ g₂ f₁-resp-✓ f₂[]≡[] as | no ¬✓bs₁ =
  begin
    g₁ (f₁ as₁) ++ g₂ (f₂ as₂)
  ≡⟨ cong (_++_  (g₁ (f₁ as₁))) (cong g₂ (cong f₂ (back≡[] ¬✓as₁))) ⟩
    g₁ (f₁ as₁) ++ g₂ (f₂ [])
  ≡⟨ cong (_++_  (g₁ (f₁ as₁))) (cong g₂ f₂[]≡[]) ⟩
    g₁ (f₁ as₁) ++ g₂ []
  ≡⟨ cong₂ _++_ (cong g₁ (sym (++-β₁ _ _))) (cong g₂ (sym (++-β₂-[] ¬✓bs₁ _))) ⟩
    g₁ (front (f₁ as₁ ++ f₂ as₂)) ++ g₂ (back {T₁} (f₁ as₁ ++ f₂ as₂))
  ∎ where
  as₁ = front {S₁} as
  as₂ = back {S₁} as
  ¬✓as₁ : ¬ as₁ ✓
  ¬✓as₁ = λ as₁✓ → ¬✓bs₁ (f₁-resp-✓ as₁ as₁✓)

-- Tensor respects composition when Q₁ is reflective

[&]-resp-⟫ : ∀ {S₁ S₂ T₁ T₂ U₁ U₂}
  (P₁ : S₁ ⇒ T₁) {Q₁ : T₁ ⇒ U₁} (⟳Q₁ : Reflective Q₁)
    (P₂ : S₂ ⇒ T₂) (Q₂ : T₂ ⇒ U₂) →
      ⟦ (P₁ ⟫ Q₁) [&] (P₂ ⟫ Q₂) ⟧ ≃ ⟦ (P₁ [&] P₂) ⟫ (Q₁ [&] Q₂) ⟧
[&]-resp-⟫ P₁ {Q₁} ⟳Q₁ P₂ Q₂ as =
  begin
    ⟦ (P₁ ⟫ Q₁) [&] (P₂ ⟫ Q₂) ⟧ as
  ≡⟨ [&]-≃-⟦[&]⟧ (⟫-semantics P₁ Q₁) (⟫-semantics P₂ Q₂) as ⟩
    ((⟦ P₁ ⟧ ⟦⟫⟧ ⟦ Q₁ ⟧) ⟦[&]⟧ (⟦ P₂ ⟧ ⟦⟫⟧ ⟦ Q₂ ⟧)) as
  ≡⟨ ⟦[&]⟧-resp-⟦⟫⟧ ⟦ P₁ ⟧ ⟦ Q₁ ⟧ ⟦ P₂ ⟧ ⟦ Q₂ ⟧ (⟦⟧-refl-✓ ⟳Q₁) as ⟩
    ((⟦ P₁ ⟧ ⟦[&]⟧ ⟦ P₂ ⟧) ⟦⟫⟧ (⟦ Q₁ ⟧ ⟦[&]⟧ ⟦ Q₂ ⟧)) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ ([&]-semantics P₁ P₂) ([&]-semantics Q₁ Q₂) as) ⟩
    ⟦ P₁ [&] P₂ ⟫ Q₁ [&] Q₂ ⟧ as
  ∎

-- Tensor respects composition when P₂ is strict

[&]-resp-⟫' : ∀ {S₁ S₂ T₁ T₂ U₁ U₂}
  (P₁ : S₁ ⇒ T₁) (Q₁ : T₁ ⇒ U₁)
    {P₂ : S₂ ⇒ T₂} (#P₂ : Strict P₂) (Q₂ : T₂ ⇒ U₂) →
      ⟦ (P₁ ⟫ Q₁) [&] (P₂ ⟫ Q₂) ⟧ ≃ ⟦ (P₁ [&] P₂) ⟫ (Q₁ [&] Q₂) ⟧
[&]-resp-⟫' P₁ Q₁ {P₂} #P₂ Q₂ as =
  begin
    ⟦ (P₁ ⟫ Q₁) [&] (P₂ ⟫ Q₂) ⟧ as
  ≡⟨ [&]-≃-⟦[&]⟧ (⟫-semantics P₁ Q₁) (⟫-semantics P₂ Q₂) as ⟩
    ((⟦ P₁ ⟧ ⟦⟫⟧ ⟦ Q₁ ⟧) ⟦[&]⟧ (⟦ P₂ ⟧ ⟦⟫⟧ ⟦ Q₂ ⟧)) as
  ≡⟨ ⟦[&]⟧-resp-⟦⟫⟧' ⟦ P₁ ⟧ ⟦ Q₁ ⟧ ⟦ P₂ ⟧ ⟦ Q₂ ⟧ (⟦⟧-resp-✓ P₁) (⟦⟧-resp-[] #P₂) as ⟩
    ((⟦ P₁ ⟧ ⟦[&]⟧ ⟦ P₂ ⟧) ⟦⟫⟧ (⟦ Q₁ ⟧ ⟦[&]⟧ ⟦ Q₂ ⟧)) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ ([&]-semantics P₁ P₂) ([&]-semantics Q₁ Q₂) as) ⟩
    ⟦ P₁ [&] P₂ ⟫ Q₁ [&] Q₂ ⟧ as
  ∎

-- Units and associator are equivalences

unit₁-isEquiv : ∀ {S} → IsEquiv (unit₁ {S})
unit₁-isEquiv = isEquiv ∼-unit₁ ≃-refl

unit₂-isEquiv : ∀ {S} → IsEquiv (unit₂ {S})
unit₂-isEquiv {S} = isEquiv (∼-unit₂ {S}) ≃-refl

assoc-isEquiv : ∀ {S T U} → IsEquiv (assoc {S} {T} {U})
assoc-isEquiv {S} {T} = isEquiv (∼-assoc {S} {T}) ≃-refl

unit₁⁻¹-isEquiv : ∀ {S} → IsEquiv (unit₁⁻¹ {S})
unit₁⁻¹-isEquiv = isEquiv (∼-sym ∼-unit₁) ≃-refl

unit₂⁻¹-isEquiv : ∀ {S} → IsEquiv (unit₂⁻¹ {S})
unit₂⁻¹-isEquiv = isEquiv (∼-sym ∼-unit₂) ≃-refl

assoc⁻¹-isEquiv : ∀ {S T U} → IsEquiv (assoc⁻¹ {S} {T} {U})
assoc⁻¹-isEquiv {S} = isEquiv (∼-sym (∼-assoc {S})) ≃-refl

-- Equivalence respects &

&-resp-∼ : ∀ {S T U V} → (S ∼ T) → (U ∼ V) → ((S & U) ∼ (T & V))
&-resp-∼ I       U∼V = U∼V
&-resp-∼ (Σ V F) U∼V = Σ V (♯ λ a → &-resp-∼ (♭ F a) U∼V)

equiv-resp-⟦[&]⟧ : ∀ {S T U V} (S∼T : S ∼ T) (U∼V : U ∼ V) →
  ⟦ equiv S∼T ⟧ ⟦[&]⟧ ⟦ equiv U∼V ⟧ ≃ ⟦ equiv (&-resp-∼ S∼T U∼V) ⟧
equiv-resp-⟦[&]⟧ I       U∼V as       = refl
equiv-resp-⟦[&]⟧ (Σ V F) U∼V []       = refl
equiv-resp-⟦[&]⟧ (Σ V F) U∼V (a ∷ as) = cong (_∷_ a) (equiv-resp-⟦[&]⟧ (♭ F a) U∼V as)

equiv-resp-[&] : ∀ {S T U V} (S∼T : S ∼ T) (U∼V : U ∼ V) →
  ⟦ equiv S∼T [&] equiv U∼V ⟧ ≃ ⟦ equiv (&-resp-∼ S∼T U∼V) ⟧
equiv-resp-[&] S∼T U∼V as =
  begin
    ⟦ equiv S∼T [&] equiv U∼V ⟧ as
  ≡⟨ [&]-semantics (equiv S∼T) (equiv U∼V) as ⟩
    (⟦ equiv S∼T ⟧ ⟦[&]⟧ ⟦ equiv U∼V ⟧) as
  ≡⟨ equiv-resp-⟦[&]⟧ S∼T U∼V as ⟩
    ⟦ equiv (&-resp-∼ S∼T U∼V) ⟧ as
  ∎

[&]-isEquiv : ∀ {S T U V} {P : S ⇒ T} {Q : U ⇒ V} →
  (IsEquiv P) → (IsEquiv Q) → (IsEquiv (P [&] Q))
[&]-isEquiv {S} {T} {U} {V} {P} {Q} (isEquiv S∼T P≃S∼T) (isEquiv U∼V Q≃U∼V) =
  isEquiv (&-resp-∼ S∼T U∼V) λ as →
    begin
      ⟦ P [&] Q ⟧ as
    ≡⟨ [&]-resp-≃ P≃S∼T Q≃U∼V as ⟩
      ⟦ equiv S∼T [&] equiv U∼V ⟧ as
    ≡⟨ equiv-resp-[&] S∼T U∼V as ⟩
      ⟦ equiv (&-resp-∼ S∼T U∼V) ⟧ as
    ∎

-- Isomorphisms

unit₁-iso : ∀ {S} → ⟦ unit₁ {S} ⟫ unit₁⁻¹ {S} ⟧ ≃ ⟦ done ⟧
unit₁-iso = equiv-is-iso unit₁-isEquiv unit₁⁻¹-isEquiv

unit₁⁻¹-iso : ∀ {S} → ⟦ unit₁⁻¹ {S} ⟫ unit₁ {S} ⟧ ≃ ⟦ done ⟧
unit₁⁻¹-iso = equiv-is-iso unit₁⁻¹-isEquiv unit₁-isEquiv

unit₂-iso : ∀ {S} → ⟦ unit₂ {S} ⟫ unit₂⁻¹ {S} ⟧ ≃ ⟦ done ⟧
unit₂-iso {S} = equiv-is-iso (unit₂-isEquiv {S}) unit₂⁻¹-isEquiv

unit₂⁻¹-iso : ∀ {S} → ⟦ unit₂⁻¹ {S} ⟫ unit₂ {S} ⟧ ≃ ⟦ done ⟧
unit₂⁻¹-iso {S} = equiv-is-iso unit₂⁻¹-isEquiv (unit₂-isEquiv {S})

assoc-iso : ∀ {S T U} → ⟦ assoc {S} {T} {U} ⟫ assoc⁻¹ {S} {T} {U} ⟧ ≃ ⟦ done ⟧
assoc-iso {S} {T} = equiv-is-iso (assoc-isEquiv {S} {T}) (assoc⁻¹-isEquiv {S} {T})

assoc⁻¹-iso : ∀ {S T U} → ⟦ assoc⁻¹ {S} {T} {U} ⟫ assoc {S} {T} {U} ⟧ ≃ ⟦ done ⟧
assoc⁻¹-iso {S} {T} = equiv-is-iso (assoc⁻¹-isEquiv {S} {T}) (assoc-isEquiv {S} {T})

-- Coherence conditions

assoc-unit : ∀ {S T} →
  ⟦ done {S} [&] unit₁ {T} ⟧ ≃ ⟦ assoc {S} {I} {T} ⟫ unit₂ {S} [&] done {T} ⟧
assoc-unit {S} {T} =
  ≃-equiv ([&]-isEquiv (done-isEquiv {S}) (unit₁-isEquiv {T}))
    (⟫-isEquiv (assoc-isEquiv {S} {I} {T}) ([&]-isEquiv (unit₂-isEquiv {S}) (done-isEquiv {T})))

assoc-assoc : ∀ {S T U V} →
  ⟦ done {S} [&] assoc {T} {U} {V} ⟫
      assoc {S} {T & U} {V} ⟫
        assoc {S} {T} {U} [&] done {V} ⟧ ≃
  ⟦ assoc {S} {T} {U & V} ⟫ assoc {S & T} {U} {V} ⟧
assoc-assoc {S} {T} {U} {V} =
  ≃-equiv
    (⟫-isEquiv ([&]-isEquiv (done-isEquiv {S}) (assoc-isEquiv {T} {U} {V}))
      (⟫-isEquiv (assoc-isEquiv {S} {T & U} {V})
        ([&]-isEquiv (assoc-isEquiv {S} {T} {U}) done-isEquiv)))
    (⟫-isEquiv (assoc-isEquiv {S} {T} {U & V}) (assoc-isEquiv {S & T} {U} {V}))

-- Concatenation plays nicely with associativity

⟦assoc⟧-++ : ∀ {S T U} → (as : Trace S) (bs : Trace T) (cs : Trace U) →
  ⟦assoc⟧ {S} (as ++ (bs ++ cs)) ≡ ((as ++ bs) ++ cs)
⟦assoc⟧-++ {I} {I}     []        bs       cs = refl
⟦assoc⟧-++ {I} {Σ W G} []        []       cs = refl
⟦assoc⟧-++ {I} {Σ W G} []        (b ∷ bs) cs = cong (_∷_ b) (⟦assoc⟧-++ {I} [] bs cs)
⟦assoc⟧-++ {Σ W F}     []        bs       cs = refl
⟦assoc⟧-++ {Σ W F}     (a ∷ as)  bs       cs = cong (_∷_ a) (⟦assoc⟧-++ as bs cs)
⟦assoc⟧-++ {I}         (() ∷ as) bs       cs

⟦assoc⁻¹⟧-++ : ∀ {S T U} → (as : Trace S) (bs : Trace T) (cs : Trace U) →
  ⟦assoc⁻¹⟧ {S} ((as ++ bs) ++ cs) ≡ (as ++ (bs ++ cs))
⟦assoc⁻¹⟧-++ {I} {I}     []        bs       cs = refl
⟦assoc⁻¹⟧-++ {I} {Σ W G} []        []       cs = refl
⟦assoc⁻¹⟧-++ {I} {Σ W G} []        (b ∷ bs) cs = cong (_∷_ b) (⟦assoc⁻¹⟧-++ {I} [] bs cs)
⟦assoc⁻¹⟧-++ {Σ W F}     []        bs       cs = refl
⟦assoc⁻¹⟧-++ {Σ W F}     (a ∷ as)  bs       cs = cong (_∷_ a) (⟦assoc⁻¹⟧-++ as bs cs)
⟦assoc⁻¹⟧-++ {I}         (() ∷ as) bs       cs

-- Front and back play well with associativity

front-⟦assoc⟧ : ∀ {S T U} (as : Trace (S & (T & U))) →
  (front {S} as ≡ front {S} (front {S & T} (⟦assoc⟧ {S} as)))
front-⟦assoc⟧ {I}     as = refl
front-⟦assoc⟧ {Σ V F} []       = refl
front-⟦assoc⟧ {Σ V F} (a ∷ as) = cong (_∷_ a) (front-⟦assoc⟧ as)

mid-⟦assoc⟧ : ∀ {S T U} (as : Trace (S & (T & U))) →
  (front {T} (back {S} as) ≡ back {S} (front {S & T} (⟦assoc⟧ {S} as)))
mid-⟦assoc⟧ {I}     {T}     as       = cong (front {T}) (sym (++-η {T} as))
mid-⟦assoc⟧ {Σ V F} {I}     []       = refl
mid-⟦assoc⟧ {Σ V F} {Σ W G} []       = refl
mid-⟦assoc⟧ {Σ V F}         (a ∷ as) = mid-⟦assoc⟧ {♭ F a} as

back-⟦assoc⟧ : ∀ {S T U} (as : Trace (S & (T & U))) →
  (back {T} (back {S} as) ≡ back {S & T} (⟦assoc⟧ {S} as))
back-⟦assoc⟧ {I}     {T}     as       = cong (back {T}) (sym (++-η {T} as))
back-⟦assoc⟧ {Σ V F} {I}     []       = refl
back-⟦assoc⟧ {Σ V F} {Σ W G} []       = refl
back-⟦assoc⟧ {Σ V F}         (a ∷ as) = back-⟦assoc⟧ {♭ F a} as

-- Units are natural

⟦unit₁⟧-natural : ∀ {S T} (f : Trace S → Trace T) →
  (⟦done⟧ {I} ⟦[&]⟧ f) ⟦⟫⟧ ⟦unit₁⟧ ≃ ⟦unit₁⟧ ⟦⟫⟧ f
⟦unit₁⟧-natural f []       = refl
⟦unit₁⟧-natural f (a ∷ as) = refl

unit₁-natural : ∀ {S T} (P : S ⇒ T) →
  ⟦ done {I} [&] P ⟫ unit₁ ⟧ ≃ ⟦ unit₁ ⟫ P ⟧
unit₁-natural P as =
  begin
    ⟦ done {I} [&] P ⟫ unit₁ ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ ([&]-semantics (done {I}) P) unit₁-semantics as ⟩
    (⟦done⟧ {I} ⟦[&]⟧ ⟦ P ⟧ ⟦⟫⟧ ⟦unit₁⟧) as
  ≡⟨ ⟦unit₁⟧-natural ⟦ P ⟧ as ⟩
     (⟦unit₁⟧ ⟦⟫⟧ ⟦ P ⟧) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ unit₁-semantics ≃-refl as) ⟩
    ⟦ unit₁ ⟫ P ⟧ as
  ∎

⟦unit₂⟧-natural : ∀ {S T} (f : Trace S → Trace T) →
  (f ⟦[&]⟧ ⟦done⟧ {I}) ⟦⟫⟧ ⟦unit₂⟧ ≃ ⟦unit₂⟧ ⟦⟫⟧ f
⟦unit₂⟧-natural {S} {T} f as =
  ++-β₁ (f (front {S} as)) (back {S} as)

unit₂-natural : ∀ {S T} (P : S ⇒ T) →
  ⟦ P [&] done {I} ⟫ unit₂ ⟧ ≃ ⟦ unit₂ ⟫ P ⟧
unit₂-natural {S} {T} P as =
  begin
    ⟦ P [&] done {I} ⟫ unit₂ ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ ([&]-semantics P (done {I})) (unit₂-semantics {T}) as ⟩
    (⟦ P ⟧ ⟦[&]⟧ ⟦done⟧ {I} ⟦⟫⟧ ⟦unit₂⟧) as
  ≡⟨ ⟦unit₂⟧-natural ⟦ P ⟧ as ⟩
     (⟦unit₂⟧ ⟦⟫⟧ ⟦ P ⟧) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ (unit₂-semantics {S}) ≃-refl as) ⟩
    ⟦ unit₂ ⟫ P ⟧ as
  ∎

-- Associativity is natural

⟦assoc⟧-natural : ∀ {S S' T T' U U'}
  (f : Trace S → Trace S') (g : Trace T → Trace T') (h : Trace U → Trace U') →
    ((f ⟦[&]⟧ (g ⟦[&]⟧ h)) ⟦⟫⟧ ⟦assoc⟧ {S'} {T'} {U'}) ≃
      (⟦assoc⟧ {S} {T} {U} ⟦⟫⟧ ((f ⟦[&]⟧ g) ⟦[&]⟧ h))
⟦assoc⟧-natural {S} {S'} {T} {T'} {U} {U'} f g h as =
  begin
    ⟦assoc⟧ {S'} (f as₁ ++ g as₂ ++ h as₃)
  ≡⟨ ⟦assoc⟧-++ (f as₁) (g as₂) (h as₃) ⟩
    (f as₁ ++ g as₂) ++ h as₃
  ≡⟨ cong₂ _++_ (cong₂ _++_ (cong f (front-⟦assoc⟧ as))
       (cong g (mid-⟦assoc⟧ {S} as))) (cong h (back-⟦assoc⟧ {S} as)) ⟩
    ((f ⟦[&]⟧ g) ⟦[&]⟧ h) ((as₁ ++ as₂) ++ as₃)
  ∎ where
  as₁ = front {S} as
  as₂ = front {T} (back {S} as)
  as₃ = back {T} (back {S} as)

assoc-natural : ∀ {S S' T T' U U'} (P : S ⇒ S') (Q : T ⇒ T') (R : U ⇒ U') →
  ⟦ P [&] (Q [&] R) ⟫ assoc {S'} {T'} {U'} ⟧ ≃
    ⟦ assoc {S} {T} {U} ⟫ (P [&] Q) [&] R ⟧
assoc-natural {S} {S'} {T} {T'} {U} {U'} P Q R as =
  begin
    ⟦ P [&] (Q [&] R) ⟫ assoc {S'} {T'} {U'} ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ ([&]-≃-⟦[&]⟧ {P = P} ≃-refl ([&]-semantics Q R)) (assoc-semantics {S'} {T'} {U'}) as ⟩
    ((⟦ P ⟧ ⟦[&]⟧ (⟦ Q ⟧ ⟦[&]⟧ ⟦ R ⟧)) ⟦⟫⟧ ⟦assoc⟧ {S'} {T'} {U'}) as
  ≡⟨ ⟦assoc⟧-natural ⟦ P ⟧ ⟦ Q ⟧ ⟦ R ⟧ as ⟩
    (⟦assoc⟧ {S} {T} {U} ⟦⟫⟧ ((⟦ P ⟧ ⟦[&]⟧ ⟦ Q ⟧) ⟦[&]⟧ ⟦ R ⟧)) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ (assoc-semantics {S} {T} {U}) ([&]-≃-⟦[&]⟧ ([&]-semantics P Q) ≃-refl) as) ⟩
    ⟦ assoc {S} {T} {U} ⟫ (P [&] Q) [&] R ⟧ as
  ∎

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
open import Proc

module Silence (param : Param) where

open import Basics
import Interp
import Hear

open Process param
open Interp param
open Hear param

NoSpeak : {a : U} -> Proc a -> Set
NoSpeak {a} p = (w : LT a)(q : Proc a) -> ¬ (p -! w !-> q)

silent-nospeak : {a : U}{p : Proc a} -> Silent p -> NoSpeak p
silent-nospeak silent-o          w  q  ()
silent-nospeak silent->          w  q  ()
silent-nospeak (silent-|| s1 s2) w  ._ (tx-!| h _) = silent-nospeak s1 _ _ h
silent-nospeak (silent-|| s1 s2) w  ._ (tx-|! _ h) = silent-nospeak s2 _ _ h
silent-nospeak (silent-def s)    w  q  (tx-def h)  = silent-nospeak s _ _ h
silent-nospeak (silent-/| s)     ._ ._ (tx-/| h)   = silent-nospeak s _ _ h

nospeak-silent : {a : U}{p : Proc a} -> Guard p -> NoSpeak p -> Silent p
nospeak-silent og           s = silent-o
nospeak-silent (>g f)       s = silent->
nospeak-silent (w !g p)     s = kill (s _ _ tx-!)
nospeak-silent (w ! p +g f) s = kill (s _ _ tx-+)
nospeak-silent (g1 ||g g2)  s =
    silent-|| (nospeak-silent g1 (inv1 g2 s))
              (nospeak-silent g2 (inv2 g1 s))
  where
    module Inv {a : U}{p1 p2 : Proc a} where
      inv1 : Guard p2 -> NoSpeak (p1 || p2) -> NoSpeak p1
      inv1 g2 h w p t = h _ _ (tx-!| t (sound g2))

      inv2 : Guard p1 -> NoSpeak (p1 || p2) -> NoSpeak p2
      inv2 g1 h w p t = h _ _ (tx-|! (sound g1) t)
    open Inv
nospeak-silent (φ /|g g)    s = silent-/| (nospeak-silent g (inv s))
  where
    inv : forall {p} -> NoSpeak (φ /| p) -> NoSpeak p
    inv h w p t = h _ _ (tx-/| t)
nospeak-silent (defg x g)   s = silent-def (nospeak-silent g (inv s))
  where
    inv : NoSpeak (def x) -> NoSpeak (env _ x)
    inv h w p t = h _ _ (tx-def t)

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence

module HoTT.Equivalence.Transport where

open variables

transport-equiv : {x y : A} → x == y → P x ≃ P y
transport-equiv {A = A} {P = P} p = f , qinv→isequiv (g , η p , ε p)
  where
  f = transport P p
  g = transport P (p ⁻¹)
  variable x y : A
  η : (p : x == y) → transport P (p ⁻¹) ∘ transport P p ~ id
  η refl _ = refl
  ε : (p : x == y) → transport P p ∘ transport P (p ⁻¹) ~ id
  ε refl _ = refl

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module Data where

import      Lvl
open import Type

-- An empty type which cannot be constructed.
-- By default, this should be used to represent _the_ empty type.
data Empty {ℓ} : Type{ℓ} where
{-# FOREIGN GHC data Empty ℓ #-}
{-# COMPILE GHC Empty = data Empty () #-}

-- Empty functions.
-- The empty type eliminator.
-- Any type can be constructed from the empty type.
empty : ∀{ℓ₁ ℓ₂}{T : Type{ℓ₁}} → Empty{ℓ₂} → T
empty ()
{-# COMPILE GHC empty = \_ _ _ e -> case e of{} #-}

-- An unit type which can only be constructed in one way.
-- By default, this should be used to represent _the_ unit type.
record Unit {ℓ} : Type{ℓ} where
  instance constructor <>
open Unit public

{-# BUILTIN UNIT Unit #-}
{-# FOREIGN GHC type Unit ℓ = () #-}
{-# COMPILE GHC Unit = data Unit (()) #-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Data.Maybe.Base where

open import Level

data Maybe (A : Type a) : Type a where
  nothing : Maybe A
  just : A → Maybe A

maybe : {B : Maybe A → Type b} → B nothing → ((x : A) → B (just x)) → (x : Maybe A) → B x
maybe b f nothing = b
maybe b f (just x) = f x

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Homomorphism.Definitions (Σ : Signature) where

open import Fragment.Algebra.Algebra Σ

open import Level using (Level; _⊔_)
open import Relation.Binary using (Setoid)
open import Data.Vec using (Vec; map)

open import Function using (Congruent) public

private
  variable
    a b ℓ₁ ℓ₂ : Level

Homomorphic : (S : Algebra {a} {ℓ₁}) (T : Algebra {b} {ℓ₂})
              → (∥ S ∥ → ∥ T ∥) → Set (a ⊔ ℓ₂)
Homomorphic S T h = ∀ {arity} → (f : ops Σ arity)
                    → (xs : Vec ∥ S ∥ arity)
                    → T ⟦ f ⟧ (map h xs) =[ T ] h (S ⟦ f ⟧ xs)

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Helper where

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

open import Categories.Category.Core using (Category)

-- Since we add extra proofs in the definition of `Category` (i.e. `sym-assoc` and
-- `identity²`), we might still want to construct a `Category` in its originally
-- easier manner. Thus, this redundant definition is here to ease the construction.
record CategoryHelper (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  infix  4 _≈_ _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    _≈_ : ∀ {A B} → Rel (A ⇒ B) e

    id  : ∀ {A} → (A ⇒ A)
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i

categoryHelper : ∀ {o ℓ e} → CategoryHelper o ℓ e → Category o ℓ e
categoryHelper C = record
  { Obj       = Obj
  ; _⇒_       = _⇒_
  ; _≈_       = _≈_
  ; id        = id
  ; _∘_       = _∘_
  ; assoc     = assoc
  ; sym-assoc = sym assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identityˡ
  ; equiv     = equiv
  ; ∘-resp-≈  = ∘-resp-≈
  }
  where open CategoryHelper C
        module _ {A B} where
          open IsEquivalence (equiv {A} {B}) public

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
{-# OPTIONS --warning=error #-}
module Issue329 where

mutual
  infixl 0 D Undeclared
  data D : Set where

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module PLRTree {A : Set} where

open import BTree {A} hiding (flatten)
open import Data.List

data Tag : Set where
  perfect : Tag
  left : Tag
  right : Tag

data PLRTree : Set where
  leaf : PLRTree
  node : Tag → A → PLRTree → PLRTree → PLRTree

forget : PLRTree → BTree
forget leaf = leaf
forget (node _ x l r) = node x (forget l) (forget r)

flatten : PLRTree → List A
flatten leaf = []
flatten (node _ x l r) = x ∷ flatten l ++ flatten r

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import Data.Product using ( _×_ )
open import Web.Semantic.DL.Signature using ( Signature ; CN ; RN )

module Web.Semantic.DL.FOL where

-- A fragment of first order logic with no existentials or disjunctions.

infixr 4 _∧_

data Formula (Σ : Signature) (Δ : Set) : Set where
  true : Formula Σ Δ
  false : Formula Σ Δ
  _∧_ : Formula Σ Δ → Formula Σ Δ → Formula Σ Δ
  _∈₁_ : Δ → CN Σ → Formula Σ Δ
  _∈₁_⇒_ : Δ → CN Σ → Formula Σ Δ → Formula Σ Δ
  _∈₂_ : (Δ × Δ) → RN Σ → Formula Σ Δ
  _∈₂_⇒_ : (Δ × Δ) → RN Σ → Formula Σ Δ → Formula Σ Δ
  _∼_ : Δ → Δ → Formula Σ Δ
  _∼_⇒_ : Δ → Δ → Formula Σ Δ → Formula Σ Δ
  ∀₁ : (Δ → Formula Σ Δ) → Formula Σ Δ

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
-- Andreas, 2015-07-16
-- For printing lambda-bound names, name _ should behave as no name.

-- {-# OPTIONS -v tc.term.lambda:60 #-}

module _ where

Test = (A : Set) {A : Set} → A → A

works : Test
works = λ C x → {!!}

-- the goal should be displayed as ?0 : .A

g : Test
g = λ C {_} x → {!!}

-- the goal should be displayed as ?1 : .A
-- not ?1 : _ or ?1 : A

h : Test
h = λ C {_} → λ x → {!!}

-- the goal should be displayed as ?1 : .A
-- not ?1 : _ or ?1 : A


text:
-- Andreas, 2018-09-12, issue #3167-2: --(no-)prop option
--
-- A local --prop option should override a global --no-prop flag.
-- Issue3167prop.flags has --no-prop.

{-# OPTIONS --prop #-}

-- The following depends on Prop enabled

data _≡_ {a} {A : Prop a} (x : A) : A → Prop a where
  refl : x ≡ x

data P : Prop where
  a b : P

test : (x y : P) → x ≡ y
test x y = refl


text:
module BTA10 where
----------------------------------------
--equivalence between two typing systems
----------------------------------------
------------
--system one
------------
  --  module annotated-type-one where
  --  open import Data.Bool
  --  open import Data.List
  --  open import Data.Nat

  --  infix 4 _∈_
  --  data _∈_ {A : Set} : A → List A → Set where
  --    hd : ∀ {x xs} → x ∈ (x ∷ xs)
  --    tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

  --  data BT : Set where
  --    S : BT
  --    D : BT

  --  data _⊑_ : BT → BT → Set where
  --    bt-refl   : ∀ {bt} → bt ⊑ bt
  --    bt-≤-dyn  : ∀ {bt} → bt ⊑ D

  --  data atype : BT → Set where
  --   AInt : (bt : BT) → atype bt
  --   AFun : (bt : BT) → ∀ {bt₁ bt₂} → atype bt₁ → atype bt₂ → bt ⊑ bt₁ → bt ⊑ bt₂ → atype bt
  --   ⊎ : (bt : BT) → ∀ {bt₁ bt₂} → atype bt₁ → atype bt₂ → bt ⊑ bt₁ → bt ⊑ bt₂ → atype bt
  --   • : (bt : BT) → ∀ {bt₁ bt₂} → atype bt₁ → atype bt₂ → bt ⊑ bt₁ → bt ⊑ bt₂ → atype bt

  --  -- btof : ∀ {bt : BT} → atype bt → BT
  --  -- btof (AInt bt) = bt
  --  -- btof (AFun bt ty ty₁ x x₁) = bt
  --  -- btof (⊎ bt ty ty₁ x x₁) = bt
  --  -- btof (• bt ty ty₁ x x₁) = bt

  --  ----------------
  --  --typing context
  --  ----------------
  --  ----------------------
  --  --auxiliary definition
  --  ----------------------
  --  record Sg (S : Set) (T : S → Set) : Set where
  --    constructor _,_
  --    field
  --      ffst : S
  --      ssnd : T ffst
  --  open Sg public

  --  _of_ : (BT : Set) → (BT → Set) → Set
  --  BT of atype = Sg BT \ x → atype x

  --  AType : Set
  --  AType = BT of atype

  --  ---------
  --  --context
  --  ---------
  --  ACtx = List AType

  --  ---------
  --  --example
  --  ---------
  --  context1 : ACtx
  --  context1 = (D , AInt D) ∷ (S , AInt S) ∷ (S , AFun S (AInt D) (AInt D) bt-≤-dyn bt-≤-dyn) ∷ []

  --  ------------------
  --  --typed expression
  --  ------------------
  --  data AExp (Δ : ACtx) : AType → Set where
  --    Var : ∀ {α} → α ∈ Δ → AExp Δ α
  --    Int : (bt : BT) → ℕ → AExp Δ (bt , AInt bt)
  --    Add : ∀ {bt₁ bt₂} → (bt : BT) → AExp Δ (bt₁ , AInt bt₁) → AExp Δ (bt₂ , AInt bt₂)
  --                      → bt ⊑ bt₁ → bt ⊑ bt₂ → AExp Δ (bt , AInt bt)
  --    ALam : ∀ {b b' : BT} {α₁ : atype b} {α₂ : atype b'}  → (bt : BT)  → AExp ((b , α₁) ∷ Δ) (b' , α₂)
  --                      → (e₁ : bt ⊑ b) → (e₂ : bt ⊑ b') → AExp Δ (bt , AFun bt α₁ α₂ e₁ e₂)
  --    AApp : ∀ {b b' bt : BT} {α₁ : atype b} {α₂ : atype b'} {e₁ : bt ⊑ b} {e₂ : bt ⊑ b'}  → AExp Δ (bt , AFun bt α₁ α₂ e₁ e₂)
  --                      → AExp Δ (b , α₁) → AExp Δ (b' , α₂)
  -- -- Static pairs and sums
  --    _,_  : ∀ {b b' bt : BT} {α₁ : atype b} {α₂ : atype b'} → AExp Δ (b , α₁) → AExp Δ (b' , α₂)
  --                     → (e₁ : bt ⊑ b) → (e₂ : bt ⊑ b') → AExp Δ (bt , • bt α₁ α₂ e₁ e₂)
  --    Tl   : ∀ {b b' bt : BT} {α₁ : atype b} {α₂ : atype b'} → AExp Δ (b , α₁) → (e₁ : bt ⊑ b) → (e₂ : bt ⊑ b')
  --                     → AExp Δ (bt , ⊎ bt α₁ α₂ e₁ e₂)
  --    Tr   : ∀ {b b' bt : BT} {α₁ : atype b} {α₂ : atype b'} → AExp Δ (b' , α₂) → (e₁ : bt ⊑ b) → (e₂ : bt ⊑ b')
  --                     → AExp Δ (bt , ⊎ bt α₁ α₂ e₁ e₂)
  --    Fst  : ∀ {b b' bt : BT} {α₁ : atype b} {α₂ : atype b'} {e₁ : bt ⊑ b} {e₂ : bt ⊑ b'} → AExp Δ (bt , • bt α₁ α₂ e₁ e₂) → AExp Δ (b , α₁)
  --    Snd  : ∀ {b b' bt : BT} {α₁ : atype b} {α₂ : atype b'} {e₁ : bt ⊑ b} {e₂ : bt ⊑ b'} → AExp Δ (bt , • bt α₁ α₂ e₁ e₂) → AExp Δ (b' , α₂)
  --    Case : ∀ {b b' b'' bt : BT} {α₁ : atype b} {α₂ : atype b'} {α₃ : atype b''} {e₁ : bt ⊑ b} {e₂ : bt ⊑ b'}
  --                                 → AExp Δ (bt , ⊎ bt α₁ α₂ e₁ e₂) → AExp ((b , α₁) ∷ Δ) (b'' , α₃)
  --                                 → AExp ((b' , α₂) ∷ Δ) (b'' , α₃)
  --                                 → bt ⊑ b'' → AExp Δ (b'' , α₃)
  -- -- Liftable static terms
  -- -- ↑     : ∀ {α} → Liftable α → AExp Δ α  → AExp Δ (D (typeof α))

------------
--system two
------------

   module annotated-type-two where
   open import Data.Bool
   open import Data.List
   open import Data.Nat

   module traditional-representation where
   infix 4 _∈_
   data _∈_ {A : Set} : A → List A → Set where
     hd : ∀ {x xs} → x ∈ (x ∷ xs)
     tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

   data BT : Set where
     S : BT
     D : BT

   ------------------------------
   --binding time annotated types
   ------------------------------
   ------------------------------
   --Note
   --[BType] for ?
   --[AType] for annotated type
   ------------------------------
   mutual
     data AType : Set where
       an  : BT → BType → AType

     data BType : Set where
       BInt : BType
       BFun : AType → AType → BType
       _•_  : AType → AType → BType
       _⊎_  : AType → AType → BType

   ACtx = List AType

   ------------------
   --well-formed type
   ------------------
   ---------------------
   --auxiliaries
   ---------------------
   btof : AType → BT
   btof (an a x₁) = a

   data _⊑_ : BT → BT → Set where
     reflS : S ⊑ S
     reflD : D ⊑ D
     S≤D  :  S ⊑ D

   -----
   --wft
   -----
   data wft  : AType → Set where
     wf-int  : ∀ {a : BT} → wft (an a BInt)
     wf-fun  : ∀ {a : BT} {α₁ α₂ : AType} → wft α₁ → wft α₂
               → a ⊑ btof α₁ → a ⊑ btof α₂ → wft (an a (BFun α₁ α₂))
     wf-pair : ∀ {a : BT} {α₁ α₂ : AType} → wft α₁ → wft α₂
               → a ⊑ btof α₁ → a ⊑ btof α₂ → wft (an a (α₁ • α₂))
     wf-sum  : ∀ {a : BT} {α₁ α₂ : AType} → wft α₁ → wft α₂
               → a ⊑ btof α₁ → a ⊑ btof α₂ → wft (an a (α₁ ⊎ α₂))

   ----------
   --Liftable
   ----------
   -----------------------------------------------------------------
   --Note
   --• liftable defines a subset of annotated expressions whose type
   --  annotation can be "lifted" to "D"
   --• liftable dynamic types are trivially lifted
   --• assume that we only consider the set of well-formed types
   -----------------------------------------------------------------
   mutual
     data Liftable : AType → Set where
       --dynamic type can be trivially lifted
       D-aty  : ∀ {σ} → Liftable (an D σ)
       --static integer can be lifted to a dynamic one
       --same holds for static pair and sum
       S-int  : Liftable (an S BInt)
       S-pair : ∀ {α₁ α₂} → Liftable α₁ → Liftable α₂
                          → Liftable (an S (α₁ • α₂))
       S-sum  : ∀ {α₁ α₂} → Liftable α₁ → Liftable α₂
                          → Liftable (an S (α₁ ⊎ α₂))
       --a liftable static functional type must have
       --1. dynamic value as input
       --2. higher-order static value with dynamic output
       --3. higher-order static value as input with no
       --   static inputs
       S-fun  : ∀ {α₁ α₂} → Liftable⁻ α₁ → Liftable α₂
                          → Liftable (an S (BFun α₁ α₂))
     data Liftable⁻ : AType → Set where
       D-aty  : ∀ {σ} → Liftable⁻ (an D σ)
       S-pair : ∀ {α₁ α₂} → Liftable⁻ α₁ → Liftable⁻ α₂
                          → Liftable⁻ (an S (α₁ • α₂))
       S-fun  : ∀ {α₁ α₂} → Liftable α₁ → Liftable⁻ α₂
                          → Liftable⁻ (an S (BFun α₁ α₂))

   data liftable : AType → Set where
     ↑ : ∀ {α} → wft α → Liftable α → liftable α
   ----------------------------
   --typed annotated expression
   ----------------------------
   ----------------------------------------------------
   --Note
   --constructor name begins with an "A" for "annotated"
   --typing constructor as [AExp]
   --typing context as [Δ]
   --"a" for both expression and type annotation
   --"α" for [AType]
   --"σ" for [BType]
   ----------------------------------------------------
   data AExp (Δ : ACtx) : AType → Set where
     Var   : ∀ {α} → α ∈ Δ → AExp Δ α
     AInt  : (a : BT) → ℕ → AExp Δ (an a BInt)
     AAdd  : (a : BT) → AExp Δ (an a BInt) → AExp Δ (an a BInt) → AExp Δ (an a BInt)
     ALam  : ∀ {α₁ α₂} → (a : BT) → wft (an a (BFun α₁ α₂)) → AExp (α₁ ∷ Δ) α₂
                       → AExp Δ (an a (BFun α₁ α₂))
     AApp  : ∀ {α₁ α₂} → (a : BT) → wft (an a (BFun α₁ α₂)) → AExp Δ (an a (BFun α₁ α₂))
                       → AExp Δ α₁ → AExp Δ α₂
     APair : ∀ {α₁ α₂} → (a : BT) → wft (an a (α₁ • α₂))  → AExp Δ α₁ → AExp Δ α₂
                       → AExp Δ (an a (α₁ • α₂))
     ATl   : ∀ {α₁ α₂} → (a : BT) → wft (an a (α₁ ⊎ α₂))  → AExp Δ α₁
                       → AExp Δ (an a (α₁ ⊎ α₂))
     ATr   : ∀ {α₁ α₂} → (a : BT) → wft (an a (α₁ ⊎ α₂))  → AExp Δ α₂
                       → AExp Δ (an a (α₁ ⊎ α₂))
     ACase : ∀ {α₁ α₂ α₃} {a : BT} → a ⊑ btof α₃ → AExp Δ (an a (α₁ ⊎ α₂)) → AExp (α₁ ∷ Δ) α₃
                       → AExp (α₂ ∷ Δ) α₃ → AExp Δ α₃
     Lift  : ∀ {a} {σ} → liftable (an a σ) → AExp Δ (an a σ) → AExp Δ (an D σ)

   module two-level-representation where
   ---------------
   --residual type
   ---------------
   data type : Set where
     Int : type
     Fun : type → type → type
     _•_ : type → type → type
     _⊎_ : type → type → type

   ----------------
   --annotated type
   ----------------
   ---------------------------------------------
   --Note
   --• static type constructor starting with "S"
   --  except for pair and sum
   --• residual type used for building dynamic
   --  type
   ---------------------------------------------
   data atype : Set where
    SInt  : atype
    SFun  : atype → atype → atype
    D     : type  → atype
    _•_   : atype → atype → atype
    _⊎_   : atype → atype → atype

   btof-γ : atype → BT
   btof-γ SInt = S
   btof-γ (SFun γ γ₁) = S
   btof-γ (D x) = D
   btof-γ (γ • γ₁) = S
   btof-γ (γ ⊎ γ₁) = S

   actx = List atype

   ----------
   --Liftable
   ----------
   --Note
   --"τ" for residual type [type]
   --"γ" for [atype]
   mutual
     data Liftok : atype → Set where
       D-aty  : ∀ τ → Liftok (D τ)
       S-int  : Liftok SInt
       S-sum  : ∀ {γ₁ γ₂} → Liftok γ₁ → Liftok γ₂ → Liftok (γ₁ ⊎ γ₂)
       S-pair : ∀ {γ₁ γ₂} → Liftok γ₁ → Liftok γ₂ → Liftok (γ₁ • γ₂)
       S-fun  : ∀ {γ₁ γ₂} → Liftok⁻ γ₁ → Liftok γ₂ → Liftok (SFun γ₁ γ₂)

     data Liftok⁻ : atype → Set where
       D-aty : ∀ τ → Liftok⁻ (D τ)
       _•_   : ∀ {γ₁ γ₂} → Liftok⁻ γ₁ → Liftok⁻ γ₂ → Liftok⁻ (γ₁ • γ₂)
       S-fun : ∀ {γ₁ γ₂} → Liftok γ₁ → Liftok⁻ γ₂ → Liftok⁻ (SFun γ₁ γ₂)

   ----------------------------
   --typed two-level annotated expression
   ----------------------------
   --------------------
   --auxiliary function
   --------------------
   typeof : atype → type
   typeof SInt = Int
   typeof (SFun γ₁ γ₂) = Fun (typeof γ₁) (typeof γ₂)
   typeof (D τ) = τ
   typeof (γ₁ • γ₂) = typeof γ₁ • typeof γ₂
   typeof (γ₁ ⊎ γ₂) = typeof γ₁ ⊎ typeof γ₂

   --------
   --[aexp]
   --------
   --Note
   --• "γ" for [atype]
   --• "τ" for [type]
   --• typed terms starting with "S" for "static"
   --  and "D" for "dynamic",except for pair
   --• "Ω" for typing context
   data aexp (Ω : actx) : atype → Set where
     Var    : ∀ {γ} → γ ∈ Ω → aexp Ω γ
     SInt   : ℕ → aexp Ω SInt
     SAdd   : aexp Ω SInt → aexp Ω SInt → aexp Ω SInt
     SLam   : ∀ {γ₁ γ₂}   → aexp (γ₁ ∷ Ω) γ₂ → aexp Ω (SFun γ₁ γ₂)
     SApp   : ∀ {γ₁ γ₂}   → aexp Ω (SFun γ₁ γ₂) → aexp Ω γ₁ → aexp Ω γ₂
     DInt   : ℕ → aexp Ω (D Int)
     DAdd   : aexp Ω (D Int) → aexp Ω (D Int) → aexp Ω (D Int)
     DLam   : ∀ {τ₁ τ₂}   → aexp ((D τ₁) ∷ Ω) (D τ₂) → aexp Ω (D (Fun τ₁ τ₂))
     DApp   : ∀ {τ₁ τ₂}   → aexp Ω (D (Fun τ₁ τ₂)) → aexp Ω (D τ₁) → aexp Ω (D τ₂)
  -- Static pairs and sums
     _,_    : ∀ {γ₁ γ₂} → aexp Ω γ₁ → aexp Ω γ₂ → aexp Ω (γ₁ • γ₂)
     STl    : ∀ {γ₁ γ₂} → aexp Ω γ₁ → aexp Ω (γ₁ ⊎ γ₂)
     STr    : ∀ {γ₁ γ₂} → aexp Ω γ₂ → aexp Ω (γ₁ ⊎ γ₂)
     SFst   : ∀ {γ₁ γ₂} → aexp Ω (γ₁ • γ₂) → aexp Ω γ₁
     SSnd   : ∀ {γ₁ γ₂} → aexp Ω (γ₁ • γ₂) → aexp Ω γ₂
     SCase  : ∀ {γ₁ γ₂ γ₃} → aexp Ω (γ₁ ⊎ γ₂) → aexp (γ₁ ∷ Ω) γ₃ → aexp (γ₂ ∷ Ω) γ₃ → aexp Ω γ₃
  -- Dynamic pairs and sums
     _ḋ_    : ∀ {τ₁ τ₂} → aexp Ω (D τ₁) → aexp Ω (D τ₂) → aexp Ω (D (τ₁ • τ₂))
     DTl    : ∀ {τ₁ τ₂} → aexp Ω (D τ₁) → aexp Ω (D (τ₁ ⊎ τ₂))
     DTr    : ∀ {τ₁ τ₂} → aexp Ω (D τ₂) → aexp Ω (D (τ₁ ⊎ τ₂))
     DFst   : ∀ {τ₁ τ₂} → aexp Ω (D (τ₁ • τ₂)) → aexp Ω (D τ₁)
     DSnd   : ∀ {τ₁ τ₂} → aexp Ω (D (τ₁ • τ₂)) → aexp Ω (D τ₂)
     DCase  : ∀ {τ₁ τ₂ τ₃} → aexp Ω (D (τ₁ ⊎ τ₂)) → aexp ((D τ₁) ∷ Ω) (D τ₃) → aexp ((D τ₂) ∷ Ω) (D τ₃) → aexp Ω (D τ₃)
  -- Liftable static terms
     Lift   : ∀ {γ} → Liftok γ → aexp Ω γ  → aexp Ω (D (typeof γ))

   ---------------------------------------------------------------
   --Isomorphism between terms typed by [AExp] and terms by [aexp]
   ---------------------------------------------------------------
   module isomorphism where
   open import Data.Product
   open import Relation.Binary.PropositionalEquality
   ----------
   --Analysis
   ----------
   --consider static integer in [aexp],
   --SInt 0 : aexp Ω SInt,∀ Ω
   --naturally its counter-part in [AExp] should be,
   --AInt S 0 : AExp Δ (an S BInt)

   --for dynamic integer,
   --DInt 0 : aexp Ω (D Int)
   --AInt D 0 : aexp Δ (an D BInt)

   --Notice the two kinds of isomorphisms involved in above example
   --a. isomorphism w.r.t. types
   --b. isomorphism w.r.t. typed terms

   ---------------------
   --a. type isomorphism
   ---------------------

   --a.1. [atype] to [AType]
   --integer
   --SInt ==> an S BInt
   --D Int ==> an D BInt
   --function
   --SFun (D Int)(D Int) ==> an S (BFun (an D BInt) (an D BInt))
   --D (Fun Int Int) ==> an D (BFun (an D BInt) (an D BInt))

   ------------------------------------
   --projection from [atype] to [AType]
   ------------------------------------
   projT₁ : atype → AType
   projT₁ SInt = an S BInt
   projT₁ (SFun aty aty₁) = an S (BFun (projT₁ aty) (projT₁ aty₁))
   projT₁ (D Int) = an D BInt
   projT₁ (D (Fun x x₁)) = an D (BFun (projT₁ (D x)) (projT₁ (D x₁)))
   projT₁ (D (x • x₁)) = an D (projT₁ (D x) • projT₁ (D x₁))
   projT₁ (D (x ⊎ x₁)) = an D (projT₁ (D x) ⊎ projT₁ (D x₁))
   projT₁ (aty • aty₁) = an S ((projT₁ aty) • projT₁ aty₁)
   projT₁ (aty ⊎ aty₁) = an S ((projT₁ aty) ⊎ projT₁ aty₁)

   --a.2. [AType] to [atype]
   --imposing [wft] upon types defined in [AType] before projection
   --consider the following type,
   --an D (BFun (an S BInt) (an S BInt)) which has no counter part
   --in [atype] for the following lemma,
   --                ∀ γ, wft (projT₁ γ)
   --suppose we focus on these types satisfying [wft],
   --integer
   --an S BInt ==> SInt
   --an D BInt ==> D Int
   --function
   --an S BFun (an D BInt) (an D BInt) ==> SFun (D Int) (D Int)
   --an D BFun (an D BInt) (an D BInt) ==> D (Fun Int Int)

   ------------------------------------------------
   --projection from well-formed [AType] to [atype]
   ------------------------------------------------
   --------
   --helper
   --------
   ------------------------
   --from [atype] to [type]
   ------------------------
   γ→τ : atype → type
   γ→τ SInt = Int
   γ→τ (SFun aty aty₁) = Fun (γ→τ aty) (γ→τ aty₁)
   γ→τ (D x) = x
   γ→τ (aty • aty₁) = (γ→τ aty) • (γ→τ aty₁)
   γ→τ (aty ⊎ aty₁) = (γ→τ aty) ⊎ (γ→τ aty₁)

   projT₂ : (α : AType) → wft α → atype
   projT₂ .(an S BInt) (wf-int {S}) = SInt
   projT₂ .(an D BInt) (wf-int {D}) = D Int
   projT₂ .(an S (BFun α₁ α₂)) (wf-fun {S} {α₁} {α₂} wft wft₁ x x₁) = SFun (projT₂ α₁ wft) (projT₂ α₂ wft₁)
   projT₂ .(an D (BFun α₁ α₂)) (wf-fun {D} {α₁} {α₂} wft wft₁ x x₁) = D (Fun (γ→τ (projT₂ α₁ wft)) (γ→τ (projT₂ α₂ wft₁)))
   projT₂ .(an S (α₁ • α₂)) (wf-pair {S} {α₁} {α₂} wft wft₁ x x₁) = (projT₂ α₁ wft) • (projT₂ α₂ wft₁)
   projT₂ .(an D (α₁ • α₂)) (wf-pair {D} {α₁} {α₂} wft wft₁ x x₁) = D (γ→τ (projT₂ α₁ wft) • γ→τ (projT₂ α₂ wft₁))
   projT₂ .(an S (α₁ ⊎ α₂)) (wf-sum {S} {α₁} {α₂} wft wft₁ x x₁) = (projT₂ α₁ wft) ⊎ (projT₂ α₂ wft₁)
   projT₂ .(an D (α₁ ⊎ α₂)) (wf-sum {D} {α₁} {α₂} wft wft₁ x x₁) = D (γ→τ (projT₂ α₁ wft) ⊎ γ→τ (projT₂ α₂ wft₁))

   -------------------------------------
   --lemmas w.r.t. isomorphism of types
   -------------------------------------
   -----------------------------------------------
   --direction one:"starting from type in [atype]"
   -----------------------------------------------
   -----------------------
   --some auxiliary lemmas
   -----------------------
   S⊑* : ∀ {α} → S ⊑ btof α
   S⊑* {an S x₁} = reflS
   S⊑* {an D x₁} = S≤D

   a-pDatype : ∀ {τ : type} → btof (projT₁ (D τ)) ≡ D
   a-pDatype {Int} = refl
   a-pDatype {Fun τ τ₁} = refl
   a-pDatype {τ • τ₁} = refl
   a-pDatype {τ ⊎ τ₁} = refl

   D-a-pDatype : ∀ {τ : type} → D ⊑ (btof (projT₁ (D τ)))
   D-a-pDatype {τ} rewrite a-pDatype {τ} = reflD

   isoT₁ : ∀ (γ : atype) → Σ (wft (projT₁ γ)) \ x → γ ≡ projT₂ (projT₁ γ) x
   isoT₁ SInt = wf-int , refl
   isoT₁ (SFun γ γ₁)  with (proj₂ (isoT₁ γ)) | (proj₂ (isoT₁ γ₁))
   ... | I | I' = wf-fun (proj₁ (isoT₁ γ)) (proj₁ (isoT₁ γ₁)) (S⊑* {(projT₁ γ)}) (S⊑* {projT₁ γ₁}) , cong₂ SFun I I'
   isoT₁ (D Int) = wf-int , refl
   isoT₁ (D (Fun x x₁)) = wf-fun (proj₁ (isoT₁ (D x))) (proj₁ (isoT₁ (D x₁))) (D-a-pDatype {x}) (D-a-pDatype {x₁}) ,
                                  cong
                                    D
                                  (cong₂ Fun (cong γ→τ (proj₂ (isoT₁ (D x))))
                                  (cong γ→τ (proj₂ (isoT₁ (D x₁)))))
   isoT₁ (D (x • x₁)) = wf-pair (proj₁ (isoT₁ (D x))) (proj₁ (isoT₁ (D x₁))) (D-a-pDatype {x}) (D-a-pDatype {x₁}) ,
                                  cong
                                    D
                                  (cong₂ _•_ (cong γ→τ (proj₂ (isoT₁ (D x))))
                                  (cong γ→τ (proj₂ (isoT₁ (D x₁)))))
   isoT₁ (D (x ⊎ x₁)) = wf-sum (proj₁ (isoT₁ (D x))) (proj₁ (isoT₁ (D x₁))) (D-a-pDatype {x}) (D-a-pDatype {x₁}) ,
                                  cong
                                    D
                                  (cong₂ _⊎_ (cong γ→τ (proj₂ (isoT₁ (D x))))
                                  (cong γ→τ (proj₂ (isoT₁ (D x₁)))))
   isoT₁ (γ • γ₁) = wf-pair (proj₁ (isoT₁ γ)) (proj₁ (isoT₁ γ₁)) (S⊑* {projT₁ γ}) (S⊑* {projT₁ γ₁}) ,
                             cong₂ _•_ (proj₂ (isoT₁ γ)) (proj₂ (isoT₁ γ₁))
   isoT₁ (γ ⊎ γ₁) = wf-sum (proj₁ (isoT₁ γ)) (proj₁ (isoT₁ γ₁)) (S⊑* {projT₁ γ}) (S⊑* {projT₁ γ₁}) ,
                             cong₂ _⊎_ (proj₂ (isoT₁ γ)) (proj₂ (isoT₁ γ₁))

   -----------------------------------------------------------
   --direction two:"starting from type in well-formed [AType]"
   -----------------------------------------------------------
   -----------------------
   --some auxiliary lemmas
   -----------------------
   eqDγ→τprojT₂ : ∀ {α : AType} {wf : wft α} → D ⊑ btof α → D (γ→τ (projT₂ α wf)) ≡ projT₂ α wf
   eqDγ→τprojT₂ {an S BInt} {wf-int} ()
   eqDγ→τprojT₂ {an D BInt} {wf-int} e = refl
   eqDγ→τprojT₂ {an S (BFun α₁ α₂)} {wf-fun wf wf₁ x x₁} ()
   eqDγ→τprojT₂ {an D (BFun α₁ α₂)} {wf-fun wf wf₁ x x₁} e = refl
   eqDγ→τprojT₂ {an S (α₁ • α₂)} {wf-pair wf wf₁ x x₁} ()
   eqDγ→τprojT₂ {an D (α₁ • α₂)} {wf-pair wf wf₁ x x₁} e = refl
   eqDγ→τprojT₂ {an S (α₁ ⊎ α₂)} {wf-sum wf wf₁ x x₁} ()
   eqDγ→τprojT₂ {an D (α₁ ⊎ α₂)} {wf-sum wf wf₁ x x₁} e = refl

   isoT₂ : ∀ {α : AType} → (wf : wft α) → α ≡  projT₁ (projT₂ α wf)
   isoT₂ {an S BInt} wf-int = refl
   isoT₂ {an S (BFun x x₁)} (wf-fun wf wf₁ x₂ x₃) = cong₂ an refl (cong₂ BFun (isoT₂ {x} wf) (isoT₂ {x₁} wf₁))
   isoT₂ {an S (x • x₁)} (wf-pair wf wf₁ x₂ x₃) = cong₂ an refl (cong₂ _•_ (isoT₂ {x} wf) (isoT₂ {x₁} wf₁))
   isoT₂ {an S (x ⊎ x₁)} (wf-sum wf wf₁ x₂ x₃) = cong₂ an refl (cong₂ _⊎_ (isoT₂ {x} wf) (isoT₂ {x₁} wf₁))
   isoT₂ {an D BInt} wf-int = refl
   isoT₂ {an D (BFun x x₁)} (wf-fun wf wf₁ x₂ x₃) =
       cong₂ an refl
         (cong₂ BFun
          (trans (isoT₂ {x} wf)
           (sym (cong projT₁ (eqDγ→τprojT₂ {x} {wf} x₂))))
          (trans (isoT₂ {x₁} wf₁)
           (sym (cong projT₁ (eqDγ→τprojT₂ {x₁} {wf₁} x₃)))))
   isoT₂ {an D (x • x₁)} (wf-pair wf wf₁ x₂ x₃) =
         cong₂ an refl
           (cong₂ _•_
            (trans (isoT₂ {x} wf)
             (sym (cong projT₁ (eqDγ→τprojT₂ {x} {wf} x₂))))
            (trans (isoT₂ {x₁} wf₁)
             (sym (cong projT₁ (eqDγ→τprojT₂ {x₁} {wf₁} x₃)))))
   isoT₂ {an D (x ⊎ x₁)} (wf-sum wf wf₁ x₂ x₃) =
         cong₂ an refl
           (cong₂ _⊎_
            (trans (isoT₂ {x} wf)
             (sym (cong projT₁ (eqDγ→τprojT₂ {x} {wf} x₂))))
            (trans (isoT₂ {x₁} wf₁)
             (sym (cong projT₁ (eqDγ→τprojT₂ {x₁} {wf₁} x₃)))))

   ------------------------------------------------
   --lemmas w.r.t. isomorphism of typed expressions
   ------------------------------------------------
   ----------------
   --some instances
   ----------------
   ------------------
   --[AExp] to [aexp]
   ------------------
   --Var hd : AExp [an D (BFun (an D BInt) (an D BInt))]
   --               (an D (BFun (an D BInt) (an D BInt)))
   --==>projt₂*
   --Var hd : aexp [D (Fun Int Int)] (D (Fun Int Int))
   --*Note that projection from expression in [AExp] to
   -- that in [aexp] requires that both the type and the
   -- typing environment are well-formed

   --AInt S 0 : AExp Δ (an S BInt),∀ Δ
   --==>projt₂
   --SInt 0 : aexp Ω* SInt,∀ Ω
   --*Note that the corresponding typing environment in [aexp] satisfies,
   -- Ω = projection of Δ

   --ALam S (wf-fun wf-int wf-int *≤D *≤D) (Var hd)
   --:AExp [] (an S (BFun (an D BInt) (an D BInt)))
   --==>projt₂
   --SLam (Var hd) : aexp [] (SFun (D Int) (D Int))
   --ALam D (wf-fun wf-int wf-int refl refl) (Var hd)
   --:AExp [] (an D (BFun (an D BInt) (an D BInt)))
   --==>projt₂
   --DLam (Var hd) : aexp [] (D (Fun Int Int))

   -----------------------
   --summary upon [projt₂]
   -----------------------
   --• projection only of terms which are typed both by
   --  well-formed [AType] and under well-formed Δ
   --• the results are typed under Ω which is the projection
   --  of Δ
   ------------------------------------------
   --some auxiliary functions and definitions
   ------------------------------------------
   ---------------
   --Well-formed Δ
   ---------------
   data wfe : ACtx → Set where
     wf-[]  : wfe []
     wf-∷   : ∀ {α : AType} {AEnv : ACtx}
                 → wft α → wfe AEnv
                 → wfe (α ∷ AEnv)

   -----------------------------
   --projΔ (similar to [projT₂])
   -----------------------------
   projΔ : (Δ : ACtx) → wfe Δ → actx
   projΔ [] wfe = []
   projΔ (x ∷ Δ) (wf-∷ x₁ wfe) = projT₂ x x₁ ∷ projΔ Δ wfe

   --------
   --projt₂
   --------
   -----------------------
   --some auxiliary lemmas
   -----------------------
   -- --------
   -- --is-≡-α
   -- --------
   -- is-≡-α : (α₁ α₂ : AType) → Bool
   -- is-≡-α (an S BInt) (an S BInt) = true
   -- is-≡-α (an S BInt) (an S (BFun x x₁)) = false
   -- is-≡-α (an S BInt) (an S (x • x₁)) = false
   -- is-≡-α (an S BInt) (an S (x ⊎ x₁)) = false
   -- is-≡-α (an S (BFun x x₁)) (an S BInt) = false
   -- is-≡-α (an S (BFun x x₁)) (an S (BFun x₂ x₃)) = is-≡-α x x₂ ∧ is-≡-α x₁ x₃
   -- is-≡-α (an S (BFun x x₁)) (an S (x₂ • x₃)) = false
   -- is-≡-α (an S (BFun x x₁)) (an S (x₂ ⊎ x₃)) = false
   -- is-≡-α (an S (x • x₁)) (an S BInt) = false
   -- is-≡-α (an S (x • x₁)) (an S (BFun x₂ x₃)) = false
   -- is-≡-α (an S (x • x₁)) (an S (x₂ • x₃)) = is-≡-α x x₂ ∧ is-≡-α x₁ x₃
   -- is-≡-α (an S (x • x₁)) (an S (x₂ ⊎ x₃)) = false
   -- is-≡-α (an S (x ⊎ x₁)) (an S BInt) = false
   -- is-≡-α (an S (x ⊎ x₁)) (an S (BFun x₂ x₃)) = false
   -- is-≡-α (an S (x ⊎ x₁)) (an S (x₂ • x₃)) = false
   -- is-≡-α (an S (x ⊎ x₁)) (an S (x₂ ⊎ x₃)) = is-≡-α x x₂ ∧ is-≡-α x₁ x₃
   -- is-≡-α (an S x₁) (an D x₃) = false
   -- is-≡-α (an D x₁) (an S x₃) = false
   -- is-≡-α (an D BInt) (an D BInt) = true
   -- is-≡-α (an D BInt) (an D (BFun x x₁)) = false
   -- is-≡-α (an D BInt) (an D (x • x₁)) = false
   -- is-≡-α (an D BInt) (an D (x ⊎ x₁)) = false
   -- is-≡-α (an D (BFun x x₁)) (an D BInt) = false
   -- is-≡-α (an D (BFun x x₁)) (an D (BFun x₂ x₃)) = is-≡-α x x₂ ∧ is-≡-α x₁ x₃
   -- is-≡-α (an D (BFun x x₁)) (an D (x₂ • x₃)) = false
   -- is-≡-α (an D (BFun x x₁)) (an D (x₂ ⊎ x₃)) = false
   -- is-≡-α (an D (x • x₁)) (an D BInt) = false
   -- is-≡-α (an D (x • x₁)) (an D (BFun x₂ x₃)) = false
   -- is-≡-α (an D (x • x₁)) (an D (x₂ • x₃)) = is-≡-α x x₂ ∧ is-≡-α x₁ x₃
   -- is-≡-α (an D (x • x₁)) (an D (x₂ ⊎ x₃)) = false
   -- is-≡-α (an D (x ⊎ x₁)) (an D BInt) = false
   -- is-≡-α (an D (x ⊎ x₁)) (an D (BFun x₂ x₃)) = false
   -- is-≡-α (an D (x ⊎ x₁)) (an D (x₂ • x₃)) = false
   -- is-≡-α (an D (x ⊎ x₁)) (an D (x₂ ⊎ x₃)) = is-≡-α x x₂ ∧ is-≡-α x₁ x₃

   -- --------
   -- --is-≡-τ
   -- --------
   -- is-≡-τ : (τ₁ τ₂ : type) → Bool
   -- is-≡-τ Int Int = true
   -- is-≡-τ Int (Fun τ₂ τ₃) = false
   -- is-≡-τ Int (τ₂ • τ₃) = false
   -- is-≡-τ Int (τ₂ ⊎ τ₃) = false
   -- is-≡-τ (Fun τ₁ τ₂) Int = false
   -- is-≡-τ (Fun τ₁ τ₂) (Fun τ₃ τ₄) = is-≡-τ τ₁ τ₃ ∧ is-≡-τ τ₂ τ₄
   -- is-≡-τ (Fun τ₁ τ₂) (τ₃ • τ₄) = false
   -- is-≡-τ (Fun τ₁ τ₂) (τ₃ ⊎ τ₄) = false
   -- is-≡-τ (τ₁ • τ₂) Int = false
   -- is-≡-τ (τ₁ • τ₂) (Fun τ₃ τ₄) = false
   -- is-≡-τ (τ₁ • τ₂) (τ₃ • τ₄) = is-≡-τ τ₁ τ₃ ∧ is-≡-τ τ₂ τ₄
   -- is-≡-τ (τ₁ • τ₂) (τ₃ ⊎ τ₄) = false
   -- is-≡-τ (τ₁ ⊎ τ₂) Int = false
   -- is-≡-τ (τ₁ ⊎ τ₂) (Fun τ₃ τ₄) = false
   -- is-≡-τ (τ₁ ⊎ τ₂) (τ₃ • τ₄) = false
   -- is-≡-τ (τ₁ ⊎ τ₂) (τ₃ ⊎ τ₄) = is-≡-τ τ₁ τ₃ ∧ is-≡-τ τ₂ τ₄
   -- --------
   -- --is-≡-γ
   -- --------
   -- is-≡-γ : (γ₁ γ₂ : atype) → Bool
   -- is-≡-γ SInt SInt = true
   -- is-≡-γ SInt (SFun γ₂ γ₃) = false
   -- is-≡-γ SInt (D x) = false
   -- is-≡-γ SInt (γ₂ • γ₃) = false
   -- is-≡-γ SInt (γ₂ ⊎ γ₃) = false
   -- is-≡-γ (SFun γ₁ γ₂) SInt = false
   -- is-≡-γ (SFun γ₁ γ₂) (SFun γ₃ γ₄) = is-≡-γ γ₁ γ₃ ∧ is-≡-γ γ₂ γ₄
   -- is-≡-γ (SFun γ₁ γ₂) (D x) = false
   -- is-≡-γ (SFun γ₁ γ₂) (γ₃ • γ₄) = false
   -- is-≡-γ (SFun γ₁ γ₂) (γ₃ ⊎ γ₄) = false
   -- is-≡-γ (D x) SInt = false
   -- is-≡-γ (D x) (SFun γ₂ γ₃) = false
   -- is-≡-γ (D x) (D x₁) = is-≡-τ x x₁
   -- is-≡-γ (D x) (γ₂ • γ₃) = false
   -- is-≡-γ (D x) (γ₂ ⊎ γ₃) = false
   -- is-≡-γ (γ₁ • γ₂) SInt = false
   -- is-≡-γ (γ₁ • γ₂) (SFun γ₃ γ₄) = false
   -- is-≡-γ (γ₁ • γ₂) (D x) = false
   -- is-≡-γ (γ₁ • γ₂) (γ₃ • γ₄) = is-≡-γ γ₁ γ₃ ∧ is-≡-γ γ₂ γ₄
   -- is-≡-γ (γ₁ • γ₂) (γ₃ ⊎ γ₄) = false
   -- is-≡-γ (γ₁ ⊎ γ₂) SInt = false
   -- is-≡-γ (γ₁ ⊎ γ₂) (SFun γ₃ γ₄) = false
   -- is-≡-γ (γ₁ ⊎ γ₂) (D x) = false
   -- is-≡-γ (γ₁ ⊎ γ₂) (γ₃ • γ₄) = false
   -- is-≡-γ (γ₁ ⊎ γ₂) (γ₃ ⊎ γ₄) = is-≡-γ γ₁ γ₃ ∧ is-≡-γ γ₂ γ₄

   -- is-≡-γ→τ : {γ₁ γ₂ : atype} → btof-γ γ₁ ≡ D → btof-γ γ₁ ≡ btof-γ γ₂
   --             → is-≡-γ γ₁ γ₂ ≡ is-≡-τ (γ→τ γ₁) (γ→τ γ₂)
   -- is-≡-γ→τ {SInt} {SInt} eq eq' = refl
   -- is-≡-γ→τ {SInt} {SFun γ₂ γ₃} eq eq' = refl
   -- is-≡-γ→τ {SInt} {D x} () ()
   -- is-≡-γ→τ {SInt} {γ₂ • γ₃} () eq'
   -- is-≡-γ→τ {SInt} {γ₂ ⊎ γ₃} () eq'
   -- is-≡-γ→τ {SFun γ₁ γ₂} {SInt} () eq'
   -- is-≡-γ→τ {SFun γ₁ γ₂} {SFun γ₃ γ₄} () eq'
   -- is-≡-γ→τ {SFun γ₁ γ₂} {D x} () eq'
   -- is-≡-γ→τ {SFun γ₁ γ₂} {γ₃ • γ₄} () eq'
   -- is-≡-γ→τ {SFun γ₁ γ₂} {γ₃ ⊎ γ₄} () eq'
   -- is-≡-γ→τ {D x} {SInt} eq ()
   -- is-≡-γ→τ {D x} {SFun γ₂ γ₃} eq ()
   -- is-≡-γ→τ {D x} {D x₁} eq eq' = refl
   -- is-≡-γ→τ {D x} {γ₂ • γ₃} eq ()
   -- is-≡-γ→τ {D x} {γ₂ ⊎ γ₃} eq ()
   -- is-≡-γ→τ {γ₁ • γ₂} {SInt} eq eq' = refl
   -- is-≡-γ→τ {γ₁ • γ₂} {SFun γ₃ γ₄} () eq'
   -- is-≡-γ→τ {γ₁ • γ₂} {D x} eq ()
   -- is-≡-γ→τ {γ₁ • γ₂} {γ₃ • γ₄} () eq'
   -- is-≡-γ→τ {γ₁ • γ₂} {γ₃ ⊎ γ₄} () eq'
   -- is-≡-γ→τ {γ₁ ⊎ γ₂} {SInt} () eq'
   -- is-≡-γ→τ {γ₁ ⊎ γ₂} {SFun γ₃ γ₄} () eq'
   -- is-≡-γ→τ {γ₁ ⊎ γ₂} {D x} eq ()
   -- is-≡-γ→τ {γ₁ ⊎ γ₂} {γ₃ • γ₄} () eq'
   -- is-≡-γ→τ {γ₁ ⊎ γ₂} {γ₃ ⊎ γ₄} () eq'

   -- btof-γ-projT₂-α : ∀ {a : BT} {σ : BType} {wft : wft (an a σ)}
   --                     → btof-γ (projT₂ (an a σ) wft) ≡ a
   -- btof-γ-projT₂-α {S} {BInt} {wf-int} = refl
   -- btof-γ-projT₂-α {D} {BInt} {wf-int} = refl
   -- btof-γ-projT₂-α {S} {BFun α₁ α₂} {wf-fun wft wft₁ x x₁} = refl
   -- btof-γ-projT₂-α {D} {BFun α₁ α₂} {wf-fun wft wft₁ x x₁} = refl
   -- btof-γ-projT₂-α {S} {α₁ • α₂} {wf-pair wft wft₁ x x₁} = refl
   -- btof-γ-projT₂-α {D} {α₁ • α₂} {wf-pair wft wft₁ x x₁} = refl
   -- btof-γ-projT₂-α {S} {α₁ ⊎ α₂} {wf-sum wft wft₁ x x₁} = refl
   -- btof-γ-projT₂-α {D} {α₁ ⊎ α₂} {wf-sum wft wft₁ x x₁} = refl

   -- is-≡-projT₂ : {α₁ α₂ : AType} {wft₁ : wft α₁} {wft₂ : wft α₂}
   --                → (is-≡-α α₁ α₂) ≡ (is-≡-γ (projT₂ α₁ wft₁) (projT₂ α₂ wft₂))
   -- is-≡-projT₂ {an S BInt} {an S BInt} {wf-int} {wf-int} = refl
   -- is-≡-projT₂ {an S BInt} {an D BInt} {wf-int} {wf-int} = refl
   -- is-≡-projT₂ {an D BInt} {an S BInt} {wf-int} {wf-int} = refl
   -- is-≡-projT₂ {an D BInt} {an D BInt} {wf-int} {wf-int} = refl
   -- is-≡-projT₂ {an S BInt} {an S (BFun α₁ α₂)} {wf-int} {wf-fun wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an S BInt} {an D (BFun α₁ α₂)} {wf-int} {wf-fun wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an D BInt} {an S (BFun α₁ α₂)} {wf-int} {wf-fun wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an D BInt} {an D (BFun α₁ α₂)} {wf-int} {wf-fun wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an S BInt} {an S (α₁ • α₂)} {wf-int} {wf-pair wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an S BInt} {an D (α₁ • α₂)} {wf-int} {wf-pair wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an D BInt} {an S (α₁ • α₂)} {wf-int} {wf-pair wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an D BInt} {an D (α₁ • α₂)} {wf-int} {wf-pair wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an S BInt} {an S (α₁ ⊎ α₂)} {wf-int} {wf-sum wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an S BInt} {an D (α₁ ⊎ α₂)} {wf-int} {wf-sum wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an D BInt} {an S (α₁ ⊎ α₂)} {wf-int} {wf-sum wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an D BInt} {an D (α₁ ⊎ α₂)} {wf-int} {wf-sum wft₂ wft₃ x x₁} = refl
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an S BInt} {wf-fun wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an D BInt} {wf-fun wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an D (BFun α₁ α₃)} {an S BInt} {wf-fun wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an D (BFun α₁ α₃)} {an D BInt} {wf-fun wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an S (BFun α₂ α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃}
   --    rewrite (is-≡-projT₂ {α₁} {α₂} {wft₁} {wft₃}) | (is-≡-projT₂ {α₃} {α₄} {wft₂} {wft₄}) = refl
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an D (BFun α₂ α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (BFun α₁ α₃)} {an S (BFun α₂ α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (BFun (an D σ₁) (an D σ₃))} {an D (BFun (an D σ₂) (an D σ₄))} {wf-fun wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃}
   --    rewrite ((is-≡-projT₂ {an D σ₁} {an D σ₂} {wft₁} {wft₃})) | ((is-≡-projT₂ {an D σ₃} {an D σ₄} {wft₂} {wft₄}))
   --            | is-≡-γ→τ {projT₂ (an D σ₁) wft₁} {projT₂ (an D σ₂) wft₃}
   --              (btof-γ-projT₂-α {D} {σ₁} {wft₁}) (trans (btof-γ-projT₂-α {D} {σ₁} {wft₁}) (sym (btof-γ-projT₂-α {D} {σ₂} {wft₃})))
   --            | is-≡-γ→τ {projT₂ (an D σ₃) wft₂} {projT₂ (an D σ₄) wft₄}
   --              (btof-γ-projT₂-α {D} {σ₃} {wft₂}) (trans (btof-γ-projT₂-α {D} {σ₃} {wft₂}) (sym (btof-γ-projT₂-α {D} {σ₄} {wft₄})))
   --    = refl
   -- is-≡-projT₂ {an D (BFun (an D σ₁) (an D σ₃))} {an D (BFun (an D σ₂) (an S σ₄))} {wf-fun wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ ()}
   -- is-≡-projT₂ {an D (BFun (an D σ₁) (an S σ₃))} {an D (BFun (an D σ₂) (an a₄ σ₄))} {wf-fun wft₁ wft₂ x ()} {wf-fun wft₃ wft₄ x₂ x₃}
   -- is-≡-projT₂ {an D (BFun (an D σ₁) (an a₃ σ₃))} {an D (BFun (an S σ₂) (an a₄ σ₄))} {wf-fun wft₁ wft₂ x x₁}  {wf-fun wft₃ wft₄ () x₃}
   -- is-≡-projT₂ {an D (BFun (an S σ₁) (an a₃ σ₃))} {an D (BFun (an D σ₂) (an a₄ σ₄))} {wf-fun wft₁ wft₂ () x₁} {wf-fun wft₃ wft₄ x₂ x₃}
   -- is-≡-projT₂ {an D (BFun (an S σ₁) (an a₃ σ₃))} {an D (BFun (an S σ₂) (an a₄ σ₄))} {wf-fun wft₁ wft₂ () x₁} {wf-fun wft₃ wft₄ () x₃}
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an S (α₂ • α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an D (α₂ • α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (BFun α₁ α₃)} {an S (α₂ • α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (BFun α₁ α₃)} {an D (α₂ • α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an S (α₂ ⊎ α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-sum wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an S (BFun α₁ α₃)} {an D (α₂ ⊎ α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-sum wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (BFun α₁ α₃)} {an S (α₂ ⊎ α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-sum wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (BFun α₁ α₃)} {an D (α₂ ⊎ α₄)} {wf-fun wft₁ wft₂ x x₁} {wf-sum wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an S (α₁ • α₃)} {an S BInt} {wf-pair wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an S (α₁ • α₃)} {an D BInt} {wf-pair wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an D (α₁ • α₃)} {an S BInt} {wf-pair wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an D (α₁ • α₃)} {an D BInt} {wf-pair wft₁ wft₂ x x₁} {wf-int} = refl
   -- is-≡-projT₂ {an S (α₁ • α₃)} {an S (BFun α₂ α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an S (α₁ • α₃)} {an D (BFun α₂ α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (α₁ • α₃)} {an S (BFun α₂ α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (α₁ • α₃)} {an D (BFun α₂ α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-fun wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an S (α₁ • α₃)} {an S (α₂ • α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃}
   --   rewrite (is-≡-projT₂ {α₁} {α₂} {wft₁} {wft₃}) | (is-≡-projT₂ {α₃} {α₄} {wft₂} {wft₄})
   --   = refl
   -- is-≡-projT₂ {an S (α₁ • α₃)} {an D (α₂ • α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (α₁ • α₃)} {an S (α₂ • α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃} = refl
   -- is-≡-projT₂ {an D (α₁ • α₃)} {an D (α₂ • α₄)} {wf-pair wft₁ wft₂ x x₁} {wf-pair wft₃ wft₄ x₂ x₃} = {!!}
   -- is-≡-projT₂ {an a (α₁ • α₃)} {(an a₁ (α₂ ⊎ α₄))} {wf-pair wft₁ wft₂ x x₁} {wf-sum wft₃ wft₄ x₂ x₃} = {!!}
   -- is-≡-projT₂ {(an a (α₁ ⊎ α₃))} {α₂} {wf-sum wft₁ wft₂ x x₁} {wft'} = {!!}
   ⊑-≡ : ∀ {a b : BT} → (e : a ⊑ b) → (e' : a ⊑ b) → e ≡ e'
   ⊑-≡ {S} {S} reflS reflS = refl
   ⊑-≡ {S} {D} S≤D S≤D = refl
   ⊑-≡ {D} {S} () e'
   ⊑-≡ {D} {D} reflD reflD = refl

   wft-≡ : ∀ {α : AType} → (α₁ : wft α) → (α₂ : wft α) → α₁ ≡ α₂
   wft-≡ wf-int wf-int = refl
   wft-≡ (wf-fun wft₁ wft₂ x x₁) (wf-fun wft₃ wft₄ x₂ x₃) rewrite wft-≡ wft₁ wft₃ | wft-≡ wft₂ wft₄ | ⊑-≡ x x₂ | ⊑-≡ x₁ x₃
      = refl
   wft-≡ (wf-pair wft₁ wft₂ x x₁) (wf-pair wft₃ wft₄ x₂ x₃) rewrite wft-≡ wft₁ wft₃ | wft-≡ wft₂ wft₄ | ⊑-≡ x x₂ | ⊑-≡ x₁ x₃
      = refl
   wft-≡ (wf-sum wft₁ wft₂ x x₁) (wf-sum wft₃ wft₄ x₂ x₃) rewrite wft-≡ wft₁ wft₃ | wft-≡ wft₂ wft₄ | ⊑-≡ x x₂ | ⊑-≡ x₁ x₃
      = refl

   id-projT₂&Δ :  {α : AType} {Δ : ACtx}
                 → (wft : wft α) → (wfe : wfe Δ)
                 → (id : α ∈ Δ)
                 →   projT₂ α wft ∈ (projΔ Δ wfe)
   id-projT₂&Δ {α} {[]} wft wfe ()
   id-projT₂&Δ {.x} {x ∷ Δ} wft (wf-∷ x₁ wfe) hd rewrite wft-≡ x₁ wft = hd {x = projT₂ x wft} {xs = projΔ Δ wfe}
   id-projT₂&Δ {α} {x ∷ Δ} wft (wf-∷ x₁ wfe) (tl x₂) = tl (id-projT₂&Δ wft wfe x₂)

   αAExp→wft : ∀ {α : AType} {Δ : ACtx} → (e : AExp Δ α) → wft α
   αAExp→wft {α} {Δ} e = {!!}

   projt₂ : ∀ {α : AType} {Δ : ACtx} → (wft : wft α) → (wfe : wfe Δ)
              → AExp Δ α → aexp (projΔ Δ wfe) (projT₂ α wft)
   projt₂ {an x x₁} wft wfe (Var x₂) = Var (id-projT₂&Δ wft wfe x₂)
   projt₂ {an S BInt} wf-int wfe (AInt .S x₁) = SInt x₁
   projt₂ {an D BInt} wf-int wfe (AInt .D x₁) = DInt x₁
   projt₂ {an S BInt} wf-int wfe (AAdd .S e e₁) = SAdd (projt₂ wf-int wfe e) (projt₂ wf-int wfe e₁)
   projt₂ {an D BInt} wf-int wfe (AAdd .D e e₁) = DAdd (projt₂ wf-int wfe e) (projt₂ wf-int wfe e₁)
   projt₂ {an S (BFun α₁ α₂)} {Δ} (wf-fun wft wft₁ x x₁) wfe (ALam .S x₂ e) = SLam (projt₂ {α₂} {α₁ ∷ Δ} wft₁ (wf-∷ wft wfe) e)
   projt₂ {an D (BFun α₁ α₂)} {Δ} (wf-fun wft wft₁ x x₁) wfe (ALam .D x₂ e) =
    DLam myrewrite
       where myrewrite :  aexp (D (γ→τ (projT₂ α₁ wft)) ∷ projΔ Δ wfe) (D (γ→τ (projT₂ α₂ wft₁)))
             myrewrite rewrite (cong₂ aexp (cong₂  (_∷_) {D (γ→τ (projT₂ α₁ wft))} {projT₂ α₁ wft} {projΔ Δ wfe} {projΔ Δ wfe}
                               (eqDγ→τprojT₂ {α₁} {wft} x) refl) (eqDγ→τprojT₂ {α₂} {wft₁} x₁))
               = projt₂ {α₂} {α₁ ∷ Δ} wft₁ (wf-∷ wft wfe) e

   projt₂ {an x x₁} wft wfe (AApp {α₁} S (wf-fun x₂ x₃ x₄ x₅) e e₁) rewrite sym (wft-≡ x₃ wft)
     = SApp {γ₁ = (projT₂ α₁ x₂)} (projt₂ (wf-fun x₂ x₃ x₄ x₅) wfe e) (projt₂ x₂ wfe e₁)
   projt₂ {an S x₁} wft wfe (AApp D (wf-fun x₂ x₃ x ()) e e₁)
   projt₂ {an D x₁} wft wfe (AApp {an S x₂} D (wf-fun x₃ x₄ () x₅) e e₁)
   projt₂ {an D x₁} {Δ} wft wfe (AApp {an D x₂} D (wf-fun x₃ x₄ x x₅) e e₁)
     rewrite sym (wft-≡ x₄ wft)
       = myrewrite'
           where myrewrite' : aexp (projΔ Δ wfe) (projT₂ (an D x₁) x₄)
                 myrewrite' rewrite sym (cong₂ aexp {(projΔ Δ wfe)} {(projΔ Δ wfe)} refl (eqDγ→τprojT₂ {an D x₁} {x₄} x₅))
                       = DApp (projt₂ (wf-fun x₃ x₄ x x₅) wfe e) myrewrite
                                  where myrewrite : aexp (projΔ Δ wfe) (D (γ→τ (projT₂ (an D x₂) x₃)))
                                        myrewrite rewrite cong₂ aexp {(projΔ Δ wfe)} {(projΔ Δ wfe)} refl (eqDγ→τprojT₂ {an D x₂} {x₃} x)
                                            = projt₂ x₃ wfe e₁
   projt₂ {an S (α₁ • α₂)} (wf-pair wft wft₁ x x₁) wfe (APair .S x₂ e e₁) = projt₂ wft wfe e , projt₂ wft₁ wfe e₁
   projt₂ {an D (α₁ • α₂)} {Δ} (wf-pair wft wft₁ x x₁) wfe (APair .D x₂ e e₁)
     = myrewrite1 ḋ myrewrite2
          where myrewrite1 : aexp (projΔ Δ wfe) (D (γ→τ (projT₂ α₁ wft)))
                myrewrite1 rewrite cong₂ aexp {(projΔ Δ wfe)} {(projΔ Δ wfe)} refl (eqDγ→τprojT₂ {α₁} {wft} x)
                     =  projt₂ wft wfe e
                myrewrite2 : aexp (projΔ Δ wfe) (D (γ→τ (projT₂ α₂ wft₁)))
                myrewrite2 rewrite cong₂ aexp {(projΔ Δ wfe)} {(projΔ Δ wfe)} refl (eqDγ→τprojT₂ {α₂} {wft₁} x₁)
                     =  projt₂ wft₁ wfe e₁
   projt₂ {an S (α₁ ⊎ α₂)} (wf-sum wft wft₁ x x₁) wfe (ATl .S x₂ e) = STl (projt₂ wft wfe e)
   projt₂ {an D (α₁ ⊎ α₂)} {Δ} (wf-sum wft wft₁ x x₁) wfe (ATl .D x₂ e)
      = DTl myrewrite
           where myrewrite : aexp (projΔ Δ wfe) (D (γ→τ (projT₂ α₁ wft)))
                 myrewrite rewrite  cong₂ aexp {(projΔ Δ wfe)} {(projΔ Δ wfe)} refl (eqDγ→τprojT₂ {α₁} {wft} x)
                      = projt₂ wft wfe e
   projt₂ {an S (α₁ ⊎ α₂)} (wf-sum wft wft₁ x x₁) wfe (ATr .S x₂ e) = STr (projt₂ wft₁ wfe e)
   projt₂ {an D (α₁ ⊎ α₂)} {Δ} (wf-sum wft wft₁ x x₁) wfe (ATr .D x₂ e)
      = DTr myrewrite
           where myrewrite : aexp (projΔ Δ wfe) (D (γ→τ (projT₂ α₂ wft₁)))
                 myrewrite rewrite cong₂ aexp {(projΔ Δ wfe)} {(projΔ Δ wfe)} refl (eqDγ→τprojT₂ {α₂} {wft₁} x₁)
                   = projt₂ wft₁ wfe e
   projt₂ {an x x₁} wft wfe (ACase {α₁} {α₂} {.(an x x₁)} {S} x₂ e e₁ e₂) with  αAExp→wft e
   projt₂ {an x₂ x₃} wft wfe (ACase {α₁} {α₂} {.(an x₂ x₃)} {S} x₄ e e₁ e₂) | wf-sum WFT WFT₁ x x₁
      = SCase {γ₁ = projT₂ α₁ WFT} {γ₂ = projT₂ α₂ WFT₁}
          {γ₃ = projT₂ (an x₂ x₃) wft} (projt₂ (wf-sum WFT WFT₁ x x₁) wfe e) (projt₂ wft (wf-∷ WFT wfe) e₁) (projt₂ wft (wf-∷ WFT₁ wfe) e₂)
   projt₂ {an S x₁} wft wfe (ACase {α₁} {α₂} {.(an S x₁)} {D} () e e₁ e₂)
   projt₂ {an D x₁} wft wfe (ACase {α₁} {α₂} {.(an D x₁)} {D} x₂ e e₁ e₂) with αAExp→wft e
   projt₂ {an D x₂} {Δ} wft wfe (ACase {α₁} {α₂} {.(an D x₂)} {D} x₃ e e₁ e₂) | wf-sum WFT WFT₁ x x₁
     = myrewrite
         where myrewrite :  aexp (projΔ Δ wfe) (projT₂ (an D x₂) wft)
               myrewrite  rewrite sym (cong₂ aexp {(projΔ Δ wfe)} {(projΔ Δ wfe)} refl (eqDγ→τprojT₂ {an D x₂} {wft} x₃))
                = DCase (projt₂ (wf-sum WFT WFT₁ x x₁) wfe e) myrewrite1 myrewrite2
                       where myrewrite1 : aexp (D (γ→τ (projT₂ α₁ WFT)) ∷ projΔ Δ wfe) (D (γ→τ (projT₂ (an D x₂) wft)))
                             myrewrite1 rewrite (cong₂ aexp (cong₂  (_∷_) {D (γ→τ (projT₂ α₁ WFT))} {projT₂ α₁ WFT} {projΔ Δ wfe} {projΔ Δ wfe}
                                (eqDγ→τprojT₂ {α₁} {WFT} x) refl) (eqDγ→τprojT₂ {an D x₂} {wft} x₃))
                                  = projt₂ wft (wf-∷ WFT wfe) e₁
                             myrewrite2 : aexp (D (γ→τ (projT₂ α₂ WFT₁)) ∷ projΔ Δ wfe) (D (γ→τ (projT₂ (an D x₂) wft)))
                             myrewrite2 rewrite (cong₂ aexp (cong₂  (_∷_) {D (γ→τ (projT₂ α₂ WFT₁))} {projT₂ α₂ WFT₁} {projΔ Δ wfe} {projΔ Δ wfe}
                                (eqDγ→τprojT₂ {α₂} {WFT₁} x₁) refl) (eqDγ→τprojT₂ {an D x₂} {wft} x₃))
                                  = projt₂ wft (wf-∷ WFT₁ wfe) e₂

   projt₂ {an D x₁} wft wfe (Lift x e) = {!!}

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


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

open import Examples.Sorting.Sequential.Comparable

module Examples.Sorting.Sequential.MergeSort (M : Comparable) where

open Comparable M
open import Examples.Sorting.Sequential.Core M

open import Calf costMonoid
open import Calf.Types.Bool
open import Calf.Types.Nat
open import Calf.Types.List
open import Calf.Types.Eq
open import Calf.Types.Bounded costMonoid
open import Calf.Types.BigO costMonoid

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
open import Data.Product using (_×_; _,_; ∃)
open import Data.Sum using (inj₁; inj₂)
open import Function
open import Data.Nat as Nat using (ℕ; zero; suc; z≤n; s≤s; _+_; _*_; ⌊_/2⌋; ⌈_/2⌉)
import Data.Nat.Properties as N
open import Data.Nat.Square
open import Data.Nat.Log2

open import Examples.Sorting.Sequential.MergeSort.Split M public
open import Examples.Sorting.Sequential.MergeSort.Merge M public

sort/clocked : cmp (Π nat λ _ → Π (list A) λ _ → F (list A))
sort/clocked zero    l = ret l
sort/clocked (suc k) l =
  bind (F (list A)) (split l) λ (l₁ , l₂) →
    bind (F (list A)) (sort/clocked k l₁) λ l₁' →
      bind (F (list A)) (sort/clocked k l₂) λ l₂' →
        merge (l₁' , l₂')

sort/clocked/correct : ∀ k l → ⌈log₂ length l ⌉ Nat.≤ k → SortResult (sort/clocked k) l
sort/clocked/correct zero    l h u = l , refl , refl , short-sorted (⌈log₂n⌉≡0⇒n≤1 (N.n≤0⇒n≡0 h))
sort/clocked/correct (suc k) l h u =
  let (l₁ , l₂ , ≡ , length₁ , length₂ , ↭) = split/correct l u in
  let (l₁' , ≡₁ , ↭₁ , sorted₁) = sort/clocked/correct k l₁ (
                                    let open ≤-Reasoning in
                                    begin
                                      ⌈log₂ length l₁ ⌉
                                    ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩
                                      ⌈log₂ ⌊ length l /2⌋ ⌉
                                    ≤⟨ log₂-mono (N.⌊n/2⌋≤⌈n/2⌉ (length l)) ⟩
                                      ⌈log₂ ⌈ length l /2⌉ ⌉
                                    ≤⟨ log₂-suc (length l) h ⟩
                                      k
                                    ∎
                                  ) u in
  let (l₂' , ≡₂ , ↭₂ , sorted₂) = sort/clocked/correct k l₂ (
                                    let open ≤-Reasoning in
                                    begin
                                      ⌈log₂ length l₂ ⌉
                                    ≡⟨ Eq.cong ⌈log₂_⌉ length₂ ⟩
                                      ⌈log₂ ⌈ length l /2⌉ ⌉
                                    ≤⟨ log₂-suc (length l) h ⟩
                                      k
                                    ∎
                                  ) u in
  let (l' , ≡' , h-sorted) = merge/correct l₁' l₂' u
      (↭' , sorted) = h-sorted sorted₁ sorted₂
  in
  l' , (
    let open ≡-Reasoning in
    begin
      sort/clocked (suc k) l
    ≡⟨⟩
      (bind (F (list A)) (split l) λ (l₁ , l₂) →
        bind (F (list A)) (sort/clocked k l₁) λ l₁' →
          bind (F (list A)) (sort/clocked k l₂) λ l₂' →
            merge (l₁' , l₂'))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e _) ≡ ⟩
      (bind (F (list A)) (sort/clocked k l₁) λ l₁' →
        bind (F (list A)) (sort/clocked k l₂) λ l₂' →
          merge (l₁' , l₂'))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e λ l₁' → bind (F (list A)) (sort/clocked k l₂) _) ≡₁ ⟩
      (bind (F (list A)) (sort/clocked k l₂) λ l₂' →
        merge (l₁' , l₂'))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e λ l₂' → merge (l₁' , l₂')) ≡₂ ⟩
      merge (l₁' , l₂')
    ≡⟨ ≡' ⟩
      ret l'
    ∎
  ) , (
    let open PermutationReasoning in
    begin
      l
    ↭⟨ ↭ ⟩
      l₁ ++ l₂
    ↭⟨ ++⁺-↭ ↭₁ ↭₂ ⟩
      l₁' ++ l₂'
    ↭⟨ ↭' ⟩
      l'
    ∎
  ) , sorted

sort/clocked/cost : cmp (Π nat λ _ → Π (list A) λ _ → cost)
sort/clocked/cost zero    l = zero
sort/clocked/cost (suc k) l =
  bind cost (split l) λ (l₁ , l₂) → split/cost l +
    bind cost (sort/clocked k l₁) λ l₁' → sort/clocked/cost k l₁ +
      bind cost (sort/clocked k l₂) λ l₂' → sort/clocked/cost k l₂ +
        merge/cost/closed (l₁' , l₂')

sort/clocked/cost/closed : cmp (Π nat λ _ → Π (list A) λ _ → cost)
sort/clocked/cost/closed k l = k * length l

sort/clocked/cost≡sort/clocked/cost/closed : ∀ k l → ⌈log₂ length l ⌉ Nat.≤ k → ◯ (sort/clocked/cost k l ≡ sort/clocked/cost/closed k l)
sort/clocked/cost≡sort/clocked/cost/closed zero    l h u = refl
sort/clocked/cost≡sort/clocked/cost/closed (suc k) l h u =
  let (l₁ , l₂ , ≡ , length₁ , length₂ , ↭) = split/correct l u in
  let h₁ : ⌈log₂ length l₁ ⌉ Nat.≤ k
      h₁ =
        let open ≤-Reasoning in
        begin
          ⌈log₂ length l₁ ⌉
        ≡⟨ Eq.cong ⌈log₂_⌉ length₁ ⟩
          ⌈log₂ ⌊ length l /2⌋ ⌉
        ≤⟨ log₂-mono (N.⌊n/2⌋≤⌈n/2⌉ (length l)) ⟩
          ⌈log₂ ⌈ length l /2⌉ ⌉
        ≤⟨ log₂-suc (length l) h ⟩
          k
        ∎

      h₂ : ⌈log₂ length l₂ ⌉ Nat.≤ k
      h₂ =
        let open ≤-Reasoning in
        begin
          ⌈log₂ length l₂ ⌉
        ≡⟨ Eq.cong ⌈log₂_⌉ length₂ ⟩
          ⌈log₂ ⌈ length l /2⌉ ⌉
        ≤⟨ log₂-suc (length l) h ⟩
          k
        ∎
  in
  let (l₁' , ≡₁ , ↭₁ , sorted₁) = sort/clocked/correct k l₁ h₁ u in
  let (l₂' , ≡₂ , ↭₂ , sorted₂) = sort/clocked/correct k l₂ h₂ u in
  let open ≡-Reasoning in
  begin
    sort/clocked/cost (suc k) l
  ≡⟨⟩
    (bind cost (split l) λ (l₁ , l₂) → split/cost l +
      bind cost (sort/clocked k l₁) λ l₁' → sort/clocked/cost k l₁ +
        bind cost (sort/clocked k l₂) λ l₂' → sort/clocked/cost k l₂ +
          merge/cost/closed (l₁' , l₂'))
  ≡⟨ Eq.cong (λ e → bind cost e _) (≡) ⟩
    (split/cost l +
      bind cost (sort/clocked k l₁) λ l₁' → sort/clocked/cost k l₁ +
        bind cost (sort/clocked k l₂) λ l₂' → sort/clocked/cost k l₂ +
          merge/cost/closed (l₁' , l₂'))
  ≡⟨⟩
    (0 +
      bind cost (sort/clocked k l₁) λ l₁' → sort/clocked/cost k l₁ +
        bind cost (sort/clocked k l₂) λ l₂' → sort/clocked/cost k l₂ +
          merge/cost/closed (l₁' , l₂'))
  ≡⟨ N.+-identityˡ _ ⟩
    (bind cost (sort/clocked k l₁) λ l₁' → sort/clocked/cost k l₁ +
      bind cost (sort/clocked k l₂) λ l₂' → sort/clocked/cost k l₂ +
        merge/cost/closed (l₁' , l₂'))
  ≡⟨
    Eq.cong
      (λ e →
        bind cost e λ l₁' → sort/clocked/cost k l₁ +
          bind cost (sort/clocked k l₂) λ l₂' → sort/clocked/cost k l₂ +
            merge/cost/closed (l₁' , l₂'))
      ≡₁
  ⟩
    (sort/clocked/cost k l₁ +
      bind cost (sort/clocked k l₂) λ l₂' → sort/clocked/cost k l₂ +
        merge/cost/closed (l₁' , l₂'))
  ≡⟨
    Eq.cong
      (λ e →
        sort/clocked/cost k l₁ +
          bind cost e λ l₂' → sort/clocked/cost k l₂ +
            merge/cost/closed (l₁' , l₂'))
      ≡₂
  ⟩
    sort/clocked/cost k l₁ + (sort/clocked/cost k l₂ + merge/cost/closed (l₁' , l₂'))
  ≡˘⟨ N.+-assoc (sort/clocked/cost k l₁) (sort/clocked/cost k l₂) (merge/cost/closed (l₁' , l₂')) ⟩
    (sort/clocked/cost k l₁ + sort/clocked/cost k l₂) + merge/cost/closed (l₁' , l₂')
  ≡⟨
    Eq.cong (_+ merge/cost/closed (l₁' , l₂')) (
      Eq.cong₂ _+_
        (sort/clocked/cost≡sort/clocked/cost/closed k l₁ h₁ u)
        (sort/clocked/cost≡sort/clocked/cost/closed k l₂ h₂ u)
    )
  ⟩
    (sort/clocked/cost/closed k l₁ + sort/clocked/cost/closed k l₂) + merge/cost/closed (l₁' , l₂')
  ≡⟨⟩
    (sort/clocked/cost/closed k l₁ + sort/clocked/cost/closed k l₂) + (length l₁' + length l₂')
  ≡˘⟨
    Eq.cong ((sort/clocked/cost/closed k l₁ + sort/clocked/cost/closed k l₂) +_) (
      Eq.cong₂ _+_ (↭-length ↭₁) (↭-length ↭₂)
    )
  ⟩
    (sort/clocked/cost/closed k l₁ + sort/clocked/cost/closed k l₂) + (length l₁ + length l₂)
  ≡⟨⟩
    (k * length l₁ + k * length l₂) + (length l₁ + length l₂)
  ≡⟨
    Eq.cong₂
      (λ n₁ n₂ → k * n₁ + k * n₂ + (n₁ + n₂))
      length₁
      length₂
  ⟩
    (k * ⌊ length l /2⌋ + k * ⌈ length l /2⌉) + (⌊ length l /2⌋ + ⌈ length l /2⌉)
  ≡⟨ N.+-comm _ (⌊ length l /2⌋ + ⌈ length l /2⌉) ⟩
    (⌊ length l /2⌋ + ⌈ length l /2⌉) + (k * ⌊ length l /2⌋ + k * ⌈ length l /2⌉)
  ≡˘⟨ Eq.cong ((⌊ length l /2⌋ + ⌈ length l /2⌉) +_) (N.*-distribˡ-+ k _ _) ⟩
    (⌊ length l /2⌋ + ⌈ length l /2⌉) + k * (⌊ length l /2⌋ + ⌈ length l /2⌉)
  ≡⟨⟩
    suc k * (⌊ length l /2⌋ + ⌈ length l /2⌉)
  ≡⟨ Eq.cong (suc k *_) (N.⌊n/2⌋+⌈n/2⌉≡n (length l)) ⟩
    suc k * length l
  ∎

sort/clocked≤sort/clocked/cost : ∀ k l → IsBounded (list A) (sort/clocked k l) (sort/clocked/cost k l)
sort/clocked≤sort/clocked/cost zero l = bound/ret
sort/clocked≤sort/clocked/cost (suc k) l =
  bound/bind _ _ (split≤split/cost l) λ (l₁ , l₂) →
    bound/bind _ _ (sort/clocked≤sort/clocked/cost k l₁) λ l₁' →
      bound/bind _ _ (sort/clocked≤sort/clocked/cost k l₂) λ l₂' →
        merge≤merge/cost/closed (l₁' , l₂')

sort/clocked≤sort/clocked/cost/closed : ∀ k l → ⌈log₂ length l ⌉ Nat.≤ k → IsBounded (list A) (sort/clocked k l) (sort/clocked/cost/closed k l)
sort/clocked≤sort/clocked/cost/closed k l h = bound/relax (λ u → N.≤-reflexive (sort/clocked/cost≡sort/clocked/cost/closed k l h u)) (sort/clocked≤sort/clocked/cost k l)

sort/depth : cmp (Π (list A) λ _ → meta ℕ)
sort/depth l = ⌈log₂ length l ⌉

sort : cmp (Π (list A) λ _ → F (list A))
sort l = sort/clocked (sort/depth l) l

sort/correct : IsSort sort
sort/correct l = sort/clocked/correct (sort/depth l) l N.≤-refl

sort/cost : cmp (Π (list A) λ _ → cost)
sort/cost l = sort/clocked/cost (sort/depth l) l

sort/cost/closed : cmp (Π (list A) λ _ → cost)
sort/cost/closed l = sort/clocked/cost/closed (sort/depth l) l

sort≤sort/cost : ∀ l → IsBounded (list A) (sort l) (sort/cost l)
sort≤sort/cost l = sort/clocked≤sort/clocked/cost (sort/depth l) l

sort≤sort/cost/closed : ∀ l → IsBounded (list A) (sort l) (sort/cost/closed l)
sort≤sort/cost/closed l = sort/clocked≤sort/clocked/cost/closed (sort/depth l) l N.≤-refl

sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n * ⌈log₂ n ⌉)
sort/asymptotic = 0 ≤n⇒f[n]≤g[n]via λ l _ →
  bound/relax
    (λ u → ≤-reflexive (N.*-comm ⌈log₂ length l ⌉ (length l)))
    (sort≤sort/cost/closed l)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Data.Union.Relation.Binary.Subtype.Instances where

open import Data.List using (List)
open import Data.List.Relation.Binary.Subset.Propositional.Instances using (⦅_⊆_⦆; [_])

open import Data.Union using (Union)
open import Data.Union.Relation.Binary.Subtype
  using (_≼_; _,_⊢_≼_; refl; trans; generalize; function)

open import Level using (Level; _⊔_)

private
  variable
    a b c d f : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

    F : A → Set f
    ts ts′ : List A

-- ----------------------------------------------------------------------
-- Wrapped subtypes

infix 4 ⦅_≼_⦆ ⦅_,_⊢_≼_⦆

data ⦅_≼_⦆ {a b} : Set a → Set b → Set (a ⊔ b) where
  [_] : A ≼ B → ⦅ A ≼ B ⦆

⦅_,_⊢_≼_⦆ : (A : Set a) → (B : A → Set b) → List A → List A → Set (a ⊔ b)
⦅ A , B ⊢ ts ≼ ts′ ⦆ = ⦅ Union A B ts ≼ Union A B ts′ ⦆

proj : ⦅ A ≼ B ⦆ → A ≼ B
proj [ A≼B ] = A≼B

⊢proj : ⦅ A , F ⊢ ts ≼ ts′ ⦆ → A , F ⊢ ts ≼ ts′
⊢proj [ A,F⊢ts≼ts′ ] = A,F⊢ts≼ts′

-- ----------------------------------------------------------------------
-- Instances

instance
  ⦃refl⦄ : ⦅ A ≼ A ⦆
  ⦃refl⦄ = [ refl ]

  -- Removed since the transitivity of ⊆ provides this
  -- Also now allows for syntax directed instance search :)

  -- ⦃trans⦄ : ⦃ ⦅ A ≼ B ⦆ ⦄ → ⦃ ⦅ B ≼ C ⦆ ⦄ → ⦅ A ≼ C ⦆
  -- ⦃trans⦄ ⦃ [ A≼B ] ⦄ ⦃ [ B≼C ] ⦄ = [ trans A≼B B≼C ]

  ⦃generalize⦄ : ⦃ ⦅ ts ⊆ ts′ ⦆ ⦄ → ⦅ A , F ⊢ ts ≼ ts′ ⦆
  ⦃generalize⦄ ⦃ [ ts⊆ts′ ] ⦄ = [ generalize ts⊆ts′ ]

  ⦃function⦄ : ⦃ ⦅ C ≼ A ⦆ ⦄ → ⦃ ⦅ B ≼ D ⦆ ⦄ → ⦅ (A → B) ≼ (C → D) ⦆
  ⦃function⦄ ⦃ [ C≼A ] ⦄ ⦃ [ B≼D ] ⦄ = [ function C≼A B≼D ]

-- ----------------------------------------------------------------------
-- Coercion using instance search

⌊_⌋ : ⦃ ⦅ A ≼ B ⦆ ⦄ → A → B
⌊_⌋ ⦃ [ A≼B ] ⦄ A = A≼B A

max_stars_repo_name: johnyob/agda-union

max_issues_repo_name: johnyob/agda-union

max_forks_repo_name: johnyob/agda-union


text:
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ

postulate
  I  : Set
  U  : I → Set
  El : ∀ {i} → U i → Set
  Ctxt : Set
  Env  : Ctxt → Set

Type : Ctxt → Set
Type Γ = Σ I λ i → Env Γ → U i

Value : (Γ : Ctxt) → Type Γ → Set
Value Γ σ = (γ : Env Γ) → El (proj₂ σ γ)

_/id : ∀ {Γ} → Type Γ → Type Γ
(i , σ) /id = i , σ

data [Type] : Set where
  [_] : ∀ {Γ} → Type Γ → [Type]

_≅-Type_ : ∀ {Γ} (σ₁ σ₂ : Type Γ) → Set
σ₁ ≅-Type σ₂ = [ σ₁ ] ≡ [ σ₂ ]

data [Value] : Set where
  [_] : ∀ {Γ σ} → Value Γ σ → [Value]

_≅-Value_ : ∀ {Γ σ} (v₁ v₂ : Value Γ σ) → Set
v₁ ≅-Value v₂ = [Value].[ v₁ ] ≡ [ v₂ ]

Foo : ∀ {Γ} {σ₁ σ₂ : Type Γ} {v : Value Γ (σ₁ /id)} →
      σ₁ ≅-Type σ₂ → v ≅-Value v → Set₁
Foo refl refl = Set


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

module NewEquations where

open import Common.Prelude hiding (map; _++_)
open import Common.Equality

infixr 5 _++_

map : ∀ {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = (f x) ∷ (map f xs)

_++_ : ∀ {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

fold : ∀ {A B : Set} → (A → B → B) → B → List A → B
fold f v [] = v
fold f v (x ∷ xs) = f x (fold f v xs)

++-[] : ∀ {A} {xs : List A} → xs ++ [] ≡ xs
++-[] {xs = []} = refl
++-[] {xs = x ∷ xs} = cong (_∷_ x) ++-[]

++-assoc : ∀ {A} {xs ys zs : List A} → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc {xs = []} = refl
++-assoc {xs = x ∷ xs} = cong (_∷_ x) (++-assoc {xs = xs})

map-id : ∀ {A} {xs : List A} → map (λ x → x) xs ≡ xs
map-id {xs = []} = refl
map-id {xs = x ∷ xs} = cong (_∷_ x) map-id

map-fuse : ∀ {A B C} {f : B → C} {g : A → B} {xs : List A} → map f (map g xs) ≡ map (λ x → f (g x)) xs
map-fuse {xs = []} = refl
map-fuse {xs = x ∷ xs} = cong (_∷_ _) map-fuse

map-++ : ∀ {A B} {f : A → B} {xs ys : List A} → map f (xs ++ ys) ≡ (map f xs) ++ (map f ys)
map-++ {xs = []} = refl
map-++ {xs = x ∷ xs} = cong (_∷_ _) (map-++ {xs = xs})

fold-map : ∀ {A B C} {f : A → B} {c : B → C → C} {n : C} {xs : List A} →
           fold c n (map f xs) ≡ fold (λ x → c (f x)) n xs
fold-map {xs = []} = refl
fold-map {c = c} {xs = x ∷ xs} = cong (c _) (fold-map {xs = xs})

fold-++ : ∀ {A B} {c : A → B → B} {n : B} {xs ys : List A} →
          fold c n (xs ++ ys) ≡ fold c (fold c n ys) xs
fold-++ {xs = []} = refl
fold-++ {c = c} {xs = x ∷ xs} = cong (c _) (fold-++ {xs = xs})

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE ++-[] #-}
{-# REWRITE ++-assoc #-}
{-# REWRITE map-id #-}
{-# REWRITE map-fuse #-}
{-# REWRITE map-++ #-}
{-# REWRITE fold-map #-}
{-# REWRITE fold-++ #-}

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

swap : ∀ {A B} → A × B → B × A
swap (x , y) = y , x

test₁ : ∀ {A B} {xs : List (A × B)} → map swap (map swap xs) ≡ xs
test₁ = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

open import lib.Basics
open import lib.NType2
open import lib.NConnected
open import lib.types.Nat
open import lib.types.Subtype
open import lib.types.Truncation

-- classifying types of automorphism groups of types
module lib.types.BAut where

BAut : ∀ {i} → Type i → Type (lsucc i)
BAut {i} A = Σ (Type i) λ X → Trunc -1 (A == X)

BAut-prop : ∀ {i} (A : Type i) → SubtypeProp (Type i) (lsucc i)
BAut-prop A = ((λ X → Trunc -1 (A == X)) , (λ X → Trunc-level))

pBAut : ∀ {i} → Type i → Ptd (lsucc i)
de⊙ (pBAut A) = BAut A
pt (pBAut A) = A , [ idp ]

BAut-trunc-path : ∀ {i} (A X : Type i) → (tp : Trunc -1 (A == X))
                  → Trunc -1 ((A , [ idp ]) == (X , tp) :> BAut A)
BAut-trunc-path {i} A X = Trunc-elim λ p → [ pair= p prop-has-all-paths-↓ ]

BAut-conn : ∀ {i} (A : Type i) → is-connected 0 (BAut A)
fst (has-level-apply (BAut-conn A)) = [ pt (pBAut A) ]
snd (has-level-apply (BAut-conn A)) = Trunc-elim (λ { (X , tp) → <– (=ₜ-equiv [ A , [ idp ] ] [ X , tp ])
                                                                    (BAut-trunc-path A X tp) })

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --without-K #-}
module GroupoidStructure {a} {A : Set a} where

open import PathOperations
open import Types

p·p⁻¹ : {a b : A} (p : a ≡ b) → p · p ⁻¹ ≡ refl
p·p⁻¹ = J (λ _ _ p → p · p ⁻¹ ≡ refl) (λ _ → refl) _ _

p⁻¹·p : {a b : A} (p : a ≡ b) → p ⁻¹ · p ≡ refl
p⁻¹·p = J (λ _ _ p → p ⁻¹ · p ≡ refl) (λ _ → refl) _ _

p·id : {a b : A} (p : a ≡ b) → p · refl ≡ p
p·id = J (λ _ _ p → p · refl ≡ p) (λ _ → refl) _ _

id·p : {a b : A} (p : a ≡ b) → refl · p ≡ p
id·p _ = refl

p·q·r : {a b c d : A} (p : a ≡ b) (q : b ≡ c) (r : c ≡ d) →
  p · (q · r) ≡ (p · q) · r
p·q·r {c = c} {d = d} = J
  (λ _ b p → (q : b ≡ c) (r : c ≡ d) → p · q · r ≡ (p · q) · r)
  (λ b → J
    (λ _ c q → (r : c ≡ d) → refl · q · r ≡ (refl · q) · r)
    (λ _ _ → refl) _ _)
  _ _

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
------------------------------------------------------------------------
-- An example of how Abstract-binding-tree can be used
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module README.Abstract-binding-tree where

open import Dec
open import Equality.Path
open import Prelude as P hiding (swap; [_,_]; type-signature)

open import Abstract-binding-tree equality-with-paths
open import Bijection equality-with-J using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Equivalence equality-with-J using (_≃_)
open import Erased.Cubical equality-with-paths as E
open import Finite-subset.Listed equality-with-paths as L
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
import Nat equality-with-J as Nat

-- Sorts: expressions and statements.

Sort : Type
Sort = Bool

pattern expr = true
pattern stmt = false

-- Constructors: lambda, application and print.

data Constructor : @0 Sort → Type where
  exprᶜ : Bool → Constructor expr
  stmtᶜ : ⊤ → Constructor stmt

pattern lamᶜ   = exprᶜ true
pattern appᶜ   = exprᶜ false
pattern printᶜ = stmtᶜ tt

-- Erased equality of constructors is decidable.

_≟O_ : ∀ {@0 s} → Decidable-erased-equality (Constructor s)
exprᶜ x ≟O exprᶜ y = Dec-Erased-map
                       (record { to   = cong exprᶜ
                               ; from = cong (λ { (exprᶜ x) → x })
                               })
                       (Decidable-equality→Decidable-erased-equality
                          Bool._≟_ x y)
printᶜ  ≟O printᶜ  = yes [ refl ]

-- Variables are natural numbers.

Var : @0 Sort → Type
Var _ = ℕ

-- A signature.

sig : Signature lzero
sig .Signature.Sort          = Sort
sig .Signature.Op            = Constructor
sig .Signature.domain lamᶜ   = (expr ∷ [] , expr) ∷ []
sig .Signature.domain appᶜ   = ([] , expr) ∷ ([] , expr) ∷ []
sig .Signature.domain printᶜ = ([] , expr) ∷ []
sig .Signature.Var           = Var
sig .Signature._≟O_          = _≟O_
sig .Signature._≟S_          =
  Decidable-equality→Decidable-erased-equality Bool._≟_
sig .Signature._≟V_ =
  Decidable-equality→Decidable-erased-equality Nat._≟_
sig .Signature.fresh {s = s} xs =           $⟨ L.fresh (L.map proj₂ xs) ⟩
  (∃ λ n → n ∉ L.map proj₂ xs)              ↝⟨ Σ-map id [_]→ ⟩
  (∃ λ n → Erased (n ∉ L.map proj₂ xs))     ↝⟨ (∃-cong λ n → E.map (

      n ∉ L.map proj₂ xs                          ↔⟨ ¬-cong ext ∈map≃ ⟩
      ¬ ∥ (∃ λ x → x ∈ xs × proj₂ x ≡ n) ∥        ↔⟨ ¬∥∥↔¬ ⟩
      ¬ (∃ λ x → x ∈ xs × proj₂ x ≡ n)            ↝⟨ (λ hyp ∈xs → hyp (_ , ∈xs , refl)) ⟩□
      (s , n) ∉ xs                                □)) ⟩□

  (∃ λ n → Erased ((s , n) ∉ xs))           □

open Signature sig public
  hiding (Sort; Var; _≟O_)
  renaming (var to varᶜ)

private
  variable
    @0 s  : Sort
    @0 xs : Vars
    @0 A  : Type
    @0 x  : A

-- Pattern synonyms.

pattern varᵖ x wf = varᶜ , x , [ wf ]

pattern lamˢᵖ tˢ =
  op lamᶜ (cons (cons (nil tˢ)) nil)
pattern lamᵖ x tˢ t wf =
    lamˢᵖ tˢ
  , ((x , t) , lift tt)
  , [ wf , lift tt ]

pattern appˢᵖ t₁ˢ t₂ˢ =
  op appᶜ (cons (nil t₁ˢ) (cons (nil t₂ˢ) nil))
pattern appᵖ t₁ˢ t₂ˢ t₁ t₂ wf₁ wf₂ =
    appˢᵖ t₁ˢ t₂ˢ
  , (t₁ , t₂ , lift tt)
  , [ wf₁ , wf₂ , lift tt ]

pattern printˢᵖ tˢ =
  op printᶜ (cons (nil tˢ) nil)
pattern printᵖ tˢ t wf =
    printˢᵖ tˢ
  , (t , lift tt)
  , [ wf , lift tt ]

-- Some (more or less) smart constructors.

var : ∀ {s} (x : Var s) → Term ((s , x) ∷ xs) s
var x = varᵖ x (≡→∈∷ refl)

lam :
  (x : Var expr) →
  Term ((expr , x) ∷ xs) expr →
  Term xs expr
lam x (tˢ , t , [ wf ]) =
  lamᵖ x tˢ t (λ _ _ → rename₁-Wf tˢ wf)

app : Term xs expr → Term xs expr → Term xs expr
app (t₁ˢ , t₁ , [ wf₁ ]) (t₂ˢ , t₂ , [ wf₂ ]) =
  appᵖ t₁ˢ t₂ˢ t₁ t₂ wf₁ wf₂

print : Term xs expr → Term xs stmt
print (tˢ , t , [ wf ]) = printᵖ tˢ t wf

-- A representation of "λ x. x".

λx→x : Term [] expr
λx→x = lam 0 (var 0)

-- A representation of "λ x y. y y".

λxy→yy : Term [] expr
λxy→yy = lam 1 $ lam 2 $ app (var 2) (var 2)

-- Two representations of "λ x y. x y".

private

  λxy→xy : ℕ → ℕ → Term [] expr
  λxy→xy x y =
    lam x $ lam y $ app (weaken (λ _ → ∈→∈∷) (var x)) (var y)

λxy→xy₁ : Term [] expr
λxy→xy₁ = λxy→xy 2 1

λxy→xy₂ : Term [] expr
λxy→xy₂ = λxy→xy 1 2

-- A representation of "print (λ x y. x y)".

print[λxy→xy] : Term [] stmt
print[λxy→xy] = print λxy→xy₁

-- A third representation of "λ x y. x y".

λxy→xy₃ : Term [] expr
λxy→xy₃ = weaken lemma λxy→xy₁ [ 0 ← λx→x ]
  where
  @0 lemma : _
  lemma =
    from-⊎ $
    subset?
      (decidable→decidable-∥∥
         (Decidable-erased-equality≃Decidable-equality _ _≟∃V_))
      []
      ((expr , 0) ∷ [])

-- The second and third representations of "λ x y. x y" are equal (in
-- erased contexts).

@0 _ : λxy→xy₂ ≡ λxy→xy₃
_ = Wf-proof-irrelevant

-- An interpreter that uses fuel.

eval : ∀ {xs} → ℕ → Term xs s → Term xs s
eval zero    t = t
eval (suc n) t = eval′ t
  where
  apply : ∀ {xs} → @0 s ≡ expr → Term xs s → Term xs s → Term xs s
  apply _ (lamᵖ x t₁ˢ′ t₁′ wf₁′) t₂′ =
    eval n (subst-Term x t₂′
              ( t₁ˢ′
              , t₁′
              , [ body-Wf t₁ˢ′ wf₁′ ]
              ))
  apply s≡expr t₁′ t₂′ =
    substᴱ (Term _) (sym s≡expr) $
    app (substᴱ (Term _) s≡expr t₁′) (substᴱ (Term _) s≡expr t₂′)

  eval′ : ∀ {xs} → Term xs s → Term xs s
  eval′ t@(varᵖ _ _)                 = t
  eval′ t@(lamᵖ _ _ _ _)             = t
  eval′ (printᵖ tˢ t wf)             = print (eval′ (tˢ , t , [ wf ]))
  eval′ (appᵖ t₁ˢ t₂ˢ t₁ t₂ wf₁ wf₂) = apply refl
    (eval′ (t₁ˢ , t₁ , [ wf₁ ]))
    (eval′ (t₂ˢ , t₂ , [ wf₂ ]))

-- Simple types.

infixr 6 _⇨_

data Ty : Type where
  base : Ty
  _⇨_  : Ty → Ty → Ty

-- Contexts.

Ctxt : Vars → Type
Ctxt xs = Block "Ctxt" → ∀ x → x ∈ xs → Ty

private
  variable
    @0 σ : Ty
    @0 Γ : Ctxt xs

-- Extends a context with a new variable. If the variable already
-- exists in the context, then the old binding is removed.

infixl 5 _,_⦂_

_,_⦂_ : ∀ {xs} → Ctxt xs → ∀ x → Ty → Ctxt (x ∷ xs)
(Γ , x ⦂ σ) ⊠ y y∈x∷xs =
  case y ≟∃V x of λ where
    (yes y≡x) → σ
    (no  y≢x) → Γ ⊠ y (_≃_.to (∈≢∷≃ (Stable-¬ y≢x)) y∈x∷xs)

-- A type system.

infix 4 _⊢_⦂_

data _⊢_⦂_ : Ctxt xs → Term xs s → Ty → Type where
  ⊢var   : ∀ {s x xs} {Γ : Ctxt ((s , x) ∷ xs)} {t σ} →
           t ≡ var x →
           σ ≡ Γ ⊠ (s , x) (≡→∈∷ refl) →
           Γ ⊢ t ⦂ σ
  ⊢lam   : ∀ {xs} {Γ : Ctxt xs} {x t t′ σ τ} →
           Γ , (_ , x) ⦂ σ ⊢ t ⦂ τ →
           t′ ≡ lam x t →
           Γ ⊢ t′ ⦂ σ ⇨ τ
  ⊢app   : ∀ {xs} {Γ : Ctxt xs} {t₁ t₂ t′ σ τ} →
           Γ ⊢ t₁ ⦂ σ ⇨ τ →
           Γ ⊢ t₂ ⦂ σ →
           t′ ≡ app t₁ t₂ →
           Γ ⊢ t′ ⦂ τ
  ⊢print : ∀ {xs} {Γ : Ctxt xs} {t t′ σ} →
           Γ ⊢ t ⦂ σ →
           t′ ≡ print t →
           Γ ⊢ t′ ⦂ σ

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Lib.Bool where

open import Lib.Logic

data Bool : Set where
  true  : Bool
  false : Bool

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

{-# COMPILED_DATA Bool Bool True False #-}

isTrue : Bool -> Set
isTrue true  = True
isTrue false = False

isFalse : Bool -> Set
isFalse true  = False
isFalse false = True

data Inspect (b : Bool) : Set where
  itsTrue  : .(isTrue b)  -> Inspect b
  itsFalse : .(isFalse b) -> Inspect b

inspect : (b : Bool) -> Inspect b
inspect true  = itsTrue _
inspect false = itsFalse _

infix 5 if_then_else_

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

not : Bool -> Bool
not true  = false
not false = true

infixr 25 _&&_
infixr 22 _||_

_&&_ : Bool -> Bool -> Bool
false && y = false
true  && y = y

_||_ : Bool -> Bool -> Bool
false || y = y
true  || y = true

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2020-01-28, issue #4399
-- Pattern @{{_ = p}}@ should not be parsed as cubical partial split.

postulate
  A : Set

data T : Set where
  tt : T

f : {x : A} {{_ : T}} → Set
f ⦃ _ = tt ⦄ = A

-- Expected: Parse error
-- Not a valid named argument: _ = tt