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

module FinVecProperties where

open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin; zero; suc; inject+; raise)
open import Data.Sum using (inj₁; inj₂; [_,_]′)
open import Data.Product using (_×_; proj₁; proj₂; _,′_)

open import Data.Vec
   using (Vec; []; _∷_; tabulate; allFin)
   renaming (_++_ to _++V_; concat to concatV; map to mapV)
open import Data.Vec.Properties
    using (tabulate∘lookup; lookup∘tabulate; lookup-allFin;
           lookup-++-inject+; tabulate-∘)

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
open import Function using (_∘_; id)

--

open import Equiv using (_∼_; p∘!p≡id)
open import FinEquiv using (module Plus; module Times; module PlusTimes)
open import FinVec using (FinVec; 0C; 1C; _∘̂_; _⊎c_; _×c_;
  unite+; uniti+; unite+r; uniti+r;
  swap+cauchy; assocl+; assocr+;
  unite*; uniti*; unite*r; uniti*r;
  swap⋆cauchy; assocl*; assocr*;
  dist*+; factor*+; distl*+; factorl*+;
  right-zero*l; right-zero*r
  )

open import Proofs using (
  -- FiniteFunctions
       finext;
  -- VectorLemmas
       _!!_; lookupassoc; unSplit; lookup-++-raise; tabulate-split;
       concat-map; left!!; right!!; map-map-map; lookup-map; map-∘
     )

------------------------------------------------------------------------------
-- Two ways for reasoning about permutations: we use whichever is more
-- convenient in each context

-- I: we can reason about permutations by looking at their action at
-- every index. This exposes the underlying raw vectors...

infix 4 _∼p_

_∼p_ : {n m : ℕ} (p₁ p₂ : Vec (Fin m) n) → Set
_∼p_ {n} p₁ p₂ = (i : Fin n) → p₁ !! i ≡ p₂ !! i

∼p⇒≡ : {n : ℕ} {p₁ p₂ : Vec (Fin n) n} → (p₁ ∼p p₂) → p₁ ≡ p₂
∼p⇒≡ {n} {p₁} {p₂} eqv =
  begin (
    p₁                            ≡⟨ sym (tabulate∘lookup p₁) ⟩
    tabulate (_!!_ p₁)            ≡⟨ finext eqv ⟩
    tabulate (_!!_ p₂)            ≡⟨ tabulate∘lookup p₂ ⟩
    p₂ ∎)
  where open ≡-Reasoning

cauchyext : {m n : ℕ} (π : FinVec m n) → tabulate (_!!_ π) ≡ π
-- this is just tabulate∘lookup, but it hides the details; should this
-- be called 'join' or 'flatten' ?
cauchyext π = tabulate∘lookup π

1C!!i≡i : ∀ {m} {i : Fin m} → 1C {m} !! i ≡ i
1C!!i≡i = lookup∘tabulate id _

!!⇒∘̂ : {n₁ n₂ n₃ : ℕ} →
        (π₁ : Vec (Fin n₁) n₂) → (π₂ : Vec (Fin n₂) n₃) → (i : Fin n₃) →
        π₁ !! (π₂ !! i) ≡ (π₂ ∘̂ π₁) !! i
!!⇒∘̂ π₁ π₂ i =
  begin (
    π₁ !! (π₂ !! i)
          ≡⟨ sym (lookup∘tabulate (λ j → (π₁ !! (π₂ !! j))) i) ⟩
    tabulate (λ i → π₁ !! (π₂ !! i)) !! i
          ≡⟨ refl ⟩
    (π₂ ∘̂ π₁) !! i ∎)
    where open ≡-Reasoning

-- II: we can relate compositions of permutations of type equivalences
-- and pull back properties of permutations from properties of
-- equivalences

∘̂⇒∘ : {m n o : ℕ} → (f : Fin m → Fin n) → (g : Fin n → Fin o) →
      tabulate f ∘̂ tabulate g ∼p tabulate (g ∘ f)
      -- note the flip!
∘̂⇒∘ f g i =
  begin (
    (tabulate f ∘̂ tabulate g) !! i
      ≡⟨ lookup∘tabulate _ i ⟩
    (tabulate g) !! (tabulate f !! i)
      ≡⟨ lookup∘tabulate _ (tabulate f !! i) ⟩
    g (tabulate f !! i)
      ≡⟨ cong g (lookup∘tabulate f i) ⟩
    g (f i)
      ≡⟨ sym (lookup∘tabulate (g ∘ f) i) ⟩
    tabulate (g ∘ f) !! i ∎)
  where open ≡-Reasoning

-- we could go through ~p, but this works better in practice

~⇒≡ : {m n : ℕ} {f : Fin m → Fin n} {g : Fin n → Fin m} →
           (f ∘ g ∼ id) → (tabulate g ∘̂ tabulate f ≡ 1C)
~⇒≡ {f = f} {g} β =
  ∼p⇒≡ (λ i → trans (∘̂⇒∘ g f i) (cong (λ x → x !! i) (finext β)))

------------------------------------------------------------------------------
-- A permutation and its inverse compose to the identity
--
-- Here we just exploit the connection to type equivalences to get all
-- the properties for free.

-- additives

unite+∘̂uniti+~id : ∀ {m} → (unite+ {m}) ∘̂ uniti+ ≡ 1C {m}
unite+∘̂uniti+~id {m} = ~⇒≡ {m} {n = m} (p∘!p≡id {p = Plus.unite+ {m}})

uniti+∘̂unite+~id : ∀ {m} → (uniti+ {m}) ∘̂ unite+ ≡ 1C {m}
uniti+∘̂unite+~id {m} = ~⇒≡ {m} {n = m} (p∘!p≡id {p = Plus.uniti+})

unite+r∘̂uniti+r~id : ∀ {m} → (unite+r {m}) ∘̂ uniti+r ≡ 1C {m + 0}
unite+r∘̂uniti+r~id {m} = ~⇒≡ {m} (p∘!p≡id {p = Plus.unite+r {m}})

uniti+r∘̂unite+r~id : ∀ {m} → (uniti+r {m}) ∘̂ unite+r ≡ 1C {m}
uniti+r∘̂unite+r~id {m} = ~⇒≡ (p∘!p≡id {p = Plus.uniti+r})

swap+-inv : ∀ {m n} → swap+cauchy m n ∘̂ swap+cauchy n m ≡ 1C
swap+-inv {m} {n} = ~⇒≡ (Plus.swap-inv m n)

assocl+∘̂assocr+~id : ∀ {m n o} → assocl+ {m} {n} {o} ∘̂ assocr+ {m} ≡ 1C
assocl+∘̂assocr+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Plus.assocl+ {m}})

assocr+∘̂assocl+~id : ∀ {m n o} → assocr+ {m} {n} {o} ∘̂ assocl+ {m} ≡ 1C
assocr+∘̂assocl+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Plus.assocr+ {m}})

-- multiplicatives

unite*∘̂uniti*~id : ∀ {m} → (unite* {m}) ∘̂ uniti* ≡ 1C {1 * m}
unite*∘̂uniti*~id {m} = ~⇒≡ {m} {n = 1 * m} (p∘!p≡id {p = Times.unite* {m}})

uniti*∘̂unite*~id : ∀ {m} → (uniti* {m}) ∘̂ unite* ≡ 1C {m}
uniti*∘̂unite*~id {m} = ~⇒≡ {1 * m} {n = m} (p∘!p≡id {p = Times.uniti* {m}})

unite*r∘̂uniti*r~id : ∀ {m} → (unite*r {m}) ∘̂ uniti*r ≡ 1C {m * 1}
unite*r∘̂uniti*r~id {m} = ~⇒≡ {m} {n = m * 1} (p∘!p≡id {p = Times.unite*r {m}})

uniti*r∘̂unite*r~id : ∀ {m} → (uniti*r {m}) ∘̂ unite*r ≡ 1C {m}
uniti*r∘̂unite*r~id {m} = ~⇒≡ {m * 1} {n = m} (p∘!p≡id {p = Times.uniti*r {m}})

swap*-inv : ∀ {m n} → swap⋆cauchy m n ∘̂ swap⋆cauchy n m ≡ 1C
swap*-inv {m} {n} = ~⇒≡ (Times.swap-inv m n)

assocl*∘̂assocr*~id : ∀ {m n o} → assocl* {m} {n} {o} ∘̂ assocr* {m} ≡ 1C
assocl*∘̂assocr*~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Times.assocl* {m}})

assocr*∘̂assocl*~id : ∀ {m n o} → assocr* {m} {n} {o} ∘̂ assocl* {m} ≡ 1C
assocr*∘̂assocl*~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = Times.assocr* {m}})

-- Distributivity

right-zero*l∘̂right-zero*r~id : ∀ {m} →
  right-zero*l {m} ∘̂ right-zero*r {m} ≡ 1C {m * 0}
right-zero*l∘̂right-zero*r~id {m} =
  ~⇒≡ {f = proj₁ (PlusTimes.factorzr {m})} (p∘!p≡id {p = PlusTimes.distzr {m}})

right-zero*r∘̂right-zero*l~id : ∀ {m} → right-zero*r {m} ∘̂ right-zero*l {m} ≡ 1C
right-zero*r∘̂right-zero*l~id {m} =
  ~⇒≡ { f = proj₁ (PlusTimes.factorz {m})} (p∘!p≡id {p = PlusTimes.distz {m}})

dist*+∘̂factor*+~id : ∀ {m n o} → dist*+ {m} {n} {o} ∘̂ factor*+ {m} ≡ 1C
dist*+∘̂factor*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.dist {m}})

factor*+∘̂dist*+~id : ∀ {m n o} → factor*+ {m} {n} {o} ∘̂ dist*+ {m} ≡ 1C
factor*+∘̂dist*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.factor {m}})

distl*+∘̂factorl*+~id : ∀ {m n o} → distl*+ {m} {n} {o} ∘̂ factorl*+ {m} ≡ 1C
distl*+∘̂factorl*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.distl {m}})

factorl*+∘̂distl*+~id : ∀ {m n o} → factorl*+ {m} {n} {o} ∘̂ distl*+ {m} ≡ 1C
factorl*+∘̂distl*+~id {m} {_} {o} = ~⇒≡ (p∘!p≡id {p = PlusTimes.factorl {m}})

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

-- Now the main properties of sequential composition

0C∘̂0C≡0C : 1C {0} ∘̂ 1C {0} ≡ 1C {0}
0C∘̂0C≡0C = refl

∘̂-assoc : {m₁ m₂ m₃ m₄ : ℕ} →
         (a : Vec (Fin m₂) m₁) (b : Vec (Fin m₃) m₂) (c : Vec (Fin m₄) m₃) →
         a ∘̂ (b ∘̂ c) ≡ (a ∘̂ b) ∘̂ c
∘̂-assoc a b c = finext (lookupassoc a b c)

∘̂-rid : {m n : ℕ} → (π : Vec (Fin m) n) → π ∘̂ 1C ≡ π
∘̂-rid π = trans (finext (λ i → lookup-allFin (π !! i))) (cauchyext π)

∘̂-lid : {m n : ℕ} → (π : Vec (Fin m) n) → 1C ∘̂ π ≡ π
∘̂-lid π = trans (finext (λ i → cong (_!!_ π) (lookup-allFin i))) (cauchyext π)

--

1C₀⊎x≡x : ∀ {m n} {x : FinVec m n} → 1C {0} ⊎c x ≡ x
1C₀⊎x≡x {x = x} = cauchyext x

unite+∘[0⊎x]≡x∘unite+ : ∀ {m n} {x : FinVec m n} →
  unite+ ∘̂ (1C {0} ⊎c x) ≡ x ∘̂ unite+
unite+∘[0⊎x]≡x∘unite+ {m} {n} {x} = finext pf
  where
    pf : (i : Fin n) → (0C ⊎c x) !! (unite+ !! i) ≡ unite+ !! (x !! i)
    pf i =
      begin (
        tabulate (λ y → x !! y) !! (tabulate id !! i)
          ≡⟨ cong (λ j → tabulate (λ y → x !! y) !! j) (lookup∘tabulate id i) ⟩
        tabulate (λ y → x !! y) !! i
          ≡⟨ lookup∘tabulate (_!!_ x) i ⟩
        x !! i
          ≡⟨ sym (lookup∘tabulate id (x !! i)) ⟩
        tabulate id !! (x !! i) ∎)
      where open ≡-Reasoning

uniti+∘x≡[0⊎x]∘uniti+ : ∀ {m n} {x : FinVec m n} →
  uniti+ ∘̂ x ≡ (1C {0} ⊎c x) ∘̂ uniti+
uniti+∘x≡[0⊎x]∘uniti+ {m} {n} {x} = finext pf
  where
    pf : (i : Fin n) → x !! (uniti+ !! i) ≡ uniti+ !! ((0C ⊎c x) !! i)
    pf i = begin (
      x !! (tabulate id !! i)
        ≡⟨ cong (_!!_ x) (lookup∘tabulate id i) ⟩
      x !! i
        ≡⟨ sym (lookup∘tabulate (λ y → x !! y) i) ⟩
      tabulate (λ y → x !! y) !! i
        ≡⟨ sym (lookup∘tabulate id _) ⟩
      tabulate id !! (tabulate (λ y → x !! y) !! i) ∎)
      where open ≡-Reasoning

1C⊎1C≡1C : ∀ {m n} → 1C {m} ⊎c 1C {n} ≡ 1C
1C⊎1C≡1C {m} {n} =
  begin (
     tabulate {m} (inject+ n ∘ _!!_ 1C) ++V tabulate {n} (raise m ∘ _!!_ 1C)
       ≡⟨ cong₂ (_++V_ {m = m})
           (finext (λ i → cong (inject+ n) (lookup-allFin i)))
           (finext (λ i → cong (raise m) (lookup-allFin i))) ⟩
     tabulate {m} (inject+ n) ++V tabulate {n} (raise m)
       ≡⟨ unSplit {m} id ⟩
     tabulate {m + n} id ∎)
  where open ≡-Reasoning

idˡ⊕ : ∀ {m n} {x : FinVec m n} → uniti+ ∘̂ (1C {0} ⊎c x) ≡ x ∘̂ uniti+
idˡ⊕ {m} {n} {x} = finext pf
  where
    open ≡-Reasoning
    pf : (i : Fin n) → (1C {0} ⊎c x) !! (uniti+ !! i) ≡ (uniti+ !! (x !! i))
    pf i =  begin (
      tabulate (λ y → x !! y) !! (tabulate id !! i)
        ≡⟨ cong (_!!_ (tabulate λ y → x !! y)) (lookup∘tabulate id i) ⟩
      (tabulate (λ y → x !! y)) !! i
        ≡⟨ lookup∘tabulate (λ y → x !! y) i ⟩
      x !! i
        ≡⟨ sym (lookup∘tabulate id (x !! i)) ⟩
      tabulate id !! (x !! i) ∎)

-- [,]-commute : {A B C D E : Set} → {f : A → C} → {g : B → C} → {h : C → D} →
--   ∀ x → h ([ f , g ]′ x) ≡ [ (h ∘ f) , (h ∘ g) ]′ x
-- [,]-commute (inj₁ x) = refl
-- [,]-commute (inj₂ y) = refl

--

private

  left⊎⊎!! :  ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → (p₁ : FinVec m₁ n₁) → (p₂ : FinVec m₂ n₂)
    → (p₃ : FinVec m₃ m₁) → (p₄ : FinVec m₄ m₂) → (i : Fin n₁) →
    (p₃ ⊎c p₄) !! ( (p₁ ⊎c p₂) !! inject+ n₂ i ) ≡ inject+ m₄ ( (p₁ ∘̂ p₃) !! i)
  left⊎⊎!! {m₁} {m₂} {_} {m₄} {_} {n₂} p₁ p₂ p₃ p₄ i =
    let pp = p₃ ⊎c p₄ in
    let qq = p₁ ⊎c p₂ in
    begin (
        pp !! (qq !! inject+ n₂ i)
          ≡⟨ cong
               (_!!_ pp)
               (lookup-++-inject+
                 (tabulate (inject+ m₂ ∘ _!!_ p₁))
                 (tabulate (raise m₁ ∘ _!!_ p₂))
                 i) ⟩
       pp !! (tabulate (inject+ m₂ ∘ _!!_ p₁ ) !! i)
          ≡⟨ cong (_!!_ pp) (lookup∘tabulate _ i) ⟩
       pp !! (inject+ m₂ (p₁ !! i))
          ≡⟨ left!! (p₁ !! i) (inject+ m₄ ∘ (_!!_ p₃)) ⟩
        inject+ m₄ (p₃ !! (p₁ !! i))
          ≡⟨ cong (inject+ m₄) (sym (lookup∘tabulate _ i)) ⟩
        inject+ m₄ ((p₁ ∘̂ p₃) !! i) ∎ )
      where open ≡-Reasoning

  right⊎⊎!! :  ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → (p₁ : FinVec m₁ n₁) → (p₂ : FinVec m₂ n₂)
    → (p₃ : FinVec m₃ m₁) → (p₄ : FinVec m₄ m₂) → (i : Fin n₂) →
    (p₃ ⊎c p₄) !! ( (p₁ ⊎c p₂) !! raise n₁ i ) ≡ raise m₃ ( (p₂ ∘̂ p₄) !! i)
  right⊎⊎!! {m₁} {m₂} {m₃} {_} {n₁} {_} p₁ p₂ p₃ p₄ i =
    let pp = p₃ ⊎c p₄ in
    let qq = p₁ ⊎c p₂ in
    begin (
      pp !! (qq !! raise n₁ i)
        ≡⟨ cong
             (_!!_ pp)
             (lookup-++-raise
               (tabulate (inject+ m₂ ∘ _!!_ p₁))
               (tabulate (raise m₁ ∘ _!!_ p₂))
               i) ⟩
      pp !! (tabulate (raise m₁ ∘ _!!_ p₂) !! i)
        ≡⟨ cong (_!!_ pp) (lookup∘tabulate _ i) ⟩
      pp !! raise m₁ (p₂ !! i)
        ≡⟨ right!! {m₁} (p₂ !! i) (raise m₃ ∘ (_!!_ p₄)) ⟩
      raise m₃ (p₄ !! (p₂ !! i))
        ≡⟨ cong (raise m₃) (sym (lookup∘tabulate _ i)) ⟩
      raise m₃ ((p₂ ∘̂ p₄) !! i) ∎ )
      where open ≡-Reasoning

⊎c-distrib : ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → {p₁ : FinVec m₁ n₁} → {p₂ : FinVec m₂ n₂}
  → {p₃ : FinVec m₃ m₁} → {p₄ : FinVec m₄ m₂} →
    (p₁ ⊎c p₂) ∘̂ (p₃ ⊎c p₄) ≡ (p₁ ∘̂ p₃) ⊎c (p₂ ∘̂ p₄)
⊎c-distrib {m₁} {m₂} {m₃} {m₄} {n₁} {n₂} {p₁} {p₂} {p₃} {p₄} =
  let p₃₄ = p₃ ⊎c p₄ in let p₁₂ = p₁ ⊎c p₂ in
  let lhs = λ i → p₃₄ !! (p₁₂ !! i) in
  begin (
    tabulate lhs
      ≡⟨ tabulate-split {n₁} {n₂} ⟩
    tabulate {n₁} (lhs ∘ inject+ n₂) ++V tabulate {n₂} (lhs ∘ raise n₁)
      ≡⟨ cong₂ _++V_
          (finext (left⊎⊎!! p₁ _ _ _))
          (finext (right⊎⊎!! p₁ _ _ _)) ⟩
    tabulate {n₁} (λ i → inject+ m₄ ((p₁ ∘̂ p₃) !! i)) ++V
    tabulate {n₂} (λ i → raise m₃ ((p₂ ∘̂ p₄) !! i))
      ≡⟨ refl ⟩
    (p₁ ∘̂ p₃) ⊎c (p₂ ∘̂ p₄) ∎)
    where open ≡-Reasoning

private

  concat!! : {A : Set} {m n : ℕ} → (a : Fin m) → (b : Fin n) →
    (xss : Vec (Vec A n) m) →
    concatV xss !! (Times.fwd (a ,′ b)) ≡ (xss !! a) !! b
  concat!! zero b (xs ∷ xss) = lookup-++-inject+ xs (concatV xss) b
  concat!! (suc a) b (xs ∷ xss) =
    trans
      (lookup-++-raise xs (concatV xss) (Times.fwd (a ,′ b)))
      (concat!! a b xss)

  ×c-equiv : {m₁ m₂ n₁ n₂ : ℕ} (p₁ : FinVec m₁ n₁) (p₂ : FinVec m₂ n₂) →
    (p₁ ×c p₂) ≡
    concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁)
  ×c-equiv p₁ p₂ =
    let zss = mapV  (λ b → mapV (λ x → b ,′ x) p₂) p₁ in
    begin (
      (p₁ ×c p₂)
        ≡⟨ refl ⟩
      mapV Times.fwd (concatV zss)
        ≡⟨ sym (concat-map zss Times.fwd) ⟩
      concatV (mapV (mapV Times.fwd) zss)
        ≡⟨ cong concatV
            (map-map-map Times.fwd (λ b → mapV (λ x → b ,′ x) p₂) p₁) ⟩
       concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁) ∎)
      where open ≡-Reasoning

  lookup-2d : {A : Set} (m n : ℕ) → (k : Fin (m * n)) →
     {f : Fin m × Fin n → A} →
     concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i ,′ j)))) !! k ≡
     f (Times.bwd k)
  lookup-2d m n k {f} =
    let lhs = concatV (tabulate {m} (λ i → tabulate {n} (λ j → f (i ,′ j))))
        a = proj₁ (Times.bwd {m} {n} k)
        b = proj₂ (Times.bwd {m} {n} k) in
    begin (
      lhs !! k
        ≡⟨ cong (_!!_ lhs) (sym (Times.fwd∘bwd~id {m} k)) ⟩
      lhs !! (Times.fwd (a ,′ b))
        ≡⟨ concat!! a b _ ⟩
      (tabulate {m} (λ i → tabulate {n} (λ j → f (i ,′ j))) !! a) !! b
        ≡⟨ cong (λ x → x !! b) (lookup∘tabulate _ a) ⟩
      tabulate {n} (λ j → f (a ,′ j)) !! b
        ≡⟨ lookup∘tabulate _ b ⟩
      f (a ,′ b)
        ≡⟨ refl ⟩
      f (Times.bwd k) ∎)
      where open ≡-Reasoning

  ×c!! : {m₁ m₂ n₁ n₂ : ℕ} (p₁ : FinVec m₁ n₁) (p₂ : FinVec m₂ n₂)
    (k : Fin (n₁ * n₂)) →
    (p₁ ×c p₂) !! k ≡
    Times.fwd (p₁ !! proj₁ (Times.bwd k) ,′ p₂ !! proj₂ (Times.bwd {n₁} k))
  ×c!! {n₁ = n₁} p₁ p₂ k =
    let a = proj₁ (Times.bwd {n₁} k) in
    let b = proj₂ (Times.bwd {n₁} k) in
    begin (
      (p₁ ×c p₂) !! k
        ≡⟨ cong₂ _!!_ (×c-equiv p₁ p₂) (sym (Times.fwd∘bwd~id {n₁} k)) ⟩
      concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁) !!
      Times.fwd (a ,′ b)
        ≡⟨ concat!! a b _ ⟩
      ((mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂)) p₁) !! a) !! b
        ≡⟨ cong (λ x → x !! b) (lookup-map a _ p₁) ⟩
      mapV Times.fwd (mapV (λ x → p₁ !! a ,′ x) p₂) !! b
        ≡⟨ cong (λ x → x !! b) (sym (map-∘ Times.fwd _ p₂)) ⟩
      mapV (Times.fwd ∘ (λ x → p₁ !! a ,′ x)) p₂ !! b
        ≡⟨ lookup-map b _ p₂ ⟩
      Times.fwd (p₁ !! a ,′ p₂ !! b) ∎)
      where open ≡-Reasoning

×c-distrib : ∀ {m₁ m₂ m₃ m₄ n₁ n₂} → {p₁ : FinVec m₁ n₁} → {p₂ : FinVec m₂ n₂}
  → {p₃ : FinVec m₃ m₁} → {p₄ : FinVec m₄ m₂} →
    (p₁ ×c p₂) ∘̂ (p₃ ×c p₄) ≡ (p₁ ∘̂ p₃) ×c (p₂ ∘̂ p₄)
×c-distrib {m₁} {m₂} {m₃} {m₄} {n₁} {n₂} {p₁} {p₂} {p₃} {p₄} =
  let p₃₄ = p₃ ×c p₄ in let p₁₂ = p₁ ×c p₂ in
  let p₂₄ = p₂ ∘̂ p₄ in let p₁₃ = p₁ ∘̂ p₃ in
  let lhs = λ i → p₃₄ !! (p₁₂ !! i) in
  let zss = mapV  (λ b → mapV (λ x → b ,′ x) (p₂ ∘̂ p₄)) (p₁ ∘̂ p₃) in
  begin (
     tabulate {n₁ * n₂} (λ i → p₃₄ !! (p₁₂ !! i))
       ≡⟨ finext (λ j → cong (_!!_ p₃₄) (×c!! p₁ p₂ j)) ⟩
     tabulate {n₁ * n₂}
       (λ i → p₃₄ !! Times.fwd (p₁ !! proj₁ (Times.bwd i) ,′
              p₂ !! proj₂ (Times.bwd i)))
       ≡⟨ finext (λ j → ×c!! p₃ p₄ _) ⟩
     tabulate (λ i →
       let k = Times.fwd (p₁ !! proj₁ (Times.bwd i) ,′
                          p₂ !! proj₂ (Times.bwd i)) in
       Times.fwd (p₃ !! proj₁ (Times.bwd k) ,′ p₄ !! proj₂ (Times.bwd k)))
       ≡⟨ finext (λ i → cong₂
                         (λ x y → Times.fwd (p₃ !! proj₁ x ,′ p₄ !! proj₂ y))
                 (Times.bwd∘fwd~id {m₁} {m₂} (p₁ !! proj₁ (Times.bwd i) ,′ _))
                 (Times.bwd∘fwd~id (_ ,′ p₂ !! proj₂ (Times.bwd i)))) ⟩
     tabulate (λ i → Times.fwd (p₃ !! (p₁ !! proj₁ (Times.bwd i)) ,′
                                (p₄ !! (p₂ !! proj₂ (Times.bwd i)))))
       ≡⟨ finext (λ k → sym (lookup-2d n₁ n₂ k)) ⟩
     tabulate (λ k →
       concatV (tabulate {n₁} (λ z →
                tabulate {n₂} (λ w →
                Times.fwd ((p₃ !! (p₁ !! z)) ,′ (p₄ !! (p₂ !! w))))))
       !! k)
        ≡⟨ tabulate∘lookup _ ⟩
     concatV (tabulate {n₁} (λ z →
              tabulate {n₂} (λ w →
              Times.fwd ((p₃ !! (p₁ !! z)) ,′ (p₄ !! (p₂ !! w))))))
       ≡⟨ cong
           concatV
           (finext (λ i →
             tabulate-∘ Times.fwd
               (λ w → ((p₃ !! (p₁ !! i)) ,′ (p₄ !! (p₂ !! w)))))) ⟩
     concatV (tabulate (λ z →
              mapV Times.fwd
                (tabulate (λ w → (p₃ !! (p₁ !! z)) ,′ (p₄ !! (p₂ !! w))))))
       ≡⟨ cong
           concatV
           (finext (λ i →
             cong
               (mapV Times.fwd)
               (tabulate-∘
                 (λ x → (p₃ !! (p₁ !! i)) ,′ x)
                 (_!!_ p₄ ∘ _!!_ p₂)))) ⟩
     concatV
       (tabulate
         (λ z → mapV Times.fwd (mapV (λ x → (p₃ !! (p₁ !! z)) ,′ x) p₂₄)))
       ≡⟨ cong concatV (tabulate-∘ _ (_!!_ p₃ ∘ _!!_ p₁)) ⟩
     concatV (mapV (λ y → mapV Times.fwd (mapV (λ x → y ,′ x) p₂₄)) p₁₃)
       ≡⟨ sym (×c-equiv p₁₃ p₂₄) ⟩
     (p₁ ∘̂ p₃) ×c (p₂ ∘̂ p₄) ∎)
     where open ≡-Reasoning

-- there might be a simpler proofs of this using tablate∘lookup

1C×1C≡1C : ∀ {m n} → (1C {m} ×c 1C {n}) ≡ 1C {m * n}
1C×1C≡1C {m} {n} =
  begin (
    1C {m} ×c 1C
      ≡⟨ ×c-equiv 1C 1C ⟩
    concatV (mapV (λ y → mapV Times.fwd (mapV (_,′_ y) (1C {n}))) (1C {m}))
      ≡⟨ cong (concatV {n = m}) (sym (tabulate-∘ _ id)) ⟩
    concatV {n = m} (tabulate (λ y → mapV Times.fwd (mapV (_,′_ y) (1C {n}))))
      ≡⟨ cong (concatV {n = m})
          (finext (λ y → sym (map-∘ Times.fwd (λ x → y ,′ x) 1C))) ⟩
    concatV (tabulate {n = m} (λ y → mapV (Times.fwd ∘ (_,′_ y)) (1C {n})))
      ≡⟨ cong
          (concatV {m = n} {m})
          (finext (λ y → sym (tabulate-∘ (Times.fwd ∘ (_,′_ y)) id))) ⟩
    concatV (tabulate {n = m}
              (λ a → tabulate {n = n} (λ b → Times.fwd (a ,′ b))))
      ≡⟨ sym (tabulate∘lookup _) ⟩
    tabulate (λ k →
    concatV (tabulate {n = m}
              (λ a → tabulate {n = n} (λ b → Times.fwd (a ,′ b)))) !! k)
      ≡⟨ finext (λ k → lookup-2d m n k) ⟩
    tabulate (λ k → Times.fwd {m} {n} (Times.bwd k))
      ≡⟨ finext (Times.fwd∘bwd~id {m} {n}) ⟩
    1C {m * n} ∎ )
    where open ≡-Reasoning

------------------------------------------------------------------------------
-- A few "reveal" functions, to let us peek into the representation

reveal1C : ∀ {m} → allFin m ≡ 1C
reveal1C = refl

reveal0C : [] ≡ 1C {0}
reveal0C = refl

reveal⊎c :  ∀ {m₁ n₁ m₂ n₂} → {α : FinVec m₁ m₂} → {β : FinVec n₁ n₂} →
  α ⊎c β ≡
    tabulate (Plus.fwd ∘ inj₁ ∘ _!!_ α) ++V
    tabulate (Plus.fwd {m₁} ∘ inj₂ ∘ _!!_ β)
reveal⊎c = refl

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Agda.Builtin.String where

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Char

postulate String : Set
{-# BUILTIN STRING String #-}

primitive
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringAppend   : String → String → String
  primStringEquality : String → String → Bool
  primShowChar       : Char → String
  primShowString     : String → String

ext: agda


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

module Data.PolyP.Derivations.Levels where

open import Data.PolyP
open import Level
open import Data.PolyP.Types
open import Data.Sum
open import Data.Sigma
open import Data.Unit
open import Data.Fin
open import Data.Nat
open import Data.Vec
open import Function
open import Literals.Number
open import Data.Fin.Literals
open import Data.Nat.Literals

levels : ⟦ FOREST ⟧ ~ A → ⟦ LEVELS ⟧ ~ A
levels t = go t []′
  where
  go : ⟦ FOREST ⟧ ~ A → ⟦ LEVELS ⟧ ~ A → ⟦ LEVELS ⟧ ~ A
  go =
    cata λ xs zs →
      cata (λ  { (inl _                             )  → zs
               ; (inr (inl _         ,  qs       )  )  → qs
               ; (inr (inr (x , xs)  ,  []′      )  )  → (x ∷′ []′  ) ∷′ xs []′
               ; (inr (inr (x , xs)  ,  q ∷′ qs  )  )  → (x ∷′ q    ) ∷′ xs qs
               }) xs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Agda.Builtin.Equality using (_≡_; refl)

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

open ∃ public

uncurry : {A : Set} {B : A → Set} {C : ∃ B → Set₁} →
          ((x : A) (y : B x) → C (x , y)) →
          ((p : ∃ B) → C p)
uncurry f (x , y) = f x y

_⟶_ : {I : Set} → (I → Set) → (I → Set) → Set
A ⟶ B = ∀ {i} → A i → B i

postulate
  I   : Set
  i j : I
  R   : I → I → Set

record P : Set where
  field
    f : ∀ {k} → R i k → ∃ λ l → R k l

Q : Set
Q =
  ∃ λ (f : ∀ {j} → R i j → I) →
  (λ { (j , k) → ∃ λ (r : R i j) → f r ≡ k }) ⟶ uncurry R

to : P → Q
to f = (λ r → proj₁ (P.f f r))
     , λ { (r , refl) → proj₂ (P.f f r) }

from : Q → P
P.f (from (f , g)) r = f r , g (r , refl)

-- Should produce a nice error and not throw an __IMPOSSIBLE__.
to∘from : ∀ q → to (from q) ≡ q
to∘from _ = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --safe --no-import-sorts #-}
module Cubical.Algebra.Module.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Ring      renaming (⟨_⟩ to ⟨_⟩r)
open import Cubical.Algebra.AbGroup   hiding (⟨_⟩)
open import Cubical.Algebra.Group     hiding (⟨_⟩)

open Iso

private
  variable
    ℓ : Level

record IsLeftModule (R : Ring {ℓ}) {M : Type ℓ}
              (0m : M)
              (_+_ : M → M → M)
              (-_ : M → M)
              (_⋆_ : ⟨ R ⟩r → M → M) : Type ℓ where

  constructor ismodule

  open Ring R using (_·_; 1r) renaming (_+_ to _+r_)

  field
    +-isAbGroup : IsAbGroup 0m _+_ -_
    ⋆-assoc : (r s : ⟨ R ⟩r) (x : M) → (r · s) ⋆ x ≡ r ⋆ (s ⋆ x)
    ⋆-ldist : (r s : ⟨ R ⟩r) (x : M) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x)
    ⋆-rdist : (r : ⟨ R ⟩r) (x y : M) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y)
    ⋆-lid   : (x : M) → 1r ⋆ x ≡ x

  open IsAbGroup +-isAbGroup public
    renaming
    ( assoc       to +-assoc
    ; identity    to +-identity
    ; lid         to +-lid
    ; rid         to +-rid
    ; inverse     to +-inv
    ; invl        to +-linv
    ; invr        to +-rinv
    ; comm        to +-comm
    ; isSemigroup to +-isSemigroup
    ; isMonoid    to +-isMonoid
    ; isGroup     to +-isGroup
    )

record LeftModule (R : Ring {ℓ}) : Type (ℓ-suc ℓ) where

  constructor leftmodule

  field
    Carrier        : Type ℓ
    0m             : Carrier
    _+_            : Carrier → Carrier → Carrier
    -_             : Carrier → Carrier
    _⋆_            : ⟨ R ⟩r → Carrier → Carrier
    isLeftModule   : IsLeftModule R 0m _+_ -_ _⋆_

  open IsLeftModule isLeftModule public

module _ {R : Ring {ℓ}} where
  ⟨_⟩ : LeftModule R → Type ℓ
  ⟨_⟩ = LeftModule.Carrier

  LeftModule→AbGroup : (M : LeftModule R) → AbGroup {ℓ}
  LeftModule→AbGroup (leftmodule _ _ _ _ _ isLeftModule) =
                     abgroup _ _ _ _ (IsLeftModule.+-isAbGroup isLeftModule)

  isSetLeftModule : (M : LeftModule R) → isSet ⟨ M ⟩
  isSetLeftModule M = isSetAbGroup (LeftModule→AbGroup M)

  open Ring R using (1r) renaming (_+_ to _+r_; _·_ to _·s_)

  makeIsLeftModule : {M : Type ℓ} {0m : M}
                  {_+_ : M → M → M} { -_ : M → M} {_⋆_ : ⟨ R ⟩r → M → M}
                  (isSet-M : isSet M)
                  (+-assoc :  (x y z : M) → x + (y + z) ≡ (x + y) + z)
                  (+-rid : (x : M) → x + 0m ≡ x)
                  (+-rinv : (x : M) → x + (- x) ≡ 0m)
                  (+-comm : (x y : M) → x + y ≡ y + x)
                  (⋆-assoc : (r s : ⟨ R ⟩r) (x : M) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
                  (⋆-ldist : (r s : ⟨ R ⟩r) (x : M) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                  (⋆-rdist : (r : ⟨ R ⟩r) (x y : M) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                  (⋆-lid   : (x : M) → 1r ⋆ x ≡ x)
                → IsLeftModule R 0m _+_ -_ _⋆_
  makeIsLeftModule isSet-M
                +-assoc +-rid +-rinv +-comm
                ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid =
                ismodule (makeIsAbGroup isSet-M +-assoc +-rid +-rinv +-comm)
                         ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid

record LeftModuleEquiv {R : Ring {ℓ}} (M N : LeftModule R) : Type ℓ where

  constructor moduleiso

  private
    instance
      _ : LeftModule R
      _ = M
      _ : LeftModule R
      _ = N

  open LeftModule {{...}}

  field
    e : ⟨ M ⟩ ≃ ⟨ N ⟩
    isHom+ : (x y : ⟨ M ⟩) → equivFun e (x + y) ≡ equivFun e x + equivFun e y
    comm⋆ : (r : ⟨ R ⟩r) (x : ⟨ M ⟩) → equivFun e (r ⋆ x) ≡ r ⋆ equivFun e x

module LeftModuleΣTheory (R : Ring {ℓ}) where

  RawLeftModuleStructure = λ (M : Type ℓ) → (M → M → M) × (⟨ R ⟩r → M → M)

  RawLeftModuleEquivStr = AutoEquivStr RawLeftModuleStructure

  rawLeftModuleUnivalentStr : UnivalentStr _ RawLeftModuleEquivStr
  rawLeftModuleUnivalentStr = autoUnivalentStr RawLeftModuleStructure

  open Ring R using (_·_; 1r) renaming (_+_ to _+r_)

  LeftModuleAxioms : (M : Type ℓ) (s : RawLeftModuleStructure M) → Type ℓ
  LeftModuleAxioms M (_+_ , _⋆_) = AbGroupΣTheory.AbGroupAxioms M _+_
                                    × ((r s : ⟨ R ⟩r) (x : M) → (r · s) ⋆ x ≡ r ⋆ (s ⋆ x))
                                    × ((r s : ⟨ R ⟩r) (x : M) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                                    × ((r : ⟨ R ⟩r) (x y : M) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                                    × ((x : M) → 1r ⋆ x ≡ x)

  LeftModuleStructure : Type ℓ → Type ℓ
  LeftModuleStructure = AxiomsStructure RawLeftModuleStructure LeftModuleAxioms

  LeftModuleΣ : Type (ℓ-suc ℓ)
  LeftModuleΣ = TypeWithStr ℓ LeftModuleStructure

  LeftModuleEquivStr : StrEquiv LeftModuleStructure ℓ
  LeftModuleEquivStr = AxiomsEquivStr RawLeftModuleEquivStr LeftModuleAxioms

  open AbGroupΣTheory using (isSetAbGroupΣ)

  isSetLeftModuleΣ : (M : LeftModuleΣ)  → isSet _
  isSetLeftModuleΣ (M , (_+_ , _) , (isAbGroup-M , _)) = isSetAbGroupΣ (M , _+_ , isAbGroup-M)

  isPropLeftModuleAxioms : (M : Type ℓ) (s : RawLeftModuleStructure M)
                             → isProp (LeftModuleAxioms M s)
  isPropLeftModuleAxioms M (_+_ , _⋆_) =
     isPropΣ (AbGroupΣTheory.isPropAbGroupAxioms M _+_)
             λ isAbGroup-M →
             isProp× (isPropΠ3 λ _ _ _ → (isSetAbGroupΣ (M , _+_ , isAbGroup-M)) _ _)
            (isProp× (isPropΠ3 λ _ _ _ → (isSetAbGroupΣ (M , _+_ , isAbGroup-M)) _ _)
            (isProp× (isPropΠ3 λ _ _ _ → (isSetAbGroupΣ (M , _+_ , isAbGroup-M)) _ _)
                     (isPropΠ  λ _     → (isSetAbGroupΣ (M , _+_ , isAbGroup-M)) _ _)))

  LeftModule→LeftModuleΣ : LeftModule R → LeftModuleΣ
  LeftModule→LeftModuleΣ
    (leftmodule M 0m _+_ -_ _⋆_ (ismodule +-isAbGroup ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid)) =
    M , (_+_ , _⋆_) ,
    AbGroupΣTheory.AbGroup→AbGroupΣ (abgroup _ _ _ _ +-isAbGroup) .snd .snd ,
    ⋆-assoc , ⋆-ldist , ⋆-rdist , ⋆-lid

  LeftModuleΣ→LeftModule : LeftModuleΣ → LeftModule R
  LeftModuleΣ→LeftModule (M , (_+_ , _⋆_) , isAbGroup-M , ⋆-assoc , ⋆-ldist , ⋆-rdist , ⋆-lid) =
    let isAbGroup = AbGroupΣTheory.AbGroupΣ→AbGroup (_ , _ , isAbGroup-M ) .AbGroup.isAbGroup
    in leftmodule M _ _+_ _ _⋆_
       (ismodule isAbGroup ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid)

  LeftModuleIsoLeftModuleΣ : Iso (LeftModule R) LeftModuleΣ
  LeftModuleIsoLeftModuleΣ = iso LeftModule→LeftModuleΣ LeftModuleΣ→LeftModule
                                 (λ _ → refl) helper
    where
      open AbGroupΣTheory
      abgroup-helper : retract (AbGroup→AbGroupΣ {ℓ}) AbGroupΣ→AbGroup
      abgroup-helper = Iso.leftInv AbGroupIsoAbGroupΣ

      open LeftModule
      open IsLeftModule
      helper : _
      Carrier (helper M i) = Carrier M
      0m (helper M i) = 0m M
      _+_ (helper M i) = _+_ M
      -_ (helper M i) =  -_ M
      _⋆_ (helper M i) = _⋆_ M

      +-isAbGroup (isLeftModule (helper M i)) =
        AbGroup.isAbGroup (abgroup-helper (abgroup _ _ _ _ (+-isAbGroup M)) i)
      ⋆-assoc (isLeftModule (helper M i)) = ⋆-assoc M
      ⋆-ldist (isLeftModule (helper M i)) = ⋆-ldist M
      ⋆-rdist (isLeftModule (helper M i)) = ⋆-rdist M
      ⋆-lid (isLeftModule (helper M i)) = ⋆-lid M

  leftModuleUnivalentStr : UnivalentStr LeftModuleStructure LeftModuleEquivStr
  leftModuleUnivalentStr = axiomsUnivalentStr _ isPropLeftModuleAxioms rawLeftModuleUnivalentStr

  LeftModuleΣPath : (M N : LeftModuleΣ) → (M ≃[ LeftModuleEquivStr ] N) ≃ (M ≡ N)
  LeftModuleΣPath = SIP leftModuleUnivalentStr

  LeftModuleEquivStrΣ : (M N : LeftModule R) → Type ℓ
  LeftModuleEquivStrΣ M N = LeftModule→LeftModuleΣ M ≃[ LeftModuleEquivStr ] LeftModule→LeftModuleΣ N

  LeftModuleEquivStrΣPath : {M N : LeftModule R} → Iso (LeftModuleEquiv M N) (LeftModuleEquivStrΣ M N)
  fun LeftModuleEquivStrΣPath (moduleiso e isHom+ comm⋆) = e , isHom+ , comm⋆
  inv LeftModuleEquivStrΣPath (e , isHom+ , comm⋆) = moduleiso e isHom+ comm⋆
  rightInv LeftModuleEquivStrΣPath _ = refl
  leftInv LeftModuleEquivStrΣPath _ = refl

  LeftModulePath : (M N : LeftModule R) → (LeftModuleEquiv M N) ≃ (M ≡ N)
  LeftModulePath M N =
    LeftModuleEquiv M N                                    ≃⟨ isoToEquiv LeftModuleEquivStrΣPath ⟩
    LeftModuleEquivStrΣ M N                                   ≃⟨ LeftModuleΣPath _ _ ⟩
    LeftModule→LeftModuleΣ M ≡ LeftModule→LeftModuleΣ N  ≃⟨ isoToEquiv
                                                             (invIso
                                                             (congIso
                                                             LeftModuleIsoLeftModuleΣ))
                                                           ⟩
    M ≡ N ■

LeftModulePath : {R : Ring {ℓ}} (M N : LeftModule R) → (LeftModuleEquiv M N) ≃ (M ≡ N)
LeftModulePath {ℓ} {R} = LeftModuleΣTheory.LeftModulePath R

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Highlighting where

Set-one : Set₂
Set-one = Set₁

record R (A : Set) : Set-one where
  constructor con

  field X : Set

  F : Set → Set → Set
  F A B = B

  field P : F A X → Set

  Q : F A X → Set
  Q = Q

postulate P : _

open import Highlighting.M

data D (A : Set) : Set-one where
  d : let X = D in X A

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Categories.Adjoint.Equivalence where

open import Level

open import Categories.Adjoint
open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃ using (_≃_; NaturalIsomorphism)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
import Categories.Morphism.Reasoning as MR

open import Relation.Binary using (Setoid; IsEquivalence)

private
  variable
    o ℓ e    : Level
    o′ ℓ′ e′ : Level
    C D E    : Category o ℓ e

infix 5 _⊣⊢_

record _⊣⊢_ (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
  field
    unit   : idF ≃ (R ∘F L)
    counit : (L ∘F R) ≃ idF

  module unit   = NaturalIsomorphism unit
  module counit = NaturalIsomorphism counit

  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R

  field
    zig : ∀ {A : C.Obj} → counit.⇒.η (L.₀ A) D.∘ L.₁ (unit.⇒.η A) D.≈ D.id
    zag : ∀ {B : D.Obj} → R.₁ (counit.⇒.η B) C.∘ unit.⇒.η (R.₀ B) C.≈ C.id

  op₁ : R.op ⊣⊢ L.op
  op₁ = record
    { unit   = counit.op
    ; counit = unit.op
    ; zig    = zag
    ; zag    = zig
    }

  zag⁻¹ : {B : D.Obj} → unit.⇐.η (R.F₀ B) C.∘ R.F₁ (counit.⇐.η B) C.≈ C.id
  zag⁻¹ {B} = begin
    unit.⇐.η (R.₀ B) C.∘ R.₁ (counit.⇐.η B)   ≈˘⟨ flip-fromʳ unit.FX≅GX zag ⟩∘⟨refl ⟩
    R.₁ (counit.⇒.η B) C.∘ R.₁ (counit.⇐.η B) ≈⟨ [ R ]-resp-∘ (counit.iso.isoʳ B) ⟩
    R.₁ D.id                                  ≈⟨ R.identity ⟩
    C.id                                      ∎
    where open C.HomReasoning
          open MR C

  zig⁻¹ : {A : C.Obj} → L.F₁ (unit.⇐.η A) D.∘ counit.⇐.η (L.F₀ A) D.≈ D.id
  zig⁻¹ {A} = begin
      L.₁ (unit.⇐.η A) D.∘ counit.⇐.η (L.₀ A) ≈˘⟨ refl⟩∘⟨ flip-fromˡ counit.FX≅GX zig ⟩
      L.₁ (unit.⇐.η A) D.∘ L.₁ (unit.⇒.η A)   ≈⟨ [ L ]-resp-∘ (unit.iso.isoˡ A) ⟩
      L.₁ C.id                                ≈⟨ L.identity ⟩
      D.id                                    ∎
      where open D.HomReasoning
            open MR D

  op₂ : R ⊣⊢ L
  op₂ = record
    { unit   = ≃.sym counit
    ; counit = ≃.sym unit
    ; zig    = zag⁻¹
    ; zag    = zig⁻¹
    }

  L⊣R : L ⊣ R
  L⊣R = record
    { unit   = unit.F⇒G
    ; counit = counit.F⇒G
    ; zig    = zig
    ; zag    = zag
    }

  module L⊣R = Adjoint L⊣R
  open L⊣R hiding (unit; counit; zig; zag; op) public

  R⊣L : R ⊣ L
  R⊣L = record
    { unit   = counit.F⇐G
    ; counit = unit.F⇐G
    ; zig    = zag⁻¹
    ; zag    = zig⁻¹
    }

  module R⊣L = Adjoint R⊣L

private

  record WithZig (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
    field
      unit   : idF ≃ (R ∘F L)
      counit : (L ∘F R) ≃ idF

    module unit   = NaturalIsomorphism unit
    module counit = NaturalIsomorphism counit

    private
      module C = Category C
      module D = Category D
      module L = Functor L
      module R = Functor R
      module ℱ = Functor

    field
      zig : ∀ {A : C.Obj} → counit.⇒.η (L.₀ A) D.∘ L.₁ (unit.⇒.η A) D.≈ D.id

    zag : ∀ {B : D.Obj} → R.₁ (counit.⇒.η B) C.∘ unit.⇒.η (R.₀ B) C.≈ C.id
    zag {B} = F≃id⇒id (≃.sym unit) helper
      where open C
            open HomReasoning
            helper : R.₁ (L.₁ (R.₁ (counit.⇒.η B) ∘ unit.⇒.η (R.₀ B))) ≈ id
            helper = begin
              R.₁ (L.₁ (R.₁ (counit.⇒.η B) ∘ unit.⇒.η (R.₀ B)))             ≈⟨ ℱ.homomorphism (R ∘F L) ⟩
              R.₁ (L.₁ (R.₁ (counit.⇒.η B))) ∘ R.₁ (L.₁ (unit.⇒.η (R.₀ B))) ≈˘⟨ R.F-resp-≈ (F≃id-comm₁ counit) ⟩∘⟨refl ⟩
              R.₁ (counit.⇒.η (L.₀ (R.₀ B))) ∘ R.₁ (L.₁ (unit.⇒.η (R.₀ B))) ≈⟨ [ R ]-resp-∘ zig ⟩
              R.₁ D.id                                                      ≈⟨ R.identity ⟩
              id                                                            ∎

  record WithZag (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
    field
      unit   : idF ≃ (R ∘F L)
      counit : (L ∘F R) ≃ idF

    module unit   = NaturalIsomorphism unit
    module counit = NaturalIsomorphism counit

    private
      module C = Category C
      module D = Category D
      module L = Functor L
      module R = Functor R
      module ℱ = Functor

    field
      zag : ∀ {B : D.Obj} → R.₁ (counit.⇒.η B) C.∘ unit.⇒.η (R.₀ B) C.≈ C.id

    zig : ∀ {A : C.Obj} → counit.⇒.η (L.₀ A) D.∘ L.₁ (unit.⇒.η A) D.≈ D.id
    zig {A} = F≃id⇒id counit helper
      where open D
            open HomReasoning
            helper : L.₁ (R.₁ (counit.⇒.η (L.₀ A) ∘ L.₁ (unit.⇒.η A))) ≈ id
            helper = begin
              L.₁ (R.₁ (counit.⇒.η (L.₀ A) ∘ L.₁ (unit.⇒.η A)))               ≈⟨ ℱ.homomorphism (L ∘F R) ⟩
              (L.₁ (R.₁ (counit.⇒.η (L.₀ A))) ∘ L.₁ (R.₁ (L.₁ (unit.⇒.η A)))) ≈˘⟨ refl⟩∘⟨ L.F-resp-≈ (F≃id-comm₂ (≃.sym unit)) ⟩
              L.₁ (R.₁ (counit.⇒.η (L.₀ A))) ∘ L.₁ (unit.⇒.η (R.₀ (L.₀ A)))   ≈⟨ [ L ]-resp-∘ zag ⟩
              L.₁ C.id                                                       ≈⟨ L.identity ⟩
              id                                                              ∎

module _ {L : Functor C D} {R : Functor D C} where

  withZig : WithZig L R → L ⊣⊢ R
  withZig LR = record
    { unit   = unit
    ; counit = counit
    ; zig    = zig
    ; zag    = zag
    }
    where open WithZig LR

  withZag : WithZag L R → L ⊣⊢ R
  withZag LR = record
    { unit   = unit
    ; counit = counit
    ; zig    = zig
    ; zag    = zag
    }
    where open WithZag LR

id⊣⊢id : idF {C = C} ⊣⊢ idF
id⊣⊢id {C = C} = record
  { unit   = ≃.sym ≃.unitor²
  ; counit = ≃.unitor²
  ; zig    = identity²
  ; zag    = identity²
  }
  where open Category C

module _ {L : Functor C D} {R : Functor D C} {L′ : Functor D E} {R′ : Functor E D}
         (L⊣⊢R : L ⊣⊢ R) (L′⊣⊢R′ : L′ ⊣⊢ R′) where
  private
    module C   = Category C
    module D   = Category D
    module E   = Category E
    module L   = Functor L
    module R   = Functor R
    module L′  = Functor L′
    module R′  = Functor R′
    module ⊣⊢₁ = _⊣⊢_ L⊣⊢R
    module ⊣⊢₂ = _⊣⊢_ L′⊣⊢R′

    unit : idF ≃ (R ∘F R′) ∘F L′ ∘F L
    unit = record
      { F⇒G = ntHelper record
        { η       = λ c → R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ ⊣⊢₁.unit.⇒.η c
        ; commute = λ {x} {y} f → begin
          (R.₁ (⊣⊢₂.unit.⇒.η (L.₀ y)) ∘ ⊣⊢₁.unit.⇒.η y) ∘ f
            ≈⟨ pullʳ (⊣⊢₁.unit.⇒.commute f) ⟩
          R.₁ (⊣⊢₂.unit.⇒.η (L.₀ y)) ∘ R.₁ (L.₁ f) ∘ ⊣⊢₁.unit.⇒.η x
            ≈⟨ pullˡ ([ R ]-resp-square (⊣⊢₂.unit.⇒.commute (L.₁ f))) ⟩
          (R.₁ (R′.₁ (L′.₁ (L.₁ f))) ∘ R.₁ (⊣⊢₂.unit.⇒.η (L.₀ x))) ∘ ⊣⊢₁.unit.⇒.η x
            ≈⟨ assoc ⟩
          R.₁ (R′.₁ (L′.₁ (L.₁ f))) ∘ R.₁ (⊣⊢₂.unit.⇒.η (L.₀ x)) ∘ ⊣⊢₁.unit.⇒.η x
            ∎
        }
      ; F⇐G = ntHelper record
        { η       = λ c → ⊣⊢₁.unit.⇐.η c ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
        ; commute = λ {x} {y} f → begin
          (⊣⊢₁.unit.⇐.η y ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ y))) ∘ R.₁ (R′.₁ (L′.₁ (L.₁ f)))
            ≈⟨ pullʳ ([ R ]-resp-square (⊣⊢₂.unit.⇐.commute (L.₁ f))) ⟩
          ⊣⊢₁.unit.⇐.η y ∘ R.₁ (L.₁ f) ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ x))
            ≈⟨ pullˡ (⊣⊢₁.unit.⇐.commute f) ⟩
          (f ∘ ⊣⊢₁.unit.⇐.η x) ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ x))
            ≈⟨ assoc ⟩
          f ∘ ⊣⊢₁.unit.⇐.η x ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ x))
            ∎
        }
      ; iso = λ c → record
        { isoˡ = begin
          (⊣⊢₁.unit.⇐.η c ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))) ∘ R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ ⊣⊢₁.unit.⇒.η c
            ≈⟨ center ([ R ]-resp-∘ (⊣⊢₂.unit.iso.isoˡ (L.₀ c))) ⟩
          ⊣⊢₁.unit.⇐.η c ∘ R.₁ D.id ∘ ⊣⊢₁.unit.⇒.η c
            ≈⟨ refl⟩∘⟨ elimˡ R.identity ⟩
          ⊣⊢₁.unit.⇐.η c ∘ ⊣⊢₁.unit.⇒.η c
            ≈⟨ ⊣⊢₁.unit.iso.isoˡ c ⟩
          id
            ∎
        ; isoʳ = begin
          (R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ ⊣⊢₁.unit.⇒.η c) ∘ ⊣⊢₁.unit.⇐.η c ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
            ≈⟨ center (⊣⊢₁.unit.iso.isoʳ c) ⟩
          R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ id ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
            ≈⟨ refl⟩∘⟨ identityˡ ⟩
          R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ R.₁ (⊣⊢₂.unit.⇐.η (L.₀ c))
            ≈⟨ [ R ]-resp-∘ (⊣⊢₂.unit.iso.isoʳ (L.₀ c)) ⟩
          R.₁ D.id
            ≈⟨ R.identity ⟩
          id
            ∎
        }
      }
      where open C
            open HomReasoning
            open MR C

    module unit = NaturalIsomorphism unit

    counit : (L′ ∘F L) ∘F R ∘F R′ ≃ idF
    counit = record
      { F⇒G = ntHelper record
        { η       = λ e → ⊣⊢₂.counit.⇒.η e ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
        ; commute = λ {x} {y} f → begin
          (⊣⊢₂.counit.⇒.η y ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ y))) ∘ L′.₁ (L.₁ (R.₁ (R′.₁ f)))
            ≈⟨ pullʳ ([ L′ ]-resp-square (⊣⊢₁.counit.⇒.commute (R′.₁ f))) ⟩
          ⊣⊢₂.counit.⇒.η y ∘ L′.₁ (R′.₁ f) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ x))
            ≈⟨ pullˡ (⊣⊢₂.counit.⇒.commute f) ⟩
          (f ∘ ⊣⊢₂.counit.⇒.η x) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ x))
            ≈⟨ assoc ⟩
          f ∘ ⊣⊢₂.counit.⇒.η x ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ x))
            ∎
        }
      ; F⇐G = ntHelper record
        { η       = λ e → L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ ⊣⊢₂.counit.⇐.η e
        ; commute = λ {x} {y} f → begin
          (L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ y)) ∘ ⊣⊢₂.counit.⇐.η y) ∘ f
            ≈⟨ pullʳ (⊣⊢₂.counit.⇐.commute f) ⟩
          L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ y)) ∘ L′.₁ (R′.₁ f) ∘ ⊣⊢₂.counit.⇐.η x
            ≈⟨ pullˡ ([ L′ ]-resp-square (⊣⊢₁.counit.⇐.commute (R′.₁ f))) ⟩
          (L′.₁ (L.₁ (R.₁ (R′.₁ f))) ∘ L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ x))) ∘ ⊣⊢₂.counit.⇐.η x
            ≈⟨ assoc ⟩
          L′.₁ (L.₁ (R.₁ (R′.₁ f))) ∘ L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ x)) ∘ ⊣⊢₂.counit.⇐.η x
            ∎
        }
      ; iso = λ e → record
        { isoˡ = begin
          (L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ ⊣⊢₂.counit.⇐.η e) ∘ ⊣⊢₂.counit.⇒.η e ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
            ≈⟨ center (⊣⊢₂.counit.iso.isoˡ e) ⟩
          L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ id ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
            ≈⟨ refl⟩∘⟨ identityˡ ⟩
          L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))
            ≈⟨ [ L′ ]-resp-∘ (⊣⊢₁.counit.iso.isoˡ (R′.₀ e)) ⟩
          L′.₁ D.id
            ≈⟨ L′.identity ⟩
          id
            ∎
        ; isoʳ = begin
          (⊣⊢₂.counit.⇒.η e ∘ L′.₁ (⊣⊢₁.counit.⇒.η (R′.₀ e))) ∘ L′.₁ (⊣⊢₁.counit.⇐.η (R′.₀ e)) ∘ ⊣⊢₂.counit.⇐.η e
            ≈⟨ center ([ L′ ]-resp-∘ (⊣⊢₁.counit.iso.isoʳ (R′.₀ e))) ⟩
          ⊣⊢₂.counit.⇒.η e ∘ L′.₁ D.id ∘ ⊣⊢₂.counit.⇐.η e
            ≈⟨ refl⟩∘⟨ elimˡ L′.identity ⟩
          ⊣⊢₂.counit.⇒.η e ∘ ⊣⊢₂.counit.⇐.η e
            ≈⟨ ⊣⊢₂.counit.iso.isoʳ e ⟩
          id
            ∎
        }
      }
      where open E
            open HomReasoning
            open MR E

    module counit = NaturalIsomorphism counit

    zig : ∀ {c} → counit.⇒.η (L′.₀ (L.₀ c)) E.∘ L′.₁ (L.₁ (unit.⇒.η c)) E.≈ E.id
    zig {c} = begin
      counit.⇒.η (L′.₀ (L.₀ c)) ∘ L′.₁ (L.₁ (unit.⇒.η c))
        ≈⟨ refl⟩∘⟨ Functor.homomorphism (L′ ∘F L) ⟩
      counit.⇒.η (L′.₀ (L.₀ c)) ∘ L′.₁ (L.₁ (R.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)))) ∘ L′.₁ (L.₁ (⊣⊢₁.unit.⇒.η c))
        ≈⟨ center ([ L′ ]-resp-square (⊣⊢₁.counit.⇒.commute (⊣⊢₂.unit.⇒.η (L.₀ c)))) ⟩
      ⊣⊢₂.counit.⇒.η (L′.₀ (L.₀ c)) ∘ (L′.₁ (⊣⊢₂.unit.⇒.η (L.₀ c)) ∘ L′.₁ (⊣⊢₁.counit.⇒.η (L.₀ c))) ∘ L′.₁ (L.₁ (⊣⊢₁.unit.⇒.η c))
        ≈⟨ pull-first ⊣⊢₂.zig ⟩
      id ∘ L′.₁ (⊣⊢₁.counit.⇒.η (L.₀ c)) ∘ L′.₁ (L.₁ (⊣⊢₁.unit.⇒.η c))
        ≈⟨ elimʳ (([ L′ ]-resp-∘ ⊣⊢₁.zig) ○ L′.identity) ⟩
      id
        ∎
      where open E
            open HomReasoning
            open MR E

  _∘⊣⊢_ : (L′ ∘F L) ⊣⊢ (R ∘F R′)
  _∘⊣⊢_ = withZig record
    { unit   = unit
    ; counit = counit
    ; zig    = zig
    }

record ⊣Equivalence (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    L    : Functor C D
    R    : Functor D C
    L⊣⊢R : L ⊣⊢ R

  module L    = Functor L
  module R    = Functor R
  module L⊣⊢R = _⊣⊢_ L⊣⊢R

  open L⊣⊢R public

refl : ⊣Equivalence C C
refl = record
  { L    = idF
  ; R    = idF
  ; L⊣⊢R = id⊣⊢id
  }

sym : ⊣Equivalence C D → ⊣Equivalence D C
sym e = record
  { L    = R
  ; R    = L
  ; L⊣⊢R = op₂
  }
  where open ⊣Equivalence e

trans : ⊣Equivalence C D → ⊣Equivalence D E → ⊣Equivalence C E
trans e e′ = record
  { L    = e′.L ∘F e.L
  ; R    = e.R ∘F e′.R
  ; L⊣⊢R = e.L⊣⊢R ∘⊣⊢ e′.L⊣⊢R
  }
  where module e  = ⊣Equivalence e
        module e′ = ⊣Equivalence e′

isEquivalence : ∀ {o ℓ e} → IsEquivalence (⊣Equivalence {o} {ℓ} {e})
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : ∀ o ℓ e → Setoid _ _
setoid o ℓ e = record
  { Carrier       = Category o ℓ e
  ; _≈_           = ⊣Equivalence
  ; isEquivalence = isEquivalence
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Empty
open import Data.Product
open import Data.List using ([]; _∷_; _++_)

open import Relation.Nullary
open import Relation.Unary using (_⊆_)
open import Relation.Nullary.Negation using (contraposition)

open import Common

module TraceInclusion {ℙ : Set} (message : Message ℙ)
  where

open import Trace message
open import SessionType message
open import Transitions message
open import Session message
open import HasTrace message
open import TraceSet message

TraceInclusionS : SessionType -> SessionType -> Set
TraceInclusionS T S = ⟦ T ⟧ ⊆ ⟦ S ⟧

TraceExclusionS : SessionType -> SessionType -> Set
TraceExclusionS T S = ∃[ φ ] (T HasTrace φ × ¬ S HasTrace φ)

nil<=any : ∀{T} -> TraceInclusionS nil T
nil<=any (_ , () , refl)
nil<=any (_ , _ , step () _)

end<=def : ∀{T S} -> End T -> Defined S -> TraceInclusionS T S
end<=def e def (_ , tdef , refl) = _ , def , refl
end<=def (inp U) _ (_ , tdef , step inp tr) = ⊥-elim (U _ (transitions+defined->defined tr tdef))
end<=def (out U) _ (_ , tdef , step (out !x) _) = ⊥-elim (U _ !x)

inclusion-preserves-success : ∀{T S} -> TraceInclusionS T S -> ImplyS MaySucceed T S
inclusion-preserves-success spec ((R' # T') , reds , win#def w def) =
  let as , rr , tr = unzip-red* reds in
  let (S' , def' , sr) = spec (_ , def , tr) in
  _ , zip-red* rr sr , win#def w def'

input-excluded-trace :
  ∀{f : Continuation}{x as}
  (ntr : ¬ inp f HasTrace (I x ∷ as)) ->
  ¬ f x .force HasTrace as
input-excluded-trace ntr (_ , def , tr) = ntr (_ , def , step inp tr)

output-excluded-trace :
  ∀{f x as}
  (ntr : ¬ out f HasTrace (O x ∷ as)) ->
  ¬ f x .force HasTrace as
output-excluded-trace {f} {x} ntr (_ , def , tr) with x ∈? f
... | yes fx = ntr (_ , def , step (out fx) tr)
output-excluded-trace {_} {_} _ (_ , def , refl) | no nfx = ⊥-elim (nfx def)
output-excluded-trace {_} {_} _ (_ , _ , step t _) | no nfx = ⊥-elim (nfx (transition->defined t))

has-trace-input : ∀{f x as} -> inp f HasTrace (I x ∷ as) -> f x .force HasTrace as
has-trace-input (_ , def , step inp tr) = _ , def , tr

has-trace-output : ∀{f x as} -> out f HasTrace (O x ∷ as) -> f x .force HasTrace as
has-trace-output (_ , def , step (out _) tr) = _ , def , tr

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
mutual

  record R : Set₁ where
    field
      A : Set

    B : Set
    B = A

    field
      C : Set

    D : Set
    D = A → B → C

  record S : Set₁ where
    field
      A : Set

    B : Set
    B = A

    field
      C : Set

    D : Set
    D = A → B → C

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module plfa-exercises.Practice2 where

-- Trying exercises:
-- 5.2 pp 340
-- 5.7 pp 386
-- 6.1 pp 423

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; subst)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
--open import plfa.part1.Isomorphism using (_≃_; extensionality)

∀-elim : ∀ {A : Set} {B : A → Set} → (L : ∀ (x : A) → B x) → (M : A) → B M
∀-elim l m = l m

--totype : ℕ → Set
--totype 0 = ℕ
--totype 1 = 4 ≡ 2 + 2
--totype _ = ℕ

-- λ noidea → ∀-elim {ℕ} {totype} noidea 4

------- Preliminary proofs -------
modus-tollens : ∀ {A B : Set}
  → (A → B)
  -------------
  → (¬ B → ¬ A)
modus-tollens a→b = λ{¬b → λ{a → ¬b (a→b a)}}
----------------------------------

postulate
  dne : ∀ {A : Set} → ¬ ¬ A → A

--data Σ (A : Set) (B : A → Set) : Set where
--  ⟨_,_⟩ : (x : A) → B x → Σ A B
--
--Σ-syntax = Σ
--infix 2 Σ-syntax
--syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
--
--∃ : ∀ {A : Set} (B : A → Set) → Set
--∃ {A} B = Σ A B
--
--∃-syntax = ∃
--syntax ∃-syntax (λ x → B) = ∃[ x ] B

--⟨,⟩-syntax : ∀ {A : Set} {B : A → Set} (x : A) → B x → Σ A B
--⟨,⟩-syntax = ⟨_,_⟩
----⟨,⟩-syntax = Σ.⟨_,_⟩
--syntax ⟨,⟩-syntax x p = the-proof-for x is p

--∃-elim : ∀ {A : Set} {B : A → Set} {C : Set}
--  → (∀ x → B x → C)
--  → ∃[ x ] B x
--    ---------------
--  → C
--∃-elim f ⟨ x , y ⟩ = f x y

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

---------------------- Athena book exercises ----------------------

exercise531 : ∀ {A : Set} {R : A → A → Set}
            → (∀ (x y : A) → R x y)
            → (∀ (x : A) → R x x)
exercise531 R x = R x x

exercise532 : ∀ {A : Set} (x : A) → ∃[ y ] (x ≡ y)
exercise532 e = ⟨ e , refl ⟩

exercise533 : ∀ {A : Set} {P Q S : A → Set}
            → (∀ {x} → (P x ⊎ Q x) → S x)
            → (∃[ y ] (Q y))
            -------------------------
            → (∃[ y ] (S y))
exercise533 Px⊎Qx→Sx ⟨ y , qy ⟩ =
  let
    -- P x ⊎ Q x
    py⊎qy = inj₂ qy
  in ⟨ y , Px⊎Qx→Sx py⊎qy ⟩

exercise534 : ∀ {A : Set} {P Q S : A → Set}
            → (∃[ y ] (P y × Q y))
            → (∀ {y} → P y → S y)
            -------------------------
            → (∃[ y ] (S y × Q y))
exercise534 ⟨ y , ⟨ py , qy ⟩ ⟩ py→sy = ⟨ y , ⟨ py→sy py , qy ⟩ ⟩

exercise535 : ∀ {A : Set} {P Q : A → Set}
            → (¬ ∃[ x ] (Q x))
            → (∀ {x} → P x → Q x)
            -------------------------
            → (¬ ∃[ x ] (P x))
exercise535 ¬∃x-qx ∀x→px→qx = λ{ ∃x-px@(⟨ x , px ⟩) → ¬∃x-qx ⟨ x , ∀x→px→qx px ⟩ }

exercise536 : ∀ {A : Set} {P Q S : A → Set}
            → (∀ {y} → P y → Q y)
            → (∃[ y ] (S y × ¬ Q y))
            ------------------------
            → (∃[ y ] (S y × ¬ P y))
exercise536 ∀y→py→qy ⟨ y , ⟨ sy , ¬qy ⟩ ⟩ = ⟨ y , ⟨ sy , modus-tollens ∀y→py→qy ¬qy ⟩ ⟩

exercise537 : ∀ {A : Set} {P Q : A → Set} {R : A → A → Set}
            → (∀ {x} → R x x → P x)
            → (∃[ x ] (P x) → ¬ ∃[ x ] (Q x))
            -------------------------------
            → ((∀ {x} → Q x) → ¬ ∃[ x ] (R x x))
exercise537 ∀x→rxx→px ∃x-px→¬∃x-qx ∀x→qx = λ{∃x-rxx@(⟨ x , rxx ⟩) → ∃x-px→¬∃x-qx ⟨ x , ∀x→rxx→px rxx ⟩ ⟨ x , ∀x→qx {x} ⟩ }

exercise538 : ∀ {A : Set} {P Q : A → Set}
            → (∃[ x ] (P x ⊎ Q x)) ⇔ (∃[ x ] (P x) ⊎ ∃[ x ] (Q x))
exercise538 = record { to = to ; from = from }
  where
  to : ∀ {A : Set} {P Q : A → Set}
     → ∃[ x ] (P x ⊎ Q x)
     -----------------------------
     → ∃[ x ] (P x) ⊎ ∃[ x ] (Q x)
  to ⟨ x , (inj₁ px) ⟩ = inj₁ ⟨ x , px ⟩
  to ⟨ x , (inj₂ qx) ⟩ = inj₂ ⟨ x , qx ⟩

  from : ∀ {A : Set} {P Q : A → Set}
       → ∃[ x ] (P x) ⊎ ∃[ x ] (Q x)
       -----------------------------
       → ∃[ x ] (P x ⊎ Q x)
  from (inj₁ ⟨ x , px ⟩) = ⟨ x , inj₁ px ⟩
  from (inj₂ ⟨ x , qx ⟩) = ⟨ x , inj₂ qx ⟩

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

exercise571 : ∀ {A : Set} {P Q : A → Set}
            → (∀ {x} → P x ⇔ Q x)
            → (∀ {x} → P x) ⇔ (∀ {x} → Q x)
exercise571 px⇔qx =
  record
  { to   = λ{px → (_⇔_.to   px⇔qx) px}
  ; from = λ{qx → (_⇔_.from px⇔qx) qx}
  }
--exercise571 ∀x→px⇔qx =
--  record
--  { to   = λ{∀x→px →  (_⇔_.to   (∀x→px⇔qx {x})) (∀x→px {x})}
--  ; from = λ{∀x→qx →  (_⇔_.from (∀x→px⇔qx {x})) (∀x→qx {x})}
--  }

exercise572 : ∀ {A : Set} {B : Set} {Q S : B → Set} {R T : B → B → Set}
            → (∃[ y ] (R y y × A))
            → (∃[ y ] (Q y × T y y))
            → (∀ y → A × Q y → ¬ S y)
            → (∃[ y ] (¬ S y × T y y))
exercise572 ⟨ _ , ⟨ _ , a ⟩ ⟩ ⟨ y , ⟨ qy , tyy ⟩ ⟩ ∀y→a×qy→¬sy = ⟨ y , ⟨ ∀y→a×qy→¬sy y ⟨ a , qy ⟩ , tyy ⟩ ⟩

-- This is fucking false!!!
--postulate
--  existence : {A : Set} {P : A → Set}
--            → (∀ x → P x)
--            ----------------
--            → (∃[ x ] (P x))

-- This cannot be proved! Take the empty set as an example. For any function
-- and relation the ∀'s are trivially true, but there is no element that
-- actually fulfills the function or the relation
--exercise574 : ∀ {A : Set} {F : A → A} {R : A → A → Set}
--            → (∀ x → R x x)
--            → (∀ x → F x ≡ F (F x))
--            -----------------------
--            → (∃[ y ] (R y (F y)))
--exercise574 ∀x→rxx ∀x→fx≡ffx = ⟨ ? , ? ⟩

exercise574 : ∀ {F : ℕ → ℕ} {R : ℕ → ℕ → Set}
            → (∀ x → R x x)
            → (∀ x → F x ≡ F (F x))
            -----------------------
            → (∃[ y ] (R y (F y)))
exercise574 {f} {r} ∀x→rxx ∀x→fx≡ffx =
  let y    = f 0
      y≡fy = ∀x→fx≡ffx 0          -- F 0 ≡ F (F 0)     =>  y ≡ F y
      ryy  = ∀x→rxx y             -- R (F 0) (F 0)     =>  R y y
      ryfy = subst (r y) y≡fy ryy -- R (F 0) (F (F 0)) =>  R y (F y)
  in ⟨ y , ryfy ⟩

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

exercise61a : ∀ {A B : Set}
            → (B ⊎ (A → B))
            → A
            ---------------
            → B
exercise61a (inj₁ b)   _ = b
exercise61a (inj₂ a→b) a = a→b a

exercise61b : ∀ {A B C : Set}
            → (¬ B → ¬ C)
            → ((A × B) ⊎ ¬ ¬ C)
            -------------------
            → B
exercise61b ¬b→¬c (inj₁ ⟨ a , b ⟩) = b
exercise61b ¬b→¬c (inj₂ ¬¬c) = dne ((modus-tollens ¬b→¬c) ¬¬c)

¬¬ : ∀ {A : Set}
   → A
   → ¬ ¬ A
¬¬ a = λ{¬a → ¬a a}

-- What is the difference between: ∀ x → P x → ∀ y → R y → L  and  (∀ x → P x) → (∀ y → R y) → L

---- Can the following be proved without Double Negation Elimination (dne)?
--lemma₁ : ∀ {A B : Set}
--       → (¬ B → ¬ A)
--       → A
--       -------------------
--       → B
--lemma₁ = ?
--
--lemma₂ : ∀ {A B : Set}
--       → (¬ B → ¬ A)
--       → ¬ ¬ A
--       -------------------
--       → B
--lemma₂ = ?
--
---- `lemma₁` seems not to imply `dne` but it can't be proven without it.
----
---- The answer is NO (for the second one)! Because from it we can prove `dne`!
---- `dne` cannot be proved in vanila Agda.
--dne₁ : ∀ {A : Set} → ¬ ¬ A → A
--dne₁ ¬¬a = lemma₁ ? ?
--
--dne₂ : ∀ {A : Set} → ¬ ¬ A → A
--dne₂ ¬¬a = lemma₂ (λ{x → x}) ¬¬a


text: open import Issue623.B


text:
-- Soundness of term equality
module Semantics.Soundness where

open import Syntax.Types
open import Syntax.Context renaming (_,_ to _,,_)
open import Syntax.Terms
open import Syntax.Equality
open import Syntax.Substitution

open import Semantics.Types
open import Semantics.Context
open import Semantics.Terms
open import Semantics.Substitution
open import Semantics.Bind

open import CategoryTheory.Categories using (ext)
open import CategoryTheory.BCCCs.Cartesian using (Product)
open import CategoryTheory.BCCCs
open import CategoryTheory.Instances.Reactive renaming (top to Top)
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import TemporalOps.Diamond
open import TemporalOps.OtherOps

open import Data.Sum
open import Data.Product using (_,_ ; proj₁ ; proj₂)
open import Relation.Binary.PropositionalEquality as ≡
    using (_≡_ ; refl ; sym ; trans ; cong ; cong₂ ; subst)

open ≡.≡-Reasoning
open Monad M-◇
open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

open ⟦Kit⟧ ⟦𝒯erm⟧
open Kit 𝒯erm
open ⟦K⟧ ⟦𝒯erm⟧
open K 𝒯erm

mutual
    -- Soundness of term equality: equal terms have equal denotations
    sound : ∀{A Γ} {M₁ M₂ : Γ ⊢ A}
             -> Γ ⊢ M₁ ≡ M₂ ∷ A
             -> ⟦ M₁ ⟧ₘ ≈ ⟦ M₂ ⟧ₘ
    sound (refl M) = refl
    sound (Eq.sym eq) = ≡.sym (sound eq)
    sound (Eq.trans eq₁ eq₂) = ≡.trans (sound eq₁) (sound eq₂)

    sound (β-lam N M) {n} {⟦Γ⟧} rewrite subst-sound M N {n} {⟦Γ⟧} = refl
    sound (β-fst M N) = refl
    sound (β-snd M N) = refl
    sound (β-inl M N₁ N₂) {n} {⟦Γ⟧} rewrite subst-sound M N₁ {n} {⟦Γ⟧} = refl
    sound (β-inr M N₁ N₂) {n} {⟦Γ⟧} rewrite subst-sound M N₂ {n} {⟦Γ⟧} = refl
    sound (β-sig N M) {n} {⟦Γ⟧} rewrite subst-sound M N {n} {⟦Γ⟧} = refl

    sound (η-lam {A} M) {n} {⟦Γ⟧} = ext λ ⟦A⟧ →
                        cong (λ x → x ⟦A⟧) (≡.sym (⟦𝓌⟧ (A now) M {n} {⟦Γ⟧ , ⟦A⟧}))
    sound (η-pair M) = ≡.sym (⊗-η-exp {m = ⟦ M ⟧ₘ})
    sound (η-unit M) = refl
    sound (η-sum M) {n} {⟦Γ⟧} with ⟦ M ⟧ₘ n ⟦Γ⟧
    sound (η-sum M) {n} {a} | inj₁ _ = refl
    sound (η-sum M) {n} {a} | inj₂ _ = refl
    sound (η-sig M) = refl
    sound {Γ = Γ} (η-evt {A} M) {n} {a}
        rewrite bind-to->>= Γ (⟦ M ⟧ₘ) (η.at ⟦ A ⟧ₜ ∘ π₂) n a
              = ≡.sym (>>=-unit-right (⟦ M ⟧ₘ n a))

    sound (cong-pair eq₁ eq₂) {n} {a} rewrite sound eq₁ {n} {a}
                                            | sound eq₂ {n} {a} = refl
    sound (cong-fst eq) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-snd eq) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-lam eq) {n} {a} = ext λ ⟦A⟧ → sound eq
    sound (cong-app eq₁ eq₂) {n} {a} rewrite sound eq₁ {n} {a}
                                           | sound eq₂ {n} {a} = refl
    sound (cong-inl eq) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-inr eq) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-case eq N₁ N₂) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-sig eq) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-letSig eq N) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-sample eq) {n} {a} rewrite sound eq {n} {a} = refl
    sound (cong-stable eq) = ext λ k → sound eq
    sound (cong-event eq) {n} {a} rewrite sound′ eq {n} {a} = refl

    -- Soundness of computational term equality: equal terms have equal denotations
    sound′ : ∀{A Γ} {M₁ M₂ : Γ ⊨ A}
             -> Γ ⊨ M₁ ≡ M₂ ∷ A
             -> ⟦ M₁ ⟧ᵐ ≈ ⟦ M₂ ⟧ᵐ
    sound′ (refl M) = refl
    sound′ (Eq′.sym eq) = ≡.sym (sound′ eq)
    sound′ (Eq′.trans eq₁ eq₂) = ≡.trans (sound′ eq₁) (sound′ eq₂)
    sound′ (β-sig′ C M) {n} {⟦Γ⟧} rewrite subst′-sound M C {n} {⟦Γ⟧} = refl
    sound′ (β-evt′ C D) {n} {⟦Γ⟧} rewrite subst″-sound D C {n} {⟦Γ⟧} = refl
    sound′ {_}{Γ} (β-selectₚ {A}{B}{C} C₁ C₂ C₃ M₁ M₂) {n} {⟦Γ⟧} =
        begin
            ⟦ select event (pure M₁) ↦ C₁ || event (pure M₂) ↦ C₂ ||both↦ C₃ ⟧ᵐ n ⟦Γ⟧
        ≡⟨⟩
            ⟦ C₃ ⟧ᵐ n ((⌞ ⟦ Γ ˢ⟧□ n ⟦Γ⟧ n ⌟ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) , ⟦ M₂ ⟧ₘ n ⟦Γ⟧)
        ≡⟨ cong! (⟦ˢ⟧-factor Γ {n} {⟦Γ⟧}) ⟩
            ⟦ C₃ ⟧ᵐ n ((⌞ ⟦ Γ ˢ⟧ n ⟦Γ⟧ ⌟ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) , ⟦ M₂ ⟧ₘ n ⟦Γ⟧)
        ≡⟨ cong! (⟦subst⟧-Γˢ⊆Γ Γ {n} {⟦Γ⟧}) ⟩
            ⟦ C₃ ⟧ᵐ n (⌞ (⟦subst⟧ (Γˢ⊆Γ Γ ⊆ₛ 𝒯erm) n ⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) ⌟ , ⟦ M₂ ⟧ₘ n ⟦Γ⟧ )
        ≡⟨ cong! (⟦↑⟧ (A now) (Γˢ⊆Γ Γ ⊆ₛ 𝒯erm) {n} {⟦Γ⟧ , (⟦ M₁ ⟧ₘ n ⟦Γ⟧)}) ⟩
            ⟦ C₃ ⟧ᵐ n ⌞ ((⟦subst⟧ (_↑_ {A now} (Γˢ⊆Γ Γ ⊆ₛ 𝒯erm) 𝒯erm) n (⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧)) , ⟦ M₂ ⟧ₘ n ⟦Γ⟧) ⌟
        ≡⟨ cong! (⟦↑⟧ (B now) (_↑_ {A now} (Γˢ⊆Γ Γ ⊆ₛ 𝒯erm) 𝒯erm) {n} {(⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) , (⟦ M₂ ⟧ₘ n ⟦Γ⟧)}) ⟩
            ⟦ C₃ ⟧ᵐ n (⟦subst⟧ (_↑_ {B now} (_↑_ {A now} (Γˢ⊆Γ Γ ⊆ₛ 𝒯erm) 𝒯erm) 𝒯erm) n ((⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) , ⌞ ⟦ M₂ ⟧ₘ n ⟦Γ⟧ ⌟))
        ≡⟨ cong! (⟦𝓌⟧ (A now) M₂ {n} {⟦Γ⟧ , (⟦ M₁ ⟧ₘ n ⟦Γ⟧)}) ⟩
            ⟦ C₃ ⟧ᵐ n (⟦subst⟧ (weakₛ 𝒯ermₛ s) n ((⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) , ⟦ 𝓌 M₂ ⟧ₘ n (⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧)))
        ≡⟨ ≡.sym (traverse′-sound ⟦𝒯erm⟧ (weakₛ 𝒯ermₛ s) C₃ {n} {(⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) , ⟦ 𝓌 M₂ ⟧ₘ n (⟦Γ⟧ , (⟦ M₁ ⟧ₘ n ⟦Γ⟧))})  ⟩
            ⟦ traverse′ (weakₛ 𝒯ermₛ s) C₃ ⟧ᵐ n ((⟦Γ⟧ , ⟦ M₁ ⟧ₘ n ⟦Γ⟧) , ⟦ 𝓌 M₂ ⟧ₘ n (⟦Γ⟧ , (⟦ M₁ ⟧ₘ n ⟦Γ⟧)))
        ≡⟨ ≡.sym (subst′-sound (𝓌 M₂) (weakening′ s C₃) {n} {⟦Γ⟧ , (⟦ M₁ ⟧ₘ n ⟦Γ⟧)}) ⟩
            ⟦ [ 𝓌 M₂ /′] (weakening′ s C₃) ⟧ᵐ n (⟦Γ⟧ , (⟦ M₁ ⟧ₘ n ⟦Γ⟧))
        ≡⟨ ≡.sym (subst′-sound M₁ ([ 𝓌 M₂ /′] (weakening′ s C₃)) {n} {⟦Γ⟧} ) ⟩
            ⟦ [ M₁ /′] ([ 𝓌 M₂ /′] (weakening′ s C₃)) ⟧ᵐ n ⟦Γ⟧
        ∎
        where
        s : Γ ˢ ,, A now ,, B now ⊆ Γ ,, A now ,, B now
        s = keep (keep (Γˢ⊆Γ Γ))
    sound′ (η-sig′ M) = refl
    sound′ (cong-pure′ eq) {n} {⟦Γ⟧} rewrite sound eq {n} {⟦Γ⟧} = refl
    sound′ (cong-letSig′ eq B) {n} {⟦Γ⟧} rewrite sound eq {n} {⟦Γ⟧} = refl
    sound′ (cong-letEvt′ eq D) {n} {⟦Γ⟧} rewrite sound eq {n} {⟦Γ⟧} = refl

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module _ where

postulate
  A B : Set

{-# DISPLAY A = B #-}
{-# DISPLAY B = A #-}

loop : A
loop = {!!}


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

open import LogicalFormulae
open import Decidable.Relations
open import Boolean.Definition

module Decidable.Reduction where

squash : {a b : _} {A : Set a} {f : A → Set b} → DecidableRelation f → A → Bool
squash rel a with rel a
... | inl x = BoolTrue
... | inr x = BoolFalse

unsquash : {a b : _} {A : Set a} {f : A → Set b} → (rel : DecidableRelation f) → {x : A} → .(squash rel x ≡ BoolTrue) → f x
unsquash rel {x} pr with rel x
... | inl ans = ans


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- All predicate transformer for fresh lists
------------------------------------------------------------------------

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

module Data.List.Fresh.Relation.Unary.All where

open import Level using (Level; _⊔_; Lift)
open import Data.Product using (_×_; _,_; proj₁; uncurry)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary  as U
open import Relation.Binary as B using (Rel)

open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)

private
  variable
    a p q r : Level
    A : Set a

module _ {A : Set a} {R : Rel A r} (P : Pred A p) where

  data All : List# A R → Set (p ⊔ a ⊔ r) where
    []  : All []
    _∷_ : ∀ {x xs pr} → P x → All xs → All (cons x xs pr)

module _ {R : Rel A r} {P : Pred A p} where

  uncons : ∀ {x} {xs : List# A R} {pr} →
           All P (cons x xs pr) → P x × All P xs
  uncons (p ∷ ps) = p , ps

module _ {R : Rel A r} where

  append   : (xs ys : List# A R) → All (_# ys) xs → List# A R
  append-# : ∀ {x} xs ys {ps} → x # xs → x # ys → x # append xs ys ps

  append []             ys _  = ys
  append (cons x xs pr) ys ps =
    let (p , ps) = uncons ps in
    cons x (append xs ys ps) (append-# xs ys pr p)

  append-# []             ys x#xs       x#ys = x#ys
  append-# (cons x xs pr) ys (r , x#xs) x#ys = r , append-# xs ys x#xs x#ys

module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} where

  map : ∀ {xs : List# A R} → ∀[ P ⇒ Q ] → All P xs → All Q xs
  map p⇒q []       = []
  map p⇒q (p ∷ ps) = p⇒q p ∷ map p⇒q ps

  lookup : ∀ {xs : List# A R} → All Q xs → (ps : Any P xs) →
           Q (proj₁ (Any.witness ps))
  lookup (q ∷ _)  (here _)  = q
  lookup (_ ∷ qs) (there k) = lookup qs k

module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where

  all? : (xs : List# A R) → Dec (All P xs)
  all? []        = yes []
  all? (x ∷# xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×-dec all? xs)


text:
module Data.Bit where

open import Data.Nat.Literal using (Number; ℕ-num; Fin-num)
open import Data.Nat using (ℕ ; suc; zero; ⌊_/2⌋)
                     renaming (_*_ to ℕ*; _+_ to ℕ+; _≤_ to ℕ≤; _^_ to ℕ^)
open import Data.Int.Literal using (Negative)
open import Data.Fin using (Fin; suc; zero; raise)
                     renaming (toℕ to finToℕ; fromℕ to finFromℕ)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Vec using (Vec; []; _∷_; _++_; replicate; insert; head; tail)
                     renaming (map to mapVec)
open import Data.Unit using (⊤)
open import Data.Empty using (⊥)
open import Level using (_⊔_)
open import Data.Bool using (Bool; false; true) renaming (_∧_ to Bool-∧)
open import Data.Maybe using (Maybe; just; nothing; map)

record WithCarry {a} {c} (A : Set a) (C : Set c) : Set (a ⊔ c) where
  constructor _with-carry:_
  field
    result : A
    carry : C

open WithCarry public

record Overflowing {a} (A : Set a) : Set a where
  constructor _overflow:_
  field
    result : A
    overflow : Bool

open Overflowing public

data Bit : Set where
  b0 : Bit
  b1 : Bit

infixl 8 _-_ _+_
infixl 7 _<<_ _>>_
infixl 6 _∧_ _&_
infixl 5 _⊕_ _^_
infixl 4 _∨_ _~|_
infixl 3 _↔_ _==_
infixl 1 _with-carry:_

fromBool : Bool → Bit
fromBool false = b0
fromBool true = b1

toBool : Bit → Bool
toBool b0 = false
toBool b1 = true

! : Bit → Bit
! b0 = b1
! b1 = b0

_∧_ : Bit → Bit → Bit
b0 ∧ _ = b0
b1 ∧ q = q

_∨_ : Bit → Bit → Bit
b0 ∨ q = q
b1 ∨ _ = b1

_⊕_ : Bit → Bit → Bit
b0 ⊕ q = q
b1 ⊕ q = ! q

_↔_ : Bit → Bit → Bit
b0 ↔ q = ! q
b1 ↔ q = q

maj3 : Bit → Bit → Bit → Bit
maj3 p q r = p ∧ q ∨ p ∧ r ∨ q ∧ r

half-add : Bit → Bit → WithCarry Bit Bit
half-add p q = p ⊕ q with-carry: p ∧ q

full-add : Bit → Bit → Bit → WithCarry Bit Bit
full-add p q r = p ⊕ q ⊕ r with-carry: maj3 p q r

full-addₙ : {n : ℕ} →
            Vec Bit n →
            Vec Bit n →
            Bit →
            WithCarry (Vec Bit n) (Vec Bit 2)
full-addₙ [] [] r = [] with-carry: b0 ∷ r ∷ []
full-addₙ (p ∷ []) (q ∷ []) r = result s ∷ [] with-carry: r ∷ carry s ∷ [] where
  s = full-add p q r
full-addₙ (p ∷ ps) (q ∷ qs) r = result s ∷ result ss with-carry: carry ss  where
  s = full-add p q r
  ss = full-addₙ ps qs (carry s)

!ₙ : {n : ℕ} → Vec Bit n → Vec Bit n
!ₙ = mapVec !

_+_ : {n : ℕ} → Vec Bit n → Vec Bit n → WithCarry (Vec Bit n) (Vec Bit 2)
ps + qs = full-addₙ ps qs b0

_-_ : {n : ℕ} → Vec Bit n → Vec Bit n → WithCarry (Vec Bit n) (Vec Bit 2)
ps - qs = full-addₙ ps (!ₙ qs) b1

inc : {n : ℕ} → Vec Bit n → WithCarry (Vec Bit n) (Vec Bit 2)
inc ps = full-addₙ ps (replicate b0) b1

dec : {n : ℕ} → Vec Bit n → WithCarry (Vec Bit n) (Vec Bit 2)
dec ps = full-addₙ ps (replicate b1) b0

_>>_ : {m : ℕ} → Vec Bit m → Fin m → WithCarry (Vec Bit m) (Vec Bit m)
ps >> zero = ps with-carry: replicate b0
_>>_ {suc m} (p ∷ ps) (suc i) = new-result with-carry: new-carry
  where
    qs : WithCarry (Vec Bit m) (Vec Bit m)
    qs = ps >> i
    new-result : Vec Bit (suc m)
    new-result = insert (result qs) (finFromℕ m) b0
    new-carry : Vec Bit (suc m)
    new-carry = insert (carry qs) (finFromℕ m) p

_<<_ : {m : ℕ} → Vec Bit m → Fin m → WithCarry (Vec Bit m) (Vec Bit m)
_<<_ {m} ps i = proj₂ (do-shift ps) where
  do-shift : {n : ℕ} → Vec Bit n → Fin m × WithCarry (Vec Bit n) (Vec Bit n)
  do-shift [] = i , ([] with-carry: [])
  do-shift {suc n} (p ∷ ps) = ret (proj₁ pair) where
    pair : Fin m × WithCarry (Vec Bit n) (Vec Bit n)
    pair = do-shift ps
    qs : WithCarry (Vec Bit n) (Vec Bit n)
    qs = proj₂ pair
    ret : Fin m → Fin m × WithCarry (Vec Bit (suc n)) (Vec Bit (suc n))
    ret zero = zero , (b0 ∷ result qs with-carry: p ∷ carry qs)
    ret (suc j) = raise 1 j , (p ∷ result qs with-carry: b0 ∷ carry qs)

_>>>_ : {m : ℕ} → Vec Bit m → Fin m → WithCarry (Vec Bit m) (Vec Bit m)
ps >>> zero = ps with-carry: replicate b0
_>>>_ {suc m} (p ∷ ps) (suc i) = new-result with-carry: new-carry where
  qs : WithCarry (Vec Bit m) (Vec Bit m)
  qs = ps >> i
  new-result : Vec Bit (suc m)
  new-result = insert (result qs) (finFromℕ m) p
  new-carry : Vec Bit (suc m)
  new-carry = b0 ∷ carry qs

_<<<_ : {m : ℕ} → Vec Bit m → Fin m → WithCarry (Vec Bit m) (Vec Bit m)
ps <<< zero = ps with-carry: replicate b0
_<<<_ {suc m} (p ∷ ps) (suc i) = new-result with-carry: new-carry where
  qs : WithCarry (Vec Bit m) (Vec Bit m)
  qs = ps << i
  new-result : Vec Bit (suc m)
  new-result = p ∷ result qs
  new-carry : Vec Bit (suc m)
  new-carry = insert (result qs) (finFromℕ m) b0

_&_ : {n : ℕ} → Vec Bit n → Vec Bit n → Vec Bit n
[] & [] = []
(p ∷ ps) & (q ∷ qs) = p ∧ q ∷ ps & qs

_~|_ : {n : ℕ} → Vec Bit n → Vec Bit n → Vec Bit n
[] ~| [] = []
(p ∷ ps) ~| (q ∷ qs) = (p ∨ q) ∷ (ps ~| qs)

_^_ : {n : ℕ} → Vec Bit n → Vec Bit n → Vec Bit n
[] ^ [] = []
(p ∷ ps) ^ (q ∷ qs) = (p ⊕ q) ∷ (ps ^ qs)

~ : {n : ℕ} → Vec Bit n → WithCarry (Vec Bit n) (Vec Bit 2)
~ n = inc (!ₙ n)

toℕ : Bit → ℕ
toℕ b0 = 0
toℕ b1 = 1

toFin : {n : ℕ} → Bit → Fin (suc (suc n))
toFin b0 = 0
toFin b1 = 1

toℕₙ : {n : ℕ} → Vec Bit n → ℕ
toℕₙ [] = 0
toℕₙ (p ∷ ps) = ℕ+ (toℕ p) (ℕ* 2 (toℕₙ ps))

tryToFinₙ : {m n : ℕ} → Vec Bit m → Maybe (Fin n)
tryToFinₙ {_} {n} ps = tryℕ n (toℕₙ ps) where
  tryℕ : (k : ℕ) → ℕ → Maybe (Fin k)
  tryℕ zero _ = nothing
  tryℕ (suc _) zero = just zero
  tryℕ (suc m) (suc n) = map suc (tryℕ m n)

ℕ-mod2 : ℕ → Bit
ℕ-mod2 zero = b0
ℕ-mod2 (suc zero) = b1
ℕ-mod2 (suc (suc n)) = ℕ-mod2 n

instance
  Bit-num : Number Bit
  Bit-num .Number.Constraint n = constrain n where
    constrain : ℕ → Set
    constrain zero = ⊤
    constrain (suc zero) = ⊤
    constrain  _ = ⊥
  Bit-num .Number.fromNat n ⦃ p ⦄ = fromNat n p where
    fromNat : (m : ℕ) → (Number.Constraint Bit-num) m → Bit
    fromNat zero _ = b0
    fromNat (suc zero) _ = b1
    fromNat (suc (suc _)) ()

instance
  Bits-num : {m : ℕ} → Number (Vec Bit m)
  Bits-num {m} .Number.Constraint n = ℕ≤ (suc n) (ℕ^ 2 m)
  Bits-num {m} .Number.fromNat n  = fromNat m n where
    fromNat : (m : ℕ) → ℕ → Vec Bit m
    fromNat zero _ = []
    fromNat (suc m) n = ℕ-mod2 n ∷ fromNat m ⌊ n /2⌋

instance
  Bits-neg : {m : ℕ} → Negative (Vec Bit (suc m))
  Bits-neg {m} .Negative.Constraint n = ℕ≤ n (ℕ^ 2 m)
  Bits-neg {m} .Negative.fromNeg n  = number where
    iterateBits : (m : ℕ) → ℕ → Vec Bit m × Bit
    iterateBits zero _ = [] , b0 where
    iterateBits (suc m) n = newVec , newSign where
      subRes : Vec Bit m × Bit
      subRes = iterateBits m ⌊ n /2⌋
      newVec : Vec Bit (suc m)
      newVec = ℕ-mod2 n ∷ proj₁ subRes
      newSign : Bit
      newSign = ℕ-mod2 n ∨ proj₂ subRes
    iteration : Vec Bit (suc m) × Bit
    iteration = iterateBits (suc m) n
    preNumber : Vec Bit (suc m)
    preNumber = proj₁ iteration
    signBit : Bit
    signBit = proj₂ iteration
    number : Vec Bit (suc m)
    number = (head preNumber ∨ signBit) ∷ tail preNumber

_==_ : {n : ℕ} → Vec Bit n → Vec Bit n → Bool
[] == [] = true
p ∷ ps == q ∷ qs = Bool-∧ (toBool (p ↔ q)) (ps == qs)

max_stars_repo_name: brunoczim/Celeste

max_issues_repo_name: brunoczim/Celeste

max_forks_repo_name: brunoczim/Celeste


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Fun.Facts where

open import Cats.Category.Fun.Facts.Iso public using
  ( ≈→≅ ; ≅→≈ )
open import Cats.Category.Fun.Facts.Limit public using
  ( complete )
open import Cats.Category.Fun.Facts.Product public using
  ( hasBinaryProducts ; hasFiniteProducts )
open import Cats.Category.Fun.Facts.Terminal public using
  ( hasTerminal )

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
-- Andreas, 2012-09-15
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.meta:50 #-}
-- {-# OPTIONS -v tc.conv:50 #-}
-- {-# OPTIONS -v tc.polarity:10 #-}
-- {-# OPTIONS -v tc.constr.findInScope:50 #-}
module BrokenInferenceDueToNonvariantPolarity where

import Common.Level

data ⊥ : Set where
record ⊤ : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

False : Nat → Set
False zero    = ⊥
False (suc n) = False n

module Invariant where
  record Bla (n : Nat)(p : False n) : Set where
  -- phantom arguments to Bla get polarity 'Invariant'

module Nonvariant where
  Bla : (n : Nat) → False n → Set
  Bla n p = ⊤
  -- polarity checker infers arguments to be 'Nonvariant'

-- open Invariant  -- succeeds
open Nonvariant -- fails

module Works where

  drop-suc : {n : Nat}{{p : False n}} → Bla (suc n) p → Bla n p
  drop-suc _ = _

  works :  (n : Nat) → {{p : False n}} → Bla n p → ⊥
  works zero {{()}} b
  works (suc n) b = works n (drop-suc {n} b)

module Fails where

  drop-suc : {n : Nat}{{p : False n}} → Bla (suc n) p → Bla n p
  drop-suc _ = _

  bla : (n : Nat) → {p : False n} → Bla n p → ⊥
  bla zero {()} b
  bla (suc n) b = bla n (drop-suc b)
  -- Since Bla is analysed as constant function, the constraint
  -- Bla n p = Bla X Y does not provide unique solutions for X and Y.
  -- And since the positivity checker runs after constraint solving,
  -- Agda does not recognize that bla is Nonvariant in argument p
  -- and that it hence could search for any solution.


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.SumFin where

open import Cubical.Data.SumFin.Base public
open import Cubical.Data.SumFin.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Interacting with the real world ---Compilation, Haskell, and IO
-- :PROPERTIES:
-- :header-args: :tangle "CompilingAgda.agda" :comments org
-- :CUSTOM_ID: agda-interacting-with-the-real-world
-- :END:

-- # C-c C-v C-t tangles the following code into CompilingAgda.agda.
-- # Then we may compile the result using:
-- # (shell-command "NAME=CompilingAgda; time agda --compile $NAME.agda; ./$NAME")
-- #
-- # Btw: (find-file "./MAlonzo/Code/CompilingAgda.hs")

-- #+latex: {\color{white}.} \vspace{-1em}
-- #+begin_quote org
-- /Let's demonstrate how we can reach into Haskell, thereby subverting Agda!/
-- #+end_quote

-- An Agda program module containing a ~main~ function is compiled into a standalone executable
-- with ~agda --compile myfile.agda~. If the module has no main file, use the flag ~--no-main~.
-- If you only want the resulting Haskell, not necessarily an executable program, then use the flag
-- ~--ghc-dont-call-ghc~.

-- The type of ~main~ should be ~Agda.Builtin.IO.IO A~, for some ~A~;
-- this is just a proxy to Haskell's ~IO~.
-- We may ~open import IO.Primitive~ to get /this/ ~IO~, but
-- this one works with costrings, which are a bit awkward.
-- Instead, we use the standard library's wrapper type, also named ~IO~.
-- Then we use ~run~ to move from ~IO~ to ~Primitive.IO~; conversely one uses ~lift~.

-- #+latex: \begin{minipage}[c]{0.55\linewidth}
-- #+latex: \begin{tiny}

open import Data.Nat                 using (ℕ; suc)
open import Data.Nat.Show            using (show)
open import Data.Char                using (Char)
open import Data.List as L           using (map; sum; upTo)
open import Function                 using (_$_; const; _∘_)
open import Data.String as S         using (String; _++_; fromList)
open import Agda.Builtin.Unit        using (⊤)
open import Codata.Musical.Colist    using (take)
open import Codata.Musical.Costring  using (Costring)
open import Data.BoundedVec.Inefficient as B using (toList)
open import Agda.Builtin.Coinduction using (♯_)
open import IO as IO                 using (run ; putStrLn ; IO)
import IO.Primitive as Primitive

-- #+latex: \end{tiny}
-- #+latex: \end{minipage} % no space if you would like to put them side by side
-- #+latex: \begin{minipage}[c]{0.5\linewidth}
-- #+begin_quote org
-- /Agda has *no* primitives for side-effects, instead it allows arbitrary/
-- /Haskell functions to be imported as axioms, whose definitions are only/
-- /used at run-time./
-- #+end_quote
-- #+latex: \end{minipage}

-- Agda lets us use “do”-notation as in Haskell.
-- To do so, methods named ~_>>_~ and ~_>>=_~ need to be in scope ---that is all.
-- The type of ~IO._>>_~ takes two “lazy” IO actions and yield a non-lazy IO action.
-- The one below is a homogeneously typed version.

infixr 1 _>>=_ _>>_

_>>=_ : ∀ {ℓ} {α β : Set ℓ} → IO α → (α → IO β) → IO β
this >>= f = ♯ this IO.>>= λ x → ♯ f x

_>>_ : ∀{ℓ} {α β : Set ℓ} → IO α → IO β → IO β
x >> y = x >>= const y

-- Oddly, Agda's standard library comes with ~readFile~ and
-- ~writeFile~, but the symmetry ends there since it provides ~putStrLn~
-- but not [[https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:getLine][~getLine~]]. Mimicking the ~IO.Primitive~ module, we define /two/
-- versions ourselves as proxies for Haskell's ~getLine~ ---the second one
-- below is bounded by 100 characters, whereas the first is not.

postulate
  getLine∞ : Primitive.IO Costring

{-# FOREIGN GHC
  toColist :: [a] -> MAlonzo.Code.Codata.Musical.Colist.AgdaColist a
  toColist []       = MAlonzo.Code.Codata.Musical.Colist.Nil
  toColist (x : xs) =
    MAlonzo.Code.Codata.Musical.Colist.Cons x (MAlonzo.RTE.Sharp (toColist xs))
#-}

{- Haskell's prelude is implicitly available; this is for demonstration. -}
{-# FOREIGN GHC import Prelude as Haskell #-}
{-# COMPILE GHC getLine∞  = fmap toColist Haskell.getLine #-}

-- (1)
-- getLine : IO Costring
-- getLine = IO.lift getLine∞

getLine : IO String
getLine = IO.lift
  $ getLine∞ Primitive.>>= (Primitive.return ∘ S.fromList ∘ B.toList ∘ take 100)

-- We obtain ~MAlonzo~ strings, then convert those to colists, then
-- eventually lift those to the wrapper ~IO~ type.

-- Let's also give ourselves Haskell's ~read~ method.

postulate readInt  : L.List Char → ℕ
{-# COMPILE GHC readInt = \x -> read x :: Integer  #-}

-- Now we write our ~main~ method.

main : Primitive.IO ⊤
main = run do putStrLn "Hello, world! I'm a compiled Agda program!"

              putStrLn "What is your name?"
              name ← getLine

              putStrLn "Please enter a number."
              num ← getLine
              let tri = show $ sum $ upTo $ suc $ readInt $ S.toList num
              putStrLn $ "The triangle number of " ++ num ++ " is " ++ tri

              putStrLn "Bye, "
              -- IO.putStrLn∞ name  {- If we use approach (1) above. -}
              putStrLn $ "\t" ++ name

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
{- Terms of the language.
   Based on Pfenning and Davies' "Judgmental reconstruction of modal logic."
-}
module Syntax.Terms where

open import Syntax.Types
open import Syntax.Context

mutual
    -- Pure terms of the language, expressed as typing judgements
    infix 10 _⊢_
    data _⊢_ : Context -> Judgement -> Set where
        -- | Simply typed lambda calculus
        -- Variables
        var : ∀{Γ A}            ->                   A ∈ Γ
                                                    -------
                                ->                   Γ ⊢ A

        -- Lambda abstraction
        lam : ∀{Γ A B}          ->             Γ , A now ⊢ B now
                                              -------------------
                                ->               Γ ⊢ A => B now

        -- Application
        _$_ : ∀{Γ A B}          ->         Γ ⊢ A => B now  ->   Γ ⊢ A now
                                          -------------------------------
                                ->                  Γ ⊢ B now

        -- | Basic data types
        -- Unit                                  ---------------
        unit : ∀{Γ}             ->                Γ ⊢ Unit now

        -- Pair of two terms
        [_,,_] : ∀{Γ A B}       ->          Γ ⊢ A now   ->   Γ ⊢ B now
                                        ----------------------------
                                ->                 Γ ⊢ A & B now

        -- First projection
        fst : ∀{Γ A B}          ->                 Γ ⊢ A & B now
                                                  ---------------
                                ->                   Γ ⊢ A now

        -- Second projection
        snd : ∀{Γ A B}          ->                 Γ ⊢ A & B now
                                                  ---------------
                                ->                   Γ ⊢ B now

        -- Left injection
        inl : ∀{Γ A B}          ->                   Γ ⊢ A now
                                                  ---------------
                                ->                 Γ ⊢ A + B now

        -- Right injection
        inr : ∀{Γ A B}          ->                   Γ ⊢ B now
                                                  ---------------
                                ->                 Γ ⊢ A + B now

        -- Case split
        case_inl↦_||inr↦_ : ∀{Γ A B C}
                                ->                 Γ ⊢ A + B now
                                ->    Γ , A now ⊢ C now  ->   Γ , B now ⊢ C now
                                     -------------------------------------------
                                ->                   Γ ⊢ C now

        -- | Modal operators
        -- A stable type can be sampled now
        sample : ∀{A Γ}         ->                 Γ ⊢ A always
                                                  --------------
                                ->                   Γ ⊢ A now

        -- Types in stable contexts are always inhabited
        stable : ∀{Γ A}         ->                 Γ ˢ ⊢ A now
                                                  --------------
                                ->                 Γ ⊢ A always

        -- Signal constructor
        sig : ∀{Γ A}            ->                Γ ⊢ A always
                                               ------------------
                                ->              Γ ⊢ Signal A now

        -- Signal destructor
        letSig_In_ : ∀{Γ A B}   ->   Γ ⊢ Signal A now  ->   Γ , A always ⊢ B now
                                    ----------------------------------------
                                ->                 Γ ⊢ B now

        -- Event constructor
        event : ∀{Γ A}          ->                 Γ ⊨ A now
                                               ------------------
                                ->              Γ ⊢ Event A now

    -- Computational terms of the language
    infix 10 _⊨_
    data _⊨_ : Context -> Judgement -> Set where
        -- Pure term is a computational term
        pure : ∀{A Γ}           ->                   Γ ⊢ A
                                                    -------
                                ->                   Γ ⊨ A

        -- Computational signal destructor
        letSig_InC_ : ∀{Γ A B}  ->   Γ ⊢ Signal A now   ->   Γ , A always ⊨ B now
                                    ----------------------------------------------
                                ->                 Γ ⊨ B now

        -- Event destructor
        letEvt_In_ : ∀{Γ A B}   ->   Γ ⊢ Event A now  ->   Γ ˢ , A now  ⊨ B now
                                    --------------------------------------------
                                ->                 Γ ⊨ B now

        -- Select the event that happens first
        select_↦_||_↦_||both↦_ : ∀{Γ A B C}
            ->   Γ ⊢ Event A now  ->  Γ ˢ , A now , Event B now ⊨ C now   -- A happens first
            ->   Γ ⊢ Event B now  ->  Γ ˢ , Event A now , B now ⊨ C now   -- B happens first
            ->             Γ ˢ , A now , B now ⊨ C now                    -- A and B happen at the same time
                -------------------------------------------------
            ->                  Γ ⊨ C now