text:
module Session where

open import Data.Bool
open import Data.Fin
open import Data.Empty
open import Data.List
open import Data.List.All
open import Data.Maybe
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Unit
open import Function using (_$_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values

data Cont (G : SCtx) (φ : TCtx) : (t : Type) → Set where
  halt : ∀ {t}
    → Inactive G
    → (un-t : Unr t)
    → Cont G φ t

  bind : ∀ {φ₁ φ₂ G₁ G₂ t t₂}
    → (ts : Split φ φ₁ φ₂)
    → (ss : SSplit G G₁ G₂)
    → (e₂ : Expr (t ∷ φ₁) t₂)
    → (ϱ₂ : VEnv G₁ φ₁)
    → (κ₂ : Cont G₂ φ₂ t₂)
    → Cont G φ t

  bind-thunk : ∀ {φ₁ φ₂ G₁ G₂ t₂}
    → (ts : Split φ φ₁ φ₂)
    → (ss : SSplit G G₁ G₂)
    → (e₂ : Expr φ₁ t₂)
    → (ϱ₂ : VEnv G₁ φ₁)
    → (κ₂ : Cont G₂ φ₂ t₂)
    → Cont G φ TUnit

  subsume : ∀ {t t₁}
    → SubT t t₁
    → Cont G φ t₁
    → Cont G φ t

data Command (G : SCtx) : Set where

  Fork : ∀ {φ₁ φ₂ G₁ G₂}
    → (ss : SSplit G G₁ G₂)
    → (κ₁ : Cont G₁ φ₁ TUnit)
    → (κ₂ : Cont G₂ φ₂ TUnit)
    → Command G

  Ready : ∀ {φ t G₁ G₂}
    → (ss : SSplit G G₁ G₂)
    → (v : Val G₁ t)
    → (κ : Cont G₂ φ t)
    → Command G

  Halt : ∀ {t}
    → Inactive G
    → Unr t
    → Val G t
    → Command G
  New : ∀ {φ}
    → (s : SType)
    → (κ : Cont G φ (TPair (TChan (SType.force s)) (TChan (SType.force (dual s)))))
    → Command G
  Close : ∀ {φ G₁ G₂}
    → (ss : SSplit G G₁ G₂)
    → (v : Val G₁ (TChan send!))
    → (κ : Cont G₂ φ TUnit)
    → Command G
  Wait  : ∀ {φ G₁ G₂}
    → (ss : SSplit G G₁ G₂)
    → (v : Val G₁ (TChan send?))
    → (κ : Cont G₂ φ TUnit)
    → Command G
  Send : ∀ {φ G₁ G₂ G₁₁ G₁₂ t s}
    → (ss : SSplit G G₁ G₂)
    → (ss-args : SSplit G₁ G₁₁ G₁₂)
    → (vch : Val G₁₁ (TChan (Typing.send t s)))
    → (v : Val G₁₂ t)
    → (κ : Cont G₂ φ (TChan (SType.force s)))
    → Command G
  Recv : ∀ {φ G₁ G₂ t s}
    → (ss : SSplit G G₁ G₂)
    → (vch : Val G₁ (TChan (Typing.recv t s)))
    → (κ : Cont G₂ φ (TPair (TChan (SType.force s)) t))
    → Command G
  Select : ∀ {φ G₁ G₂ s₁ s₂}
    → (ss : SSplit G G₁ G₂)
    → (lab : Selector)
    → (vch : Val G₁ (TChan (sintern s₁ s₂)))
    → (κ : Cont G₂ φ (TChan (selection lab (SType.force s₁) (SType.force s₂))))
    → Command G
  Branch : ∀ {φ G₁ G₂ s₁ s₂}
    → (ss : SSplit G G₁ G₂)
    → (vch : Val G₁ (TChan (sextern s₁ s₂)))
    → (dcont : (lab : Selector) → Cont G₂ φ (TChan (selection lab (SType.force s₁) (SType.force s₂))))
    → Command G
  NSelect : ∀ {φ G₁ G₂ m alt}
    → (ss : SSplit G G₁ G₂)
    → (lab : Fin m)
    → (vch : Val G₁ (TChan (sintN m alt)))
    → (κ : Cont G₂ φ (TChan (SType.force (alt lab))))
    → Command G
  NBranch : ∀ {φ G₁ G₂ m alt}
    → (ss : SSplit G G₁ G₂)
    → (vch : Val G₁ (TChan (sextN m alt)))
    → (dcont : (lab : Fin m) → Cont G₂ φ (TChan (SType.force (alt lab))))
    → Command G

--

rewrite-helper : ∀ {G G1 G2 G'' φ'} → Inactive G2 → SSplit G G1 G2 → SSplit G G G'' → VEnv G2 φ' → VEnv G'' φ'
rewrite-helper ina-G2 ssp-GG1G2 ssp-GGG'' ϱ with inactive-right-ssplit ssp-GG1G2 ina-G2
... | p with rewrite-ssplit1 (sym p) ssp-GG1G2
... | ssp rewrite ssplit-function2 ssp ssp-GGG'' = ϱ

-- interpret an expression
run : ∀ {φ φ₁ φ₂ t G G₁ G₂}
  → Split φ φ₁ φ₂
  → SSplit G G₁ G₂
  → Expr φ₁ t
  → VEnv G₁ φ₁
  → Cont G₂ φ₂ t
  → Command G

run{G = G}{G₁ = G₁}{G₂ = G₂} tsp ssp (var x) ϱ κ with access ϱ x
... | Gx , Gϱ , ina , ssp12 , v rewrite inactive-right-ssplit ssp12 ina =
  Ready ssp v κ
run tsp ssp (nat unr-φ i) ϱ κ =
  Ready ssp (VInt i (unrestricted-venv unr-φ ϱ)) κ
run tsp ssp (unit unr-φ) ϱ κ =
  Ready ssp (VUnit (unrestricted-venv unr-φ ϱ)) κ
run{φ}{φ₁}{φ₂} tsp ssp (letbind{φ₁₁}{φ₁₂}{t₁}{t₂} sp e₁ e₂) ϱ κ₂ with split-env sp ϱ | split-rotate tsp sp
... | (G₁ , G₂) , ssp-G1G2 , ϱ₁ , ϱ₂ | φ' , tsp-φ' , φ'-tsp with ssplit-compose ssp ssp-G1G2
... | Gi , ssp-3i , ssp-42 =
  run tsp-φ' ssp-3i e₁ ϱ₁
  (bind φ'-tsp ssp-42 e₂ ϱ₂ κ₂)
run tsp ssp (pair sp x₁ x₂) ϱ κ with split-env sp ϱ
... | (G₁' , G₂') , ss-G1G1'G2' , ϱ₁ , ϱ₂ with access ϱ₁ x₁ | access ϱ₂ x₂
... | Gv₁ , Gr₁ , ina-Gr₁ , ss-v1r1 , v₁ | Gv₂ , Gr₂ , ina-Gr₂ , ss-v2r2 , v₂ rewrite inactive-right-ssplit ss-v1r1 ina-Gr₁ | inactive-right-ssplit ss-v2r2 ina-Gr₂ =
  Ready ssp (VPair ss-G1G1'G2' v₁ v₂) κ
run tsp ssp (letpair sp p e) ϱ κ with split-env sp ϱ
... | (G₁' , G₂') , ss-G1G1'G2' , ϱ₁ , ϱ₂ with access ϱ₁ p
run tsp ssp (letpair sp p e) ϱ κ | (G₁' , G₂') , ss-G1G1'G2' , ϱ₁ , ϱ₂ | Gvp , Gr , ina-Gr , ss-vpr , VPair ss-GG₁G₂ v₁ v₂ with split-rotate tsp sp
... | φ' , ts-φφ1φ' , ts-φ'φ3φ4 rewrite inactive-right-ssplit ss-vpr ina-Gr with ssplit-compose ss-G1G1'G2' ss-GG₁G₂
... | Gi , ss-G3G1Gi , ss-G1G2G2' = run (left (left ts-φ'φ3φ4)) ssp e (vcons ss-G3G1Gi v₁ (vcons ss-G1G2G2' v₂ ϱ₂)) κ
run{φ}{φ₁}{G = G}{G₁ = G₁} tsp ssp (fork e) ϱ κ with ssplit-refl-left G₁ | split-refl-left φ₁
... | Gi , ss-g1g1g2 | φ' , unr-φ' , sp-φφφ' with split-env sp-φφφ' ϱ
... | (Gp1 , Gp2) , ss-Gp , ϱ₁ , ϱ₂ with unrestricted-venv unr-φ' ϱ₂
... | ina-Gp2 with inactive-right-ssplit-transform ss-Gp ina-Gp2
... | ss-Gp' rewrite sym (ssplit-function2 ss-g1g1g2 ss-Gp') =
  Fork ssp (bind-thunk sp-φφφ' ss-g1g1g2 e ϱ (halt ina-Gp2 UUnit)) κ
run tsp ssp (new unr-φ s) ϱ κ with unrestricted-venv unr-φ ϱ
... | ina rewrite inactive-left-ssplit ssp ina = New s κ
run tsp ssp (close ch) ϱ κ with access ϱ ch
... | Gch , Gϱ , ina , ssp12 , vch with vch | inactive-right-ssplit ssp12 ina
run tsp ssp (close ch) ϱ κ | Gch , Gϱ , ina , ssp12 , vch | vch' | refl = Close ssp vch' κ
run tsp ssp (wait ch) ϱ κ with access ϱ ch
... | Gch , Gϱ , ina , ssp12 , vch with vch | inactive-right-ssplit ssp12 ina
... | vch' | refl = Wait ssp vch' κ
run tsp ssp (Expr.send sp ch vv) ϱ κ with split-env sp ϱ
... | (G₁ , G₂) , ss-gg , ϱ₁ , ϱ₂ with access ϱ₁ ch
... | G₃ , G₄ , ina-G₄ , ss-g1g3g4 , vch with access ϱ₂ vv
... | G₅ , G₆ , ina-G₆ , ss-g2g5g6 , vvv with ssplit-join ss-gg ss-g1g3g4 ss-g2g5g6
... | G₁' , G₂' , ss-g1'g2' , ss-g3g5 , ss-g4g6 rewrite sym (inactive-right-ssplit ss-g1g3g4 ina-G₄) | sym (inactive-right-ssplit ss-g2g5g6 ina-G₆) = Send ssp ss-gg vch vvv κ
run tsp ssp (Expr.recv ch) ϱ κ with access ϱ ch
... | G₁ , G₂ , ina-G₂ , ss-vi , vch rewrite inactive-right-ssplit ss-vi ina-G₂ = Recv ssp vch κ
run tsp ssp (nselect lab ch) ϱ κ with access ϱ ch
... | G₁ , G₂ , ina-G₂ , ss-vi , vch rewrite inactive-right-ssplit ss-vi ina-G₂ = NSelect ssp lab vch κ
run tsp ssp (nbranch{m}{alt} sp ch ealts) ϱ κ with split-env sp ϱ
... | (G₁' , G₂') , ss-G1G1'G2' , ϱ₁ , ϱ₂ with access ϱ₁ ch
... | G₁ , G₂ , ina-G₂ , ss-vi , vch with ssplit-compose ssp ss-G1G1'G2'
... | Gi , ss-G-G1'Gi , ss-Gi-G2'-G2 with split-rotate tsp sp
... | φ' , sp-φφ1φ' , sp-φ'φ3φ4 with inactive-right-ssplit ss-vi ina-G₂
... | refl = NBranch ss-G-G1'Gi vch dcont
  where
    dcont : (lab : Fin m) → Cont Gi _ (TChan (SType.force (alt lab)))
    dcont lab = bind sp-φ'φ3φ4 ss-Gi-G2'-G2 (ealts lab) ϱ₂ κ
run tsp ssp (select lab ch) ϱ κ with access ϱ ch
... | G₁ , G₂ , ina-G₂ , ss-vi , vch rewrite inactive-right-ssplit ss-vi ina-G₂ = Select ssp lab vch κ
run tsp ssp (branch{s₁}{s₂} sp ch e-left e-rght) ϱ κ with split-env sp ϱ
... | (G₁' , G₂') , ss-G1G1'G2' , ϱ₁ , ϱ₂ with access ϱ₁ ch
... | G₁ , G₂ , ina-G₂ , ss-vi , vch with ssplit-compose ssp ss-G1G1'G2'
... | Gi , ss-G-G1'Gi , ss-Gi-G2'-G2 with split-rotate tsp sp
... | φ' , sp-φφ1φ' , sp-φ'φ3φ4 with inactive-right-ssplit ss-vi ina-G₂
... | refl = Branch ss-G-G1'Gi vch dcont
  where
    dcont : (lab : Selector) → Cont Gi _ (TChan (selection lab (SType.force s₁) (SType.force s₂)))
    dcont Left = bind sp-φ'φ3φ4 ss-Gi-G2'-G2 e-left ϱ₂ κ
    dcont Right = bind sp-φ'φ3φ4 ss-Gi-G2'-G2 e-rght ϱ₂ κ
run tsp ssp (ulambda sp unr-φ unr-φ₃ ebody) ϱ κ with split-env sp ϱ
... | (G₁' , G₂') , ss-g1-g1'-g2' , ϱ₁ , ϱ₂ with unrestricted-venv unr-φ₃ ϱ₂
... | ina-G2' with inactive-right-ssplit ss-g1-g1'-g2' ina-G2'
... | refl = Ready ssp (VFun (inj₂ unr-φ) ϱ₁ ebody) κ
run tsp ssp (llambda sp unr-φ₂ ebody) ϱ κ with split-env sp ϱ
... | (G₁' , G₂') , ss-g1-g1'-g2' , ϱ₁ , ϱ₂ with unrestricted-venv unr-φ₂ ϱ₂
... | ina-G2' with inactive-right-ssplit ss-g1-g1'-g2' ina-G2'
... | refl = Ready ssp (VFun (inj₁ refl) ϱ₁ ebody) κ
run{φ}{φ₁}{φ₂} tsp ssp e@(rec unr-φ ebody) ϱ κ with unrestricted-venv unr-φ ϱ
... | ina-G2' with inactive-right-ssplit (ssplit-sym ssp) ina-G2'
... | refl = Ready ssp (VFun (inj₂ unr-φ) ϱ (unr-subst UFun (rght (split-all-unr unr-φ)) unr-φ e ebody)) κ
run tsp ssp (app sp efun earg) ϱ κ with split-env sp ϱ
... | (G₁ , G₂) , ss-gg , ϱ₁ , ϱ₂ with access ϱ₁ efun
... | G₃ , G₄ , ina-G₄ , ss-g1g3g4 , vfun with access ϱ₂ earg
run{φ}{φ₁}{φ₂} tsp ssp (app sp efun earg) ϱ κ | (G₁ , G₂) , ss-gg , ϱ₁ , ϱ₂ | G₃ , G₄ , ina-G₄ , ss-g1g3g4 , VFun{φ'} x ϱ₃ e | G₅ , G₆ , ina-G₆ , ss-g2g5g6 , varg with ssplit-compose4 ss-gg ss-g2g5g6
... | Gi , ss-g1-g5-gi , ss-gi-g1-g6 with ssplit-compose ssp ss-g1-g5-gi
... | Gi₁ , ss-g-g5-gi1 , ss-gi1-gi-g2 with inactive-right-ssplit ss-g1g3g4 ina-G₄
... | refl with inactive-right-ssplit ss-gi-g1-g6 ina-G₆
... | refl with split-from-disjoint φ' φ₂
... | φ₀ , sp' = Ready ss-g-g5-gi1 varg (bind sp' ss-gi1-gi-g2 e ϱ₃ κ)
run tsp ssp (subsume e t≤t') ϱ κ =
  run tsp ssp e ϱ (subsume t≤t' κ)

-- apply a continuation
apply-cont : ∀ {G G₁ G₂ t φ}
  → (ssp : SSplit G G₁ G₂)
  → (κ : Cont G₂ φ t)
  → Val G₁ t
  → Command G
apply-cont ssp (halt inG un-t) v with unrestricted-val un-t v
... | inG2 with inactive-right-ssplit ssp inG
... | refl = Halt (ssplit-inactive ssp inG2 inG) un-t v
apply-cont ssp (bind ts ss e₂ ϱ₂ κ) v with ssplit-compose3 ssp ss
... | Gi , ss-GGiG4 , ss-GiG1G3 =
  run (left ts) ss-GGiG4 e₂ (vcons ss-GiG1G3 v ϱ₂) κ
apply-cont ssp (bind-thunk ts ss e₂ ϱ₂ κ) v with unrestricted-val UUnit v
... | inG1 with inactive-left-ssplit ssp inG1
... | refl =
  run ts ss e₂ ϱ₂ κ
apply-cont ssp (subsume t≤t' κ) v =
  apply-cont ssp κ (coerce v t≤t')

extract-inactive-from-cont : ∀ {G t φ} → Unr t → Cont G φ t → ∃ λ G' → Inactive G' × SSplit G G' G
extract-inactive-from-cont{G} un-t κ = ssplit-refl-right-inactive G

-- lifting through a trivial extension

lift-val : ∀ {G t} → Val G t → Val (nothing ∷ G) t
lift-venv : ∀ {G φ} → VEnv G φ → VEnv (nothing ∷ G) φ

lift-val (VUnit x) = VUnit (::-inactive x)
lift-val (VInt i x) = VInt i (::-inactive x)
lift-val (VPair x v v₁) = VPair (ss-both x) (lift-val v) (lift-val v₁)
lift-val (VChan b vcr) = VChan b (there vcr)
lift-val (VFun lu ϱ e) = VFun lu (lift-venv ϱ) e

lift-venv (vnil ina) = vnil (::-inactive ina)
lift-venv (vcons ssp v ϱ) = vcons (ss-both ssp) (lift-val v) (lift-venv ϱ)

lift-cont : ∀ {G t φ} → Cont G φ t → Cont (nothing ∷ G) φ t
lift-cont (halt inG un-t) = halt (::-inactive inG) un-t
lift-cont (bind ts ss e₂ ϱ₂ κ) = bind ts (ss-both ss) e₂ (lift-venv ϱ₂) (lift-cont κ)
lift-cont (bind-thunk ts ss e₂ ϱ₂ κ) = bind-thunk ts (ss-both ss) e₂ (lift-venv ϱ₂) (lift-cont κ)
lift-cont (subsume t≤t' κ) = subsume t≤t' (lift-cont κ)

lift-command : ∀ {G} → Command G → Command (nothing ∷ G)
lift-command (Fork ss κ₁ κ₂) = Fork (ss-both ss) (lift-cont κ₁) (lift-cont κ₂)
lift-command (Ready ss v κ) = Ready (ss-both ss) (lift-val v) (lift-cont κ)
lift-command (Halt x unr-t v) = Halt (::-inactive x) unr-t (lift-val v)
lift-command (New s κ) = New s (lift-cont κ)
lift-command (Close ss v κ) = Close (ss-both ss) (lift-val v) (lift-cont κ)
lift-command (Wait ss v κ) = Wait (ss-both ss) (lift-val v) (lift-cont κ)
lift-command (Send ss ss-args vch v κ) = Send (ss-both ss) (ss-both ss-args) (lift-val vch) (lift-val v) (lift-cont κ)
lift-command (Recv ss vch κ) = Recv (ss-both ss) (lift-val vch) (lift-cont κ)
lift-command (Select ss lab vch κ) = Select (ss-both ss) lab (lift-val vch) (lift-cont κ)
lift-command (Branch ss vch dcont) = Branch (ss-both ss) (lift-val vch) λ lab → lift-cont (dcont lab)
lift-command (NSelect ss lab vch κ) = NSelect (ss-both ss) lab (lift-val vch) (lift-cont κ)
lift-command (NBranch ss vch dcont) = NBranch (ss-both ss) (lift-val vch) λ lab → lift-cont (dcont lab)
-- threads
data ThreadPool (G : SCtx) : Set where
  tnil : (ina : Inactive G) → ThreadPool G
  tcons : ∀ {G₁ G₂} → (ss : SSplit G G₁ G₂) → (cmd : Command G₁) → (tp : ThreadPool G₂) → ThreadPool G

-- tack a task to the end of a thread pool to implement round robin scheduling
tsnoc : ∀ {G Gpool Gcmd} → SSplit G Gcmd Gpool → ThreadPool Gpool → Command Gcmd → ThreadPool G
tsnoc ss (tnil ina) cmd = tcons ss cmd (tnil ina)
tsnoc ss (tcons ss₁ cmd₁ tp) cmd with ssplit-compose2 ss ss₁
... | Gi , ss-top , ss-rec = tcons (ssplit-sym ss-top) cmd₁ (tsnoc ss-rec tp cmd)

-- append thread pools
tappend : ∀ {G G1 G2} → SSplit G G1 G2 → ThreadPool G1 → ThreadPool G2 → ThreadPool G
tappend ss-top (tnil ina) tp2 rewrite inactive-left-ssplit ss-top ina = tp2
tappend ss-top (tcons ss cmd tp1) tp2 with ssplit-compose ss-top ss
... | Gi , ss-top' , ss-rec = tcons ss-top' cmd (tappend ss-rec tp1 tp2)

-- apply the inactive extension to a thread pool
lift-threadpool : ∀ {G} → ThreadPool G → ThreadPool (nothing ∷ G)
lift-threadpool (tnil ina) = tnil (::-inactive ina)
lift-threadpool (tcons ss cmd tp) = tcons (ss-both ss) (lift-command cmd) (lift-threadpool tp)

matchWaitAndGo : ∀ {G Gc Gc₁ Gc₂ Gtp Gtpwl Gtpacc φ}
  → SSplit G Gc Gtp
  -- close command
  → SSplit Gc Gc₁ Gc₂ × Val Gc₁ (TChan send!) × Cont Gc₂ φ TUnit
  -- focused thread pool
  → SSplit Gtp Gtpwl Gtpacc → ThreadPool Gtpwl → ThreadPool Gtpacc
  → Maybe (∃ λ G' → ThreadPool G')
matchWaitAndGo ss-top cl-info ss-tp  (tnil ina) tp-acc = nothing
matchWaitAndGo ss-top cl-info ss-tp  (tcons ss (Fork ss₁ κ₁ κ₂) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' (Fork ss₁ κ₁ κ₂) tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss (Ready ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' (Ready ss₁ v κ) tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss cmd@(Halt x _ _) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss (New s κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' (New s κ) tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss cmd@(NSelect ss-args lab vch κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss cmd@(Select ss-args lab vch κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss cmd@(NBranch _ _ _) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss cmd@(Branch _ _ _) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss cmd@(Send _ ss-args vch v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss cmd@(Recv _ vch κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchWaitAndGo ss-top cl-info ss-tp (tcons ss (Close ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo ss-top cl-info ss-tp' tp-wl (tcons ss' (Close ss₁ v κ) tp-acc)
matchWaitAndGo ss-top (ss-cl , VChan cl-b cl-vcr , cl-κ) ss-tp (tcons ss (Wait ss₁ (VChan w-b w-vcr) κ) tp-wl) tp-acc with ssplit-compose6 ss ss₁
... | Gi , ss-g3gi , ss-g4g2 with ssplit-compose6 ss-tp ss-g3gi
... | Gi' , ss-g3gi' , ss-gtpacc with ssplit-join ss-top ss-cl ss-g3gi'
... | Gchannels , Gother , ss-top' , ss-channels , ss-others with vcr-match ss-channels cl-vcr w-vcr
matchWaitAndGo ss-top (ss-cl , VChan cl-b cl-vcr , cl-κ) ss-tp (tcons ss (Wait ss₁ (VChan w-b w-vcr) κ) tp-wl) tp-acc | Gi , ss-g3gi , ss-g4g2 | Gi' , ss-g3gi' , ss-gtpacc | Gchannels , Gother , ss-top' , ss-channels , ss-others | nothing with ssplit-compose5 ss-tp ss
... | _ , ss-tp' , ss' = matchWaitAndGo ss-top (ss-cl , VChan cl-b cl-vcr , cl-κ) ss-tp' tp-wl (tcons ss' (Wait ss₁ (VChan w-b w-vcr) κ) tp-acc)
matchWaitAndGo{Gc₂ = Gc₂} ss-top (ss-cl , VChan cl-b cl-vcr , cl-κ) ss-tp (tcons ss (Wait ss₁ (VChan w-b w-vcr) κ) tp-wl) tp-acc | Gi , ss-g3gi , ss-g4g2 | Gi' , ss-g3gi' , ss-gtpacc | Gchannels , Gother , ss-top' , ss-channels , ss-others | just x with ssplit-refl-right-inactive Gc₂
... | Gunit , ina-Gunit , ss-stopped with extract-inactive-from-cont UUnit κ
... | Gunit' , ina-Gunit' , ss-stopped' with ssplit-compose ss-gtpacc (ssplit-sym ss-g4g2)
... | Gi'' , ss-int , ss-g2gacc with ssplit-compose2 ss-others ss-int
... | Gi''' , ss-other , ss-outer-cons = just (Gother , tappend (ssplit-sym ss-other) tp-wl (tcons ss-outer-cons (Ready ss-stopped (VUnit ina-Gunit) cl-κ) (tcons ss-g2gacc (Ready ss-stopped' (VUnit ina-Gunit') κ) tp-acc)))

matchSendAndGo : ∀ {G Gc Gc₁ Gc₂ Gtp Gtpwl Gtpacc φ t s}
  → SSplit G Gc Gtp
  -- read command
  → SSplit Gc Gc₁ Gc₂ × Val Gc₁ (TChan (Typing.recv t s)) × Cont Gc₂ φ (TPair (TChan (SType.force s)) t)
  -- focused thread pool
  → SSplit Gtp Gtpwl Gtpacc → ThreadPool Gtpwl → ThreadPool Gtpacc
  → Maybe (∃ λ G' → ThreadPool G')
matchSendAndGo ss-top recv-info ss-tp (tnil ina) tp-acc = nothing
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Fork ss₁ κ₁ κ₂) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Ready ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Halt _ _ _) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(New s κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(NSelect ss-arg lab vch κ) tp-wl)  tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Select ss-arg lab vch κ) tp-wl)  tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(NBranch _ _ _) tp-wl)  tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Branch _ _ _) tp-wl)  tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Close ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Wait ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info ss-tp (tcons ss cmd@(Recv ss₁ vch κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchSendAndGo ss-top recv-info@(ss-rv , VChan b₁ vcr₁ , κ-rv) ss-tp (tcons ss cmd@(Send ss₁ ss-args (VChan b vcr) v κ) tp-wl) tp-acc with ssplit-compose6 ss₁ ss-args
... | Gi , ss-g1g11gi , ss-gig12g3 with ssplit-compose6 ss ss-g1g11gi
... | Gi' , ss-gtpwlg11g2 , ss-gi'gig2 with ssplit-compose6 ss-tp ss-gtpwlg11g2
... | Gi'' , ss-gtpg11gi'' , ss-gi''gi'gtpacc with ssplit-join ss-top ss-rv ss-gtpg11gi''
... | G₁' , G₂' , ss-gg1'g2' , ss-g1'gc1g11 , ss-g2'gc2gi'' with vcr-match-2-sr (ssplit2 ss-gg1'g2' ss-g1'gc1g11) vcr₁ vcr
... | just (t≤t1 , ds1≡s , GG , GG1 , GG11 , G12 , ssplit2 ss-out1 ss-out2 , vcr-recv , vcr-send) with ssplit-compose ss-gi''gi'gtpacc ss-gi'gig2
... | GSi , ss-Gi''GiGi1 , ss-Gi1G2Gtpacc with ssplit-join ss-out1 ss-out2 ss-g2'gc2gi''
... | GG1' , GG2' , ss-GG-GG1'-GG2' , ss-GG1'-GG11-Gc2 , ss-GG2'-G12-Gi'' with ssplit-rotate ss-GG2'-G12-Gi'' ss-Gi''GiGi1 ss-gig12g3
... | Gi''+ , Gi+ , ss-GG2-G12-Gi''+ , ss-Gi''+Gi+Gsi , ss-Gi+-G12-G4 with ssplit-join ss-GG-GG1'-GG2' ss-GG1'-GG11-Gc2 ss-GG2-G12-Gi''+
... | GG1'' , GG2'' , ss-GG-GG1''-GG2'' , ss-GG1''-GG11-G12 , ss-GG2''-Gc2-Gi''+ with ssplit-compose3 ss-GG-GG1''-GG2'' ss-GG2''-Gc2-Gi''+
... | _ , ss-GG-Gii-Gi''+ , ss-Gii-GG1''-Gc2 = just (GG ,  (tcons ss-GG-Gii-Gi''+ (Ready ss-Gii-GG1''-Gc2 (VPair ss-GG1''-GG11-G12 (VChan b₁ vcr-recv) (coerce v t≤t1)) κ-rv {-κ-rv-}) (tcons ss-Gi''+Gi+Gsi (Ready ss-Gi+-G12-G4 (VChan b vcr-send) κ) (tappend ss-Gi1G2Gtpacc tp-wl tp-acc))))
matchSendAndGo ss-top recv-info@(ss-rv , VChan b₁ vcr₁ , κ-rv) ss-tp (tcons ss cmd@(Send ss₁ ss-args (VChan b vcr) v κ) tp-wl) tp-acc | Gi , ss-g1g11gi , ss-gig12g3 | Gi' , ss-gtpwlg11g2 , ss-gi'gig2 | Gi'' , ss-gtpg11gi'' , ss-gi''gi'gtpacc | G₁' , G₂' , ss-gg1'g2' , ss-g1'gc1g11 , ss-g2'gc2gi'' | nothing with ssplit-compose5 ss-tp ss
... | Gi0 , ss-tp' , ss' = matchSendAndGo ss-top recv-info ss-tp' tp-wl (tcons ss' cmd tp-acc)

matchBranchAndGo : ∀ {G Gc Gc₁ Gc₂ Gtp Gtpwl Gtpacc φ s₁ s₂}
  → SSplit G Gc Gtp
  -- select command
  → (SSplit Gc Gc₁ Gc₂ × ∃ λ lab → Val Gc₁ (TChan (sintern s₁ s₂)) × Cont Gc₂ φ (TChan (selection lab (SType.force s₁) (SType.force s₂))))
  -- focused thread pool
  → SSplit Gtp Gtpwl Gtpacc → ThreadPool Gtpwl → ThreadPool Gtpacc
  → Maybe (∃ λ G' → ThreadPool G')
matchBranchAndGo ss-top select-info ss-tp (tnil ina) tp-acc = nothing
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Fork ss₁ κ₁ κ₂) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Ready ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Halt _ _ _) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(New s κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Close ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Wait ss₁ v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Send ss₁ ss-args vch v κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Recv ss₁ vch κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(NSelect ss₁ lab vch κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(NBranch _ _ _) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top select-info ss-tp (tcons ss cmd@(Select ss₁ lab vch κ) tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top (ss-vκ , lab , VChan b₁ vcr₁ , κ) ss-tp (tcons ss (Branch ss₁ (VChan b vcr) dcont) tp-wl) tp-acc with ssplit-compose6 ss ss₁
... | Gi , ss-gtpwl-g3-gi , ss-gi-g4-g2 with ssplit-compose6 ss-tp ss-gtpwl-g3-gi
... | Gi1 , ss-gtp-g3-gi1 , ss-gi1-gi-gtpacc with ssplit-join ss-top ss-vκ ss-gtp-g3-gi1
... | Gc' , Gtp' , ss-g-gc'-gtp' , ss-gc'-gc1-g1 , ss-gtp'-gc2-gi1 with vcr-match-2-sb (ssplit2 ss-g-gc'-gtp' ss-gc'-gc1-g1) vcr₁ vcr lab
matchBranchAndGo ss-top select-info@(ss-vκ , lab , VChan b₁ vcr₁ , κ) ss-tp (tcons ss cmd@(Branch ss₁ (VChan b vcr) dcont) tp-wl) tp-acc | Gi , ss-gtpwl-g3-gi , ss-gi-g4-g2 | Gi1 , ss-gtp-g3-gi1 , ss-gi1-gi-gtpacc | Gc' , Gtp' , ss-g-gc'-gtp' , ss-gc'-gc1-g1 , ss-gtp'-gc2-gi1 | nothing with ssplit-compose5 ss-tp ss
... | Gix , ss-tp' , ss' = matchBranchAndGo ss-top select-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchBranchAndGo ss-top (ss-vκ , lab , VChan b₁ vcr₁ , κ) ss-tp (tcons ss (Branch ss₁ (VChan b vcr) dcont) tp-wl) tp-acc | Gi , ss-gtpwl-g3-gi , ss-gi-g4-g2 | Gi1 , ss-gtp-g3-gi1 , ss-gi1-gi-gtpacc | Gc' , Gtp' , ss-g-gc'-gtp' , ss-gc'-gc1-g1 , ss-gtp'-gc2-gi1 | just (ds3=s1 , ds4=s2 , GG , GG1 , GG11 , GG12 , ssplit2 ss1' ss2'  , vcr-sel , vcr-bra) with ssplit-compose ss-gi1-gi-gtpacc ss-gi-g4-g2
... | Gi2 , ss-gi1-g3-gi2 , ss-gi2-g2-gtpacc with ssplit-join ss1' ss2' ss-gtp'-gc2-gi1
... | GGG1 , GGG2 , ss-GG-ggg1-ggg2 , ss-ggg1-gc1-gc2 , ss-ggg2-g1-gi1 with ssplit-compose3 ss-ggg2-g1-gi1 ss-gi1-g3-gi2
... | Gi3 , ss-ggg2-gi3-gi2 , ss-gi3-gg12-g2 = just (GG , tcons ss-GG-ggg1-ggg2 (Ready ss-ggg1-gc1-gc2 (VChan b₁ vcr-sel) κ) (tcons ss-ggg2-gi3-gi2 (Ready ss-gi3-gg12-g2 (VChan b vcr-bra) (dcont lab)) (tappend ss-gi2-g2-gtpacc tp-wl tp-acc)))

matchNBranchAndGo : ∀ {G Gc Gc₁ Gc₂ Gtp Gtpwl Gtpacc φ m alt}
  → SSplit G Gc Gtp
  -- select command
  → (SSplit Gc Gc₁ Gc₂ × Σ (Fin m) λ lab → Val Gc₁ (TChan (sintN m alt)) × Cont Gc₂ φ (TChan (SType.force (alt lab))))
  -- focused thread pool
  → SSplit Gtp Gtpwl Gtpacc → ThreadPool Gtpwl → ThreadPool Gtpacc
  → Maybe (∃ λ G' → ThreadPool G')
matchNBranchAndGo ss-top nselect-info ss-tp (tnil ina) tp-acc = nothing
matchNBranchAndGo ss-top (ss-vκ , lab , VChan b₁ vcr₁ , κ) ss-tp (tcons ss cmd@(NBranch ss₁ (VChan b vcr) dcont) tp-wl) tp-acc with ssplit-compose6 ss ss₁
... | Gi , ss-gtpwl-g3-gi , ss-gi-g4-g2 with ssplit-compose6 ss-tp ss-gtpwl-g3-gi
... | Gi1 , ss-gtp-g3-gi1 , ss-gi1-gi-gtpacc with ssplit-join ss-top ss-vκ ss-gtp-g3-gi1
... | Gc' , Gtp' , ss-g-gc'-gtp' , ss-gc'-gc1-g1 , ss-gtp'-gc2-gi1 with vcr-match-2-nsb (ssplit2 ss-g-gc'-gtp' ss-gc'-gc1-g1) vcr₁ vcr lab
matchNBranchAndGo ss-top nselect-info@(ss-vκ , lab , VChan b₁ vcr₁ , κ) ss-tp (tcons ss cmd@(NBranch ss₁ (VChan b vcr) dcont) tp-wl) tp-acc | Gi , ss-gtpwl-g3-gi , ss-gi-g4-g2 | Gi1 , ss-gtp-g3-gi1 , ss-gi1-gi-gtpacc | Gc' , Gtp' , ss-g-gc'-gtp' , ss-gc'-gc1-g1 , ss-gtp'-gc2-gi1 | nothing with ssplit-compose5 ss-tp ss
... | Gix , ss-tp' , ss' = matchNBranchAndGo ss-top nselect-info ss-tp' tp-wl (tcons ss' cmd tp-acc)
matchNBranchAndGo ss-top (ss-vκ , lab , VChan b₁ vcr₁ , κ) ss-tp (tcons ss (NBranch ss₁ (VChan b vcr) dcont) tp-wl) tp-acc | Gi , ss-gtpwl-g3-gi , ss-gi-g4-g2 | Gi1 , ss-gtp-g3-gi1 , ss-gi1-gi-gtpacc | Gc' , Gtp' , ss-g-gc'-gtp' , ss-gc'-gc1-g1 , ss-gtp'-gc2-gi1 | just (m1≤m , ds3=s1 , GG , GG1 , GG11 , GG12 , ssplit2 ss1' ss2'  , vcr-sel , vcr-bra) with ssplit-compose ss-gi1-gi-gtpacc ss-gi-g4-g2
... | Gi2 , ss-gi1-g3-gi2 , ss-gi2-g2-gtpacc with ssplit-join ss1' ss2' ss-gtp'-gc2-gi1
... | GGG1 , GGG2 , ss-GG-ggg1-ggg2 , ss-ggg1-gc1-gc2 , ss-ggg2-g1-gi1 with ssplit-compose3 ss-ggg2-g1-gi1 ss-gi1-g3-gi2
... | Gi3 , ss-ggg2-gi3-gi2 , ss-gi3-gg12-g2 = just (GG , tcons ss-GG-ggg1-ggg2 (Ready ss-ggg1-gc1-gc2 (VChan b₁ vcr-sel) κ) (tcons ss-ggg2-gi3-gi2 (Ready ss-gi3-gg12-g2 (VChan b vcr-bra) (dcont (inject≤ lab m1≤m))) (tappend ss-gi2-g2-gtpacc tp-wl tp-acc)))
matchNBranchAndGo ss-top nselect-info ss-tp (tcons ss cmd tp-wl) tp-acc with ssplit-compose5 ss-tp ss
... | Gi , ss-tp' , ss' = matchNBranchAndGo ss-top nselect-info ss-tp' tp-wl (tcons ss' cmd tp-acc)

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport

open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

private
  variable
    ℓ ℓA ℓA' ℓ≅A ℓB ℓB' ℓ≅B ℓC ℓ≅C : Level

record UARel (A : Type ℓA) (ℓ≅A : Level) : Type (ℓ-max ℓA (ℓ-suc ℓ≅A)) where
  no-eta-equality
  constructor uarel
  field
    _≅_ : A → A → Type ℓ≅A
    ua : (a a' : A) → (a ≅ a') ≃ (a ≡ a')

  uaIso : (a a' : A) → Iso (a ≅ a') (a ≡ a')
  uaIso a a' = equivToIso (ua a a')

  ≅→≡ : {a a' : A} (p : a ≅ a') → a ≡ a'
  ≅→≡ {a} {a'} = Iso.fun (uaIso a a')
  ≡→≅ : {a a' : A} (p : a ≡ a') → a ≅ a'
  ≡→≅ {a} {a'} = Iso.inv (uaIso a a')

  ρ : (a : A) → a ≅ a
  ρ a = ≡→≅ refl

open BinaryRelation

-- another constructor for UARel using contractibility of relational singletons
make-𝒮 : {A : Type ℓA} {ℓ≅A : Level} {_≅_ : A → A → Type ℓ≅A}
          (ρ : isRefl _≅_) (contrTotal : contrRelSingl _≅_) → UARel A ℓ≅A
UARel._≅_ (make-𝒮 {_≅_ = _≅_} _ _) = _≅_
UARel.ua (make-𝒮 {_≅_ = _≅_} ρ c) = contrRelSingl→isUnivalent _≅_ ρ c

record DUARel {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : UARel A ℓ≅A)
              (B : A → Type ℓB) (ℓ≅B : Level) : Type (ℓ-max (ℓ-max ℓA ℓB) (ℓ-max ℓ≅A (ℓ-suc ℓ≅B))) where
  no-eta-equality
  constructor duarel
  open UARel 𝒮-A

  field
    _≅ᴰ⟨_⟩_ : {a a' : A} → B a → a ≅ a' → B a' → Type ℓ≅B
    uaᴰ : {a a' : A} (b : B a) (p : a ≅ a') (b' : B a') → (b ≅ᴰ⟨ p ⟩ b') ≃ PathP (λ i → B (≅→≡ p i)) b b'

  fiberRel : (a : A) → Rel (B a) (B a) ℓ≅B
  fiberRel a = _≅ᴰ⟨ ρ a ⟩_

  uaᴰρ : {a : A} (b b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ (b ≡ b')
  uaᴰρ {a} b b' =
    compEquiv
      (uaᴰ b (ρ _) b')
      (substEquiv (λ q → PathP (λ i → B (q i)) b b') (retEq (ua a a) refl))

  ρᴰ : {a : A} → (b : B a) → b ≅ᴰ⟨ ρ a ⟩ b
  ρᴰ {a} b = invEq (uaᴰρ b b) refl

ext: agda

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:
module Numeric.Nat.Prime.FundamentalTheorem where

open import Prelude
open import Control.WellFounded
open import Container.List
open import Container.List.Permutation
open import Container.List.Properties
open import Numeric.Nat
open import Tactic.Nat

--- Some lemmas ----------

private
  primeProd=1-is-empty : ∀ ps → All Prime ps → productR ps ≡ 1 → ps ≡ []
  primeProd=1-is-empty [] _ _ = refl
  primeProd=1-is-empty (p ∷ ps) (prime p>1 _ ∷ _) pps=1 =
    let p=1 : p ≡ 1
        p=1 = mul=1-l p (productR ps) pps=1
    in case p=1 of λ where refl → refute p>1

  0<1<2 : ∀ {n} ⦃ _ : NonZero n ⦄ → n < 2 → n ≡ 1
  0<1<2 {0} ⦃ () ⦄ n<2
  0<1<2 {1} n<2 = refl
  0<1<2 {suc (suc _)} n<2 = refute n<2

  1>0 : ∀ {n} → n > 1 → NonZero n
  1>0 {0} n>1 = refute n>1
  1>0 {suc _} _ = _

  product-deleteIx : ∀ {a} ⦃ _ : NonZero a ⦄ (as : List Nat) (i : a ∈ as) →
                       productR as ≡ a * productR (deleteIx as i)
  product-deleteIx (a ∷ as) zero!   = refl
  product-deleteIx {a} (b ∷ as) (suc i) =
    b * productR as                  ≡⟨ b *_ $≡ product-deleteIx as i  ⟩
    b * productR (a ∷ deleteIx as i) ≡⟨ auto ⟩
    a * productR (b ∷ deleteIx as i) ∎

--- Factorisation ---------

record Factorisation (n : Nat) : Set where
  no-eta-equality
  constructor mkFactors
  field
    factors       : List Nat
    factors-prime : All Prime factors
    factors-sound : productR factors ≡ n

open Factorisation

mul-factors : ∀ {a b} → Factorisation a → Factorisation b → Factorisation (a * b)
mul-factors {a} {b} (mkFactors ps psP ps=a) (mkFactors qs qsP qs=b) =
  mkFactors (ps ++ qs) (psP ++All qsP) $
    productR (ps ++ qs)       ≡⟨ product-++ ps _ ⟩
    productR ps * productR qs ≡⟨ _*_ $≡ ps=a *≡ qs=b ⟩
    a * b ∎

private
  factorise′ : ∀ n ⦃ _ : NonZero n ⦄ → Acc _<_ n → Factorisation n
  factorise′ n (acc wf) =
    case isPrime n of λ where
      (yes p) → mkFactors (n ∷ []) (p ∷ []) auto
      (no (composite a b a>1 b>1 refl)) →
        let instance _ = 1>0 a>1; _ = 1>0 b>1 in
        mul-factors (factorise′ a (wf a (less-mul-l a>1 b>1)))
                    (factorise′ b (wf b (less-mul-r a>1 b>1)))
      (tiny n<2) → mkFactors [] [] (sym (0<1<2 n<2))

  find-prime : ∀ p ps → Prime p → All Prime ps → p Divides productR ps → p ∈ ps
  find-prime p [] isP isPs p|1 = ⊥-elim (prime-divide-coprime p 1 1 isP refl p|1 p|1)
  find-prime p (q ∷ qs) isP (qP ∷ isPs) p|qqs =
    case prime-split q (productR qs) isP p|qqs of λ where
      (left  p|q)  → zero (prime-divide-prime isP qP p|q)
      (right p|qs) → suc  (find-prime p qs isP isPs p|qs)

  unique : (ps qs : List Nat) → All Prime ps → All Prime qs → productR ps ≡ productR qs → Permutation ps qs
  unique [] qs ips iqs ps=qs = case primeProd=1-is-empty qs iqs (sym ps=qs) of λ where refl → []
  unique (p ∷ ps) qs (pP ∷ psP) qsP pps=qs =
    let instance _ = prime-nonzero pP
        p|qs : p Divides productR qs
        p|qs = factor (productR ps) (by pps=qs)
        i : p ∈ qs
        i = find-prime p qs pP qsP p|qs
        ps=qs/p : productR ps ≡ productR (deleteIx qs i)
        ps=qs/p = mul-inj₂ p _ _ (pps=qs ⟨≡⟩ product-deleteIx qs i )
    in i ∷ unique ps (deleteIx qs i) psP (deleteAllIx qsP i) ps=qs/p

--- The Fundamental Theorem of arithmetic:
--    any nonzero natural number can be factored into a product of primes,
--    and the factorisation is unique up to permutation.

factorise : (n : Nat) ⦃ _ : NonZero n ⦄ → Factorisation n
factorise n = factorise′ n (wfNat n)

factors-unique : ∀ {n} (f₁ f₂ : Factorisation n) → Permutation (factors f₁) (factors f₂)
factors-unique (mkFactors ps psP ps=n) (mkFactors qs qsP qs=n) =
  unique ps qs psP qsP (ps=n ⟨≡⟩ʳ qs=n)

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
open import Agda.Primitive using (_⊔_)

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian
import MultiSorted.Interpretation as Interpretation

open import MultiSorted.AlgebraicTheory
open import MultiSorted.Substitution
import MultiSorted.Product as Product

module MultiSorted.Model {o ℓ e ℓt}
          {𝓈 ℴ}
          {Σ : Signature {𝓈} {ℴ}}
          (T : Theory ℓt Σ)
          {𝒞 : Category.Category o ℓ e}
          {cartesian-𝒞 : Cartesian.Cartesian 𝒞} where

  -- Model of a theory

  record Is-Model (I : Interpretation.Interpretation Σ cartesian-𝒞) : Set (ℓt ⊔ o ⊔ ℓ ⊔ e) where

    open Theory T
    open Category.Category 𝒞
    open Interpretation.Interpretation I
    open HomReasoning

    field
      model-eq : ∀ (ε : ax) → ⊨ ax-eq (ε)

    -- Soundness of semantics
    module _ where
      open Product.Producted interp-ctx

      -- first we show that substitution preserves validity
      model-resp-[]s : ∀ {Γ Δ} {A} {u v : Term Γ A} {σ : Δ ⇒s Γ} →
                       interp-term u ≈ interp-term v → interp-term (u [ σ ]s) ≈ interp-term (v [ σ ]s)
      model-resp-[]s {u = u} {v = v} {σ = σ} ξ =
        begin
          interp-term (u [ σ ]s) ≈⟨  interp-[]s {t = u} ⟩
          (interp-term u ∘ interp-subst σ)  ≈⟨ ξ ⟩∘⟨refl ⟩
          (interp-term v ∘ interp-subst σ) ≈˘⟨ interp-[]s {t = v} ⟩
          interp-term (v [ σ ]s) ∎

      -- the soundness statement
      ⊢-⊨ : ∀ {ε : Equation Σ} → ⊢ ε → ⊨ ε
      ⊢-⊨ eq-refl =  Equiv.refl
      ⊢-⊨ (eq-symm ξ) = ⟺ (⊢-⊨ ξ)
      ⊢-⊨ (eq-tran ξ θ) = ⊢-⊨ ξ ○ ⊢-⊨ θ
      ⊢-⊨ (eq-congr ξ) = ∘-resp-≈ʳ (unique λ i → project ○ ⟺ (⊢-⊨ (ξ i)))
      ⊢-⊨ (eq-axiom ε σ) = model-resp-[]s {u = ax-lhs ε} {v = ax-rhs ε} (model-eq ε)

  -- Every theory has the trivial model, whose carrier is the terminal object
  Trivial : Is-Model (Interpretation.Trivial Σ cartesian-𝒞)
  Trivial =
    let open Cartesian.Cartesian cartesian-𝒞 in
    record { model-eq = λ ε → !-unique₂ }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- There are no level literals in the concrete syntax. This file tests
-- if type errors use level literals.

module LevelLiterals where

open import Common.Level

data ⊥ : Set₁ where

DoubleNegated : ∀ {ℓ} → Set ℓ → Set
DoubleNegated A = (A → ⊥) → ⊥

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{- Agda can check termination of Stream transducer operations.
   (Created: Andreas Abel, 2008-12-01
    at Agda Intensive Meeting 9 in Sendai, Japan.
    I acknowledge the support by AIST and JST.)

Stream transducers have been described in:

  N. Ghani, P. Hancock, and D. Pattinson,
  Continuous functions on final coalgebras.
  In Proc. CMCS 2006, Electr. Notes in Theoret. Comp. Sci., 2006.

They have been modelled by mixed equi-(co)inductive sized types in

  A. Abel,
  Mixed Inductive/Coinductive Types and Strong Normalization.
  In APLAS 2007, LNCS 4807.

Here we model them by mutual data/codata and mutual recursion/corecursion.
 -}

module StreamProcEat where

open import Common.Coinduction

data Stream (A : Set) : Set where
  cons : A -> ∞ (Stream A) -> Stream A

-- Stream Transducer: Trans A B
-- intended semantics: Stream A -> Stream B

mutual

  data Trans (A B : Set) : Set where
    〈_〉 : ∞ (Trans' A B) -> Trans A B

  data Trans' (A B : Set) : Set where
    get : (A -> Trans' A B) -> Trans' A B
    put : B -> Trans A B -> Trans' A B

out : forall {A B} -> Trans A B -> Trans' A B
out 〈 p 〉 = ♭ p

-- evaluating a stream transducer ("stream eating")

mutual

  -- eat is defined by corecursion into Stream B
  eat  : forall {A B} -> Trans A B -> Stream A -> Stream B
  eat 〈 sp 〉 as = eat' (♭ sp) as

  -- eat' is defined by a local recursion on Trans' A B
  eat' : forall {A B} -> Trans' A B -> Stream A -> Stream B
  eat' (get f) (cons a as) = eat' (f a) (♭ as)
  eat' (put b sp) as = cons b (♯ eat sp as)

-- composing two stream transducers

mutual

  -- comb is defined by corecursion into Trans A B
  comb : forall {A B C} -> Trans A B -> Trans B C -> Trans A C
  comb 〈 p1 〉 〈 p2 〉 = 〈 ♯ comb' (♭ p1) (♭ p2) 〉

  -- comb' preforms a local lexicographic recursion on (Trans' B C, Trans' A B)
  comb' : forall {A B C} -> Trans' A B -> Trans' B C -> Trans' A C
  comb' (put b p1) (get f)    = comb' (out p1) (f b)
  comb' (put b p1) (put c p2) = put c (comb p1 p2)
  comb' (get f)    p2         = get (\ a -> comb' (f a) p2)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module HLevels where

open import Path
open import Cubical.Foundations.Everything
  using (isProp
        ;isSet
        ;isContr
        ;isPropIsContr
        ;isProp→isSet
        ;isOfHLevel→isOfHLevelDep
        ;hProp
        ;isSetHProp
        ;isPropIsProp
        )
  public

open import Level
open import Data.Sigma

hSet : ∀ ℓ → Type (ℓsuc ℓ)
hSet ℓ = Σ (Type ℓ) isSet

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Agda.Builtin.Size

data D : Size → Set where

postulate
  f : (i : Size) → D i

data P : (i : Size) → D i → Set where
  c : (i j : Size) → P (i ⊔ˢ j) (f _)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Functional using (id)
import      Structure.Logic.Classical.NaturalDeduction

module Structure.Logic.Classical.SetTheory {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)

import      Lvl
open import Data.Tuple using () renaming (_⨯_ to _⨯ₘ_ ; _,_ to _,ₘ_)
open import Functional using (_∘_)
open import Syntax.Function
open import Structure.Logic.Classical.SetTheory.SetBoundedQuantification ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Classical.SetTheory.Relation                 ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Constructive.Syntax.Algebra                  ⦃ classicLogic ⦄
open import Syntax.Transitivity
open import Type

[⊆]-reflexivity : Proof(∀ₗ(s ↦ s ⊆ s))
[⊆]-reflexivity = [∀].intro(\{_} → [∀].intro(\{_} → [→].reflexivity))

[⊆]-transitivity : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(c ↦ (a ⊆ b)∧(b ⊆ c) ⟶ (a ⊆ c)))))
[⊆]-transitivity =
  ([∀].intro(\{a} →
    ([∀].intro(\{b} →
      ([∀].intro(\{c} →
        ([→].intro(abbc ↦
          ([∀].intro(\{x} →
            ([→].transitivity
              ([∀].elim([∧].elimₗ abbc){x})
              ([∀].elim([∧].elimᵣ abbc){x})
            )
          ))
        ))
      ))
    ))
  ))

[⊆]-transitivable : Transitivable(_⊆_)
[⊆]-transitivable = Transitivity-to-Transitivable [⊆]-transitivity

[⊆][≡ₛ]-antisymmetry : Proof(∀ₗ(x ↦ ∀ₗ(y ↦ ((x ⊇ y) ∧ (x ⊆ y)) ⟶ (x ≡ₛ y))))
[⊆][≡ₛ]-antisymmetry =
  ([∀].intro(\{a} →
    ([∀].intro(\{b} →
      ([→].intro(abba ↦
        ([∀].intro(\{x} →
          ([↔].intro
            ([→].elim([∀].elim([∧].elimₗ abba){x}))
            ([→].elim([∀].elim([∧].elimᵣ abba){x}))
          )
        ))
      ))
    ))
  ))

[≡ₛ]-to-[⊆] : Proof(∀ₗ(x ↦ ∀ₗ(y ↦ (x ≡ₛ y) ⟶ (x ⊆ y))))
[≡ₛ]-to-[⊆] =
  ([∀].intro(\{x} →
    ([∀].intro(\{y} →
      ([→].intro(x≡y ↦
        ([∀].intro(\{a} →
          [→].intro([↔].elimᵣ([∀].elim x≡y {a}))
        ))
      ))
    ))
  ))

[≡ₛ]-to-[⊇] : Proof(∀ₗ(x ↦ ∀ₗ(y ↦ (x ≡ₛ y) ⟶ (x ⊇ y))))
[≡ₛ]-to-[⊇] =
  ([∀].intro(\{x} →
    ([∀].intro(\{y} →
      ([→].intro(x≡y ↦
        ([∀].intro(\{a} →
          [→].intro([↔].elimₗ([∀].elim x≡y {a}))
        ))
      ))
    ))
  ))

[⊆][≡ₛ]-equivalence : Proof(∀ₗ(x ↦ ∀ₗ(y ↦ ((x ⊇ y) ∧ (x ⊆ y)) ⟷ (x ≡ₛ y))))
[⊆][≡ₛ]-equivalence =
  ([∀].intro(\{x} →
    ([∀].intro(\{y} →
      ([↔].intro
        (x≡y ↦
          ([∧].intro
            ([→].elim([∀].elim([∀].elim [≡ₛ]-to-[⊇] {x}){y}) (x≡y))
            ([→].elim([∀].elim([∀].elim [≡ₛ]-to-[⊆] {x}){y}) (x≡y))
          )
        )

        ([→].elim([∀].elim([∀].elim [⊆][≡ₛ]-antisymmetry{x}){y}))
      )
    ))
  ))

[≡ₛ]-reflexivity : Proof(∀ₗ(s ↦ s ≡ₛ s))
[≡ₛ]-reflexivity = [∀].intro(\{_} → [∀].intro(\{_} → [↔].reflexivity))

[≡ₛ]-transitivity : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(c ↦ (a ≡ₛ b)∧(b ≡ₛ c) ⟶ (a ≡ₛ c)))))
[≡ₛ]-transitivity =
  ([∀].intro(\{a} →
    ([∀].intro(\{b} →
      ([∀].intro(\{c} →
        ([→].intro(abbc ↦
          ([∀].intro(\{x} →
            (
              ([∀].elim([∧].elimₗ abbc){x})
              🝖 ([∀].elim([∧].elimᵣ abbc){x})
            )
          ))
        ))
      ))
    ))
  ))

[≡ₛ]-transitivable : Transitivable(_≡ₛ_)
[≡ₛ]-transitivable = Transitivity-to-Transitivable [≡ₛ]-transitivity

[≡ₛ]-symmetry : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (a ≡ₛ b) ⟶ (b ≡ₛ a))))
[≡ₛ]-symmetry =
  ([∀].intro(\{a} →
    ([∀].intro(\{b} →
      ([→].intro(ab ↦
        ([∀].intro(\{x} →
          ([↔].commutativity
            ([∀].elim ab{x})
          )
        ))
      ))
    ))
  ))

[≡ₛ]-from-equiv : ∀{A B : Domain}{Af Bf : Domain → Formula} → Proof(∀ₗ(x ↦ (x ∈ A) ⟷ Af(x))) → Proof(∀ₗ(x ↦ (x ∈ B) ⟷ Bf(x))) → Proof(∀ₗ(x ↦ Af(x) ⟷ Bf(x))) → Proof(A ≡ₛ B)
[≡ₛ]-from-equiv aeq beq afbf =
  ([∀].intro(\{x} →
    ([↔].transitivity
      ([↔].transitivity
        ([∀].elim aeq)
        ([∀].elim afbf)
      )
      ([↔].commutativity ([∀].elim beq))
    )
  ))

record SetEquality : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    extensional : Proof(∀ₗ(s₁ ↦ ∀ₗ(s₂ ↦ (s₁ ≡ₛ s₂) ⟷ (s₁ ≡ s₂))))

  extensionalᵣ : ∀{s₁ s₂} → Proof(s₁ ≡ₛ s₂) → Proof(s₁ ≡ s₂)
  extensionalᵣ{s₁}{s₂} (proof) = [↔].elimᵣ ([∀].elim([∀].elim extensional{s₁}){s₂}) (proof)

  -- TODO: Use [⊆][≡ₛ]-equivalence
  [≡]-from-subset : Proof(∀ₗ(x ↦ ∀ₗ(y ↦ ((x ⊇ y) ∧ (x ⊆ y)) ⟷ (x ≡ y))))
  [≡]-from-subset =
    ([∀].intro(\{x} →
      ([∀].intro(\{y} →
        ([↔].intro
          (x≡y ↦ [∧].intro
            ([→].elim ([∀].elim ([∀].elim ([≡]-implies-when-reflexive [⊆]-reflexivity) {x}) {y}) (x≡y))
            ([→].elim ([∀].elim ([∀].elim ([≡]-implies-when-reflexive [⊆]-reflexivity) {x}) {y}) (x≡y))
          )

          (lr ↦
            ([↔].elimᵣ
              ([∀].elim([∀].elim extensional{x}){y})
              ([∀].intro(\{a} →
                ([↔].intro
                  ([→].elim([∀].elim([∧].elimₗ(lr)){a}))
                  ([→].elim([∀].elim([∧].elimᵣ(lr)){a}))
                )
              ))
            )
          )
        )
      ))
    )) where
      [≡]-implies-when-reflexive : ∀{_▫_ : Domain → Domain → Formula} → Proof(∀ₗ(x ↦ x ▫ x)) → Proof(∀ₗ(x ↦ ∀ₗ(y ↦ (x ≡ y) ⟶ (x ▫ y))))
      [≡]-implies-when-reflexive {_▫_} ([▫]-reflexivity) =
        ([∀].intro(\{x} →
          ([∀].intro(\{y} →
            ([→].intro(x≡y ↦
              [≡].elimᵣ{x ▫_} (x≡y) ([∀].elim [▫]-reflexivity{x})
            ))
          ))
        ))

  -- All sets that are defined using an equivalence of contained elements are unique
  unique-definition : ∀{φ : Domain → Formula} → Proof(Unique(S ↦ ∀ₗ(x ↦ (x ∈ S) ⟷ φ(x))))
  unique-definition{_} =
    ([∀].intro(\{S₁} →
      ([∀].intro(\{S₂} →
        ([→].intro(proof ↦
          ([↔].elimᵣ
            ([∀].elim([∀].elim extensional{S₁}){S₂})
            ([∀].intro(\{x} →
              ([↔].transitivity
                ([∀].elim([∧].elimₗ(proof)){x})
                ([↔].commutativity([∀].elim([∧].elimᵣ(proof)){x}))
              )
            ))
          )
        ))
      ))
    ))

  -- TODO: Use [⊆][≡ₛ]-antisymmetry
  [⊆]-antisymmetry : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (b ⊆ a)∧(a ⊆ b) ⟶ (a ≡ b))))
  [⊆]-antisymmetry =
    ([∀].intro(\{a} →
      ([∀].intro(\{b} →
        ([→].intro(abba ↦
          ([↔].elimᵣ([∀].elim([∀].elim extensional{a}){b}))
          ([∀].intro(\{x} →
            ([↔].intro
              ([→].elim([∀].elim([∧].elimₗ abba){x}))
              ([→].elim([∀].elim([∧].elimᵣ abba){x}))
            )
          ))
        ))
      ))
    ))

-- Empty set
-- The set consisting of no elements.
record EmptySet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    ∅ : Domain

  field
    [∅]-membership : Proof(∀ₗ(x ↦ x ∉ ∅))

  [∅]-membership-equiv : Proof(∀ₗ(x ↦ (x ∈ ∅) ⟷ ⊥))
  [∅]-membership-equiv =
    ([∀].intro (\{x} →
      ([↔].intro
        ([⊥].elim)
        ([¬].elim
          ([∀].elim [∅]-membership{x})
        )
      )
    ))

  [∅]-subset : Proof(∀ₗ(s ↦ ∅ ⊆ s))
  [∅]-subset =
    ([∀].intro(\{s} →
      ([∀].intro(\{x} →
        ([→].intro(xin∅ ↦
          [⊥].elim ([↔].elimᵣ([∀].elim [∅]-membership-equiv {x}) (xin∅))
        ))
      ))
    ))

  [∅]-subset-is-equal : Proof(∀ₗ(s ↦ (s ⊆ ∅) ⟶ (s ≡ₛ ∅)))
  [∅]-subset-is-equal =
    ([∀].intro(\{s} →
      ([→].intro(s⊆∅ ↦
        ([→].elim
          ([∀].elim([∀].elim [⊆][≡ₛ]-antisymmetry{s}){∅})
          ([∧].intro
            ([∀].elim [∅]-subset{s})
            (s⊆∅)
          )
        )
      ))
    ))

  [⊆]-minimum : Proof(∀ₗ(min ↦ ∀ₗ(s ↦ min ⊆ s) ⟷ (min ≡ₛ ∅)))
  [⊆]-minimum =
    ([∀].intro(\{min} →
      ([↔].intro
        (min≡∅ ↦
          ([∀].intro(\{s} →
            ([→].elim
              ([∀].elim([∀].elim([∀].elim [⊆]-transitivity {min}){∅}){s})
              ([∧].intro
                ([→].elim ([∀].elim([∀].elim [≡ₛ]-to-[⊆] {min}){∅}) (min≡∅))
                ([∀].elim [∅]-subset {s})
              )
            )
          ))
        )

        (asmin⊆s ↦
          ([→].elim
            ([∀].elim [∅]-subset-is-equal{min})
            ([∀].elim asmin⊆s{∅})
          )
        )
      )
    ))

  [⊆]-minima : Proof(∀ₗ(s ↦ ∅ ⊆ s))
  [⊆]-minima = [∅]-subset

  [∃ₛ]-of-[∅] : ∀{P : Domain → Formula} → Proof(¬(∃ₛ ∅ P))
  [∃ₛ]-of-[∅] =
    ([¬].intro(ep ↦
      [∃ₛ]-elim(\{x} → x∈∅ ↦ _ ↦ [⊥].elim([¬].elim ([∀].elim [∅]-membership) x∈∅)) ep
    ))

-- Singleton set.
-- A set consisting of only a single element.
record SingletonSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    singleton : Domain → Domain

  field
    singleton-membership : Proof(∀ₗ(a ↦ ∀ₗ(x ↦ (x ∈ singleton(a)) ⟷ (x ≡ₛ a))))

  singleton-contains-self : Proof(∀ₗ(s ↦ s ∈ singleton(s)))
  singleton-contains-self =
    ([∀].intro(\{s} →
      ([↔].elimₗ
        ([∀].elim([∀].elim singleton-membership{s}){s})
        ([∀].elim [≡ₛ]-reflexivity{s})
      )
    ))

-- Subset filtering.
-- The subset of the specified set where all elements satisfy the specified formula.
record FilterSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    filter : Domain → (Domain → Formula) → Domain

  field
    filter-membership : ∀{φ : Domain → Formula} → Proof(∀ₗ(s ↦ ∀ₗ(x ↦ ((x ∈ filter(s)(φ)) ⟷ ((x ∈ s) ∧ φ(x))))))

  filter-subset : ∀{φ} → Proof(∀ₗ(s ↦ filter(s)(φ) ⊆ s))
  filter-subset =
    ([∀].intro(\{s} →
      ([∀].intro(\{x} →
        ([→].intro(xinfilter ↦
          [∧].elimₗ([↔].elimᵣ([∀].elim([∀].elim filter-membership{s}){x}) (xinfilter))
        ))
      ))
    ))

  module _ ⦃ _ : EmptySet ⦄ where
    open EmptySet ⦃ ... ⦄

    filter-of-[∅] : ∀{φ} → Proof(filter(∅)(φ) ≡ₛ ∅)
    filter-of-[∅] =
      ([→].elim
        ([∀].elim([∀].elim [⊆][≡ₛ]-antisymmetry))
        ([∧].intro
          ([∀].elim [∅]-subset)
          ([∀].elim filter-subset)
        )
      )

  filter-property : ∀{φ : Domain → Formula} → Proof(∀ₗ(s ↦ ∀ₛ(filter(s)(φ)) φ))
  filter-property =
    ([∀].intro(\{s} →
      ([∀].intro(\{x} →
        ([→].intro(xinfilter ↦
          [∧].elimᵣ([↔].elimᵣ([∀].elim([∀].elim filter-membership{s}){x}) (xinfilter))
        ))
      ))
    ))

-- Power set.
-- The set of all subsets of the specified set.
record PowerSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    ℘ : Domain → Domain

  field
    [℘]-membership : Proof(∀ₗ(s ↦ ∀ₗ(x ↦ (x ∈ ℘(s)) ⟷ (x ⊆ s))))

  module _ ⦃ _ : EmptySet ⦄ where
    open EmptySet ⦃ ... ⦄

    [℘]-contains-empty : Proof(∀ₗ(s ↦ ∅ ∈ ℘(s)))
    [℘]-contains-empty =
      ([∀].intro(\{s} →
        ([↔].elimₗ
          ([∀].elim([∀].elim [℘]-membership{s}){∅})
          ([∀].elim [∅]-subset{s})
        )
      ))

    module _ ⦃ _ : SingletonSet ⦄ where
      open SingletonSet ⦃ ... ⦄

      postulate [℘]-of-[∅] : Proof(℘(∅) ≡ₛ singleton(∅))

  [℘]-contains-self : Proof(∀ₗ(s ↦ s ∈ ℘(s)))
  [℘]-contains-self =
    ([∀].intro(\{s} →
      ([↔].elimₗ
        ([∀].elim([∀].elim [℘]-membership{s}){s})
        ([∀].elim [⊆]-reflexivity{s})
      )
    ))

-- Union over arbitrary sets.
-- Constructs a set which consists of elements which are in any of the specified sets.
record SetUnionSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    ⋃ : Domain → Domain

  field
    [⋃]-membership : Proof(∀ₗ(ss ↦ ∀ₗ(x ↦ (x ∈ ⋃(ss)) ⟷ ∃ₛ(ss)(s ↦ x ∈ s))))

  postulate [⋃]-containing-max : Proof(∀ₗ(s ↦ ∀ₛ(s)(max ↦ ∀ₛ(s)(x ↦ x ⊆ max) ⟶ (⋃(s) ≡ₛ max))))

  module _ ⦃ _ : EmptySet ⦄ where
    open EmptySet ⦃ ... ⦄

    postulate [⋃]-of-[∅] : Proof(⋃(∅) ≡ₛ ∅)
    -- [⋃]-of-[∅] =
    --   ([⋃]-membership
    --   )
    --   [∃ₛ]-of-[∅]

  postulate [⋃]-subset : Proof(∀ₗ(s ↦ ∀ₛ(s)(x ↦ x ⊆ ⋃(s))))

-- Union operator.
-- Constructs a set which consists of both elements from LHS and RHS.
record UnionSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  infixl 3000 _∪_
  field
    _∪_ : Domain → Domain → Domain

  field
    [∪]-membership : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ (x ∈ (a ∪ b)) ⟷ (x ∈ a)∨(x ∈ b)))))

  [∪]-commutativity : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ a ∪ b ≡ₛ b ∪ a)))
  [∪]-commutativity =
    ([∀].intro(\{a} →
      ([∀].intro(\{b} →
        ([∀].intro(\{x} →
          ([↔].intro
            (([↔].elimₗ ([∀].elim ([∀].elim ([∀].elim [∪]-membership)))) ∘ [∨].commutativity ∘ ([↔].elimᵣ ([∀].elim ([∀].elim ([∀].elim [∪]-membership)))))
            (([↔].elimₗ ([∀].elim ([∀].elim ([∀].elim [∪]-membership)))) ∘ [∨].commutativity ∘ ([↔].elimᵣ ([∀].elim ([∀].elim ([∀].elim [∪]-membership)))))
          )
        ))
      ))
    ))

  postulate [∪]-associativity : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(c ↦ (a ∪ b) ∪ c ≡ₛ a ∪ (b ∪ c)))))

  module _ ⦃ _ : EmptySet ⦄ where
    open EmptySet ⦃ ... ⦄

    postulate [∪]-identityₗ : Proof(∀ₗ(s ↦ ∅ ∪ s ≡ₛ s))
    postulate [∪]-identityᵣ : Proof(∀ₗ(s ↦ s ∪ ∅ ≡ₛ s))

  postulate [∪]-subsetₗ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ a ⊆ a ∪ b)))
  postulate [∪]-subsetᵣ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ b ⊆ a ∪ b)))
  postulate [∪]-of-subsetₗ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (b ⊆ a) ⟶ (a ∪ b ≡ₛ a))))
  postulate [∪]-of-subsetᵣ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (a ⊆ b) ⟶ (a ∪ b ≡ₛ b))))
  postulate [∪]-of-self : Proof(∀ₗ(s ↦ s ∪ s ≡ₛ s))

-- Intersection operator.
-- Constructs a set which consists of elements which are in both LHS and RHS.
record IntersectionSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  infixl 3001 _∩_
  field
    _∩_ : Domain → Domain → Domain

  field
    [∩]-membership : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ (x ∈ (a ∩ b)) ⟷ (x ∈ a)∧(x ∈ b)))))

  postulate [∩]-commutativity : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ a ∩ b ≡ₛ b ∩ a)))
  postulate [∩]-associativity : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(c ↦ (a ∩ b) ∩ c ≡ₛ a ∩ (b ∩ c)))))

  module _ ⦃ _ : EmptySet ⦄ where
    open EmptySet ⦃ ... ⦄

    postulate [∩]-annihilatorₗ : Proof(∀ₗ(s ↦ ∅ ∩ s ≡ₛ ∅))
    postulate [∩]-annihilatorᵣ : Proof(∀ₗ(s ↦ s ∩ ∅ ≡ₛ s))

  postulate [∩]-subsetₗ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ a ∩ b ⊆ a)))
  postulate [∩]-subsetᵣ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ a ∩ b ⊆ b)))

  postulate [∩]-of-subsetₗ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (b ⊆ a) ⟶ (a ∩ b ≡ₛ b))))
  postulate [∩]-of-subsetᵣ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (a ⊆ b) ⟶ (a ∩ b ≡ₛ a))))
  postulate [∩]-of-self : Proof(∀ₗ(s ↦ s ∩ s ≡ₛ s))

-- "Without"-operator.
-- Constructs a set which consists of elements which are in LHS, but not RHS.
record WithoutSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  infixl 3002 _∖_
  field
    _∖_ : Domain → Domain → Domain

  field
    [∖]-membership : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ (x ∈ (a ∖ b)) ⟷ (x ∈ a)∧(x ∉ b)))))

  postulate [∖]-of-disjoint : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ Disjoint(a)(b) ⟶ (a ∖ b ≡ₛ a)))))

  module _ ⦃ _ : IntersectionSet ⦄ where
    open IntersectionSet ⦃ ... ⦄

    postulate [∖]-of-intersection : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ a ∖ (a ∩ b) ≡ₛ a ∖ b))))

  module _ ⦃ _ : EmptySet ⦄ where
    open EmptySet ⦃ ... ⦄

    postulate [∖]-annihilatorₗ : Proof(∀ₗ(s ↦ ∅ ∖ s ≡ₛ ∅))
    postulate [∖]-identityᵣ : Proof(∀ₗ(s ↦ s ∖ ∅ ≡ₛ s))
    postulate [∖]-subset : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ (a ⊆ b) ⟶ (a ∖ b ≡ₛ ∅)))))
    postulate [∖]-of-self : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ a ∖ a ≡ₛ ∅))))

  module _ ⦃ _ : SingletonSet ⦄ where
    open SingletonSet ⦃ ... ⦄

    postulate [∖]-of-singleton : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ (x ∈ (a ∖ singleton(b))) ⟷ (x ∈ a)∧(x ≢ b)))))

-- Intersection over arbitrary sets.
-- Constructs a set which consists of elements which are in all of the specified sets.
record SetIntersectionSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    ⋂ : Domain → Domain

  field
    [⋂]-membership : Proof(∀ₗ(ss ↦ ∀ₗ(x ↦ (x ∈ ⋂(ss)) ⟷ ∀ₛ(ss)(s ↦ x ∈ s))))

  postulate [⋂]-containing-min : Proof(∀ₗ(s ↦ ∀ₛ(s)(min ↦ ∀ₛ(s)(x ↦ min ⊆ x) ⟶ (⋂(s) ≡ₛ min))))

  module _ ⦃ _ : EmptySet ⦄ where
    open EmptySet ⦃ ... ⦄

    postulate [⋂]-containing-disjoint : Proof(∀ₗ(s ↦ ∃ₛ(s)(a ↦ ∃ₛ(s)(b ↦ Disjoint(a)(b))) ⟶ (⋂(s) ≡ₛ ∅)))
    postulate [⋂]-containing-[∅] : Proof(∀ₗ(s ↦ (∅ ∈ s) ⟶ (⋂(s) ≡ₛ ∅)))

  postulate [⋂]-subset : Proof(∀ₗ(s ↦ ∀ₛ(s)(x ↦ ⋂(s) ⊆ x)))

-- Set of all sets.
record UniversalSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    𝐔 : Domain

  field
    [𝐔]-membership : Proof(∀ₗ(x ↦ (x ∈ 𝐔)))

  [𝐔]-membership-equiv : Proof(∀ₗ(x ↦ (x ∈ 𝐔) ⟷ ⊤))
  [𝐔]-membership-equiv =
    ([∀].intro(\{x} →
      ([↔].intro
        (_ ↦ [∀].elim [𝐔]-membership)
        (_ ↦ [⊤].intro)
      )
    ))

  [𝐔]-subset : Proof(∀ₗ(x ↦ x ⊆ 𝐔))
  [𝐔]-subset =
    ([∀].intro(\{x} →
      ([∀].intro(\{a} →
        ([→].intro(_ ↦
          [∀].elim [𝐔]-membership
        ))
      ))
    ))

  [𝐔]-superset : Proof(∀ₗ(x ↦ (x ⊇ 𝐔) ⟶ (x ≡ₛ 𝐔)))
  [𝐔]-superset =
    ([∀].intro(\{x} →
      ([→].intro(superset ↦
        ([→].elim
          ([∀].elim ([∀].elim [⊆][≡ₛ]-antisymmetry))
          ([∧].intro
            superset
            ([∀].elim [𝐔]-subset)
          )
        )
      ))
    ))

  [𝐔]-contains-self : Proof(𝐔 ∈ 𝐔)
  [𝐔]-contains-self = [∀].elim [𝐔]-membership

  [𝐔]-nonempty : Proof(∃ₗ(x ↦ (x ∈ 𝐔)))
  [𝐔]-nonempty = [∃].intro [𝐔]-contains-self

  module _ ⦃ _ : FilterSet ⦄ where
    open FilterSet ⦃ ... ⦄

    unrestricted-comprehension-contradiction : Proof(⊥)
    unrestricted-comprehension-contradiction =
      ([∨].elim
        (contains ↦
          ([¬].elim
            ([∧].elimᵣ([↔].elimᵣ
              ([∀].elim([∀].elim filter-membership{𝐔}){not-in-self})
              contains
            ))
            contains
          )
        )

        (contains-not ↦
          ([¬].elim
            (contains-not)
            ([↔].elimₗ
              ([∀].elim([∀].elim filter-membership{𝐔}){not-in-self})
              ([∧].intro
                ([∀].elim [𝐔]-membership {not-in-self})
                (contains-not)
              )
            )
          )
        )

        (excluded-middle{not-in-self ∈ not-in-self})
      ) where
        not-in-self : Domain
        not-in-self = filter(𝐔) (x ↦ (x ∉ x))

record TupleSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  infixl 3002 _⨯_
  field
    -- Set product (Set of tuples) (Cartesian product).
    _⨯_ : Domain → Domain → Domain

    -- Tuple value.
    -- An ordered pair of values.
    _,_ : Domain → Domain → Domain

    left : Domain → Domain

    right : Domain → Domain

  swap : Domain → Domain
  swap(x) = (right(x) , left(x))

  field
    [⨯]-membership : Proof(∀ₗ(A ↦ ∀ₗ(B ↦ ∀ₗ(x ↦ (x ∈ (A ⨯ B)) ⟷ ∃ₛ(A)(a ↦ ∃ₛ(B)(b ↦ x ≡ (a , b))))))) -- TODO: Maybe left and right is not neccessary because one can just take the witnesses of this
    left-equality : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ left(a , b) ≡ a)))
    right-equality : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ right(a , b) ≡ b)))

  postulate [⨯]-tuples : Proof(∀ₗ(A ↦ ∀ₗ(B ↦ ∀ₛ(A)(a ↦ ∀ₛ(B)(b ↦ (a , b) ∈ (A ⨯ B))))))
  postulate swap-equality : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ swap(a , b) ≡ (b , a))))
  postulate left-right-identity : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (left(a , b) , right(a , b)) ≡ (a , b))))

record QuotientSet : Type{ℓₘₗ Lvl.⊔ ℓₗ Lvl.⊔ ℓₒ} where
  constructor intro
  field
    -- Quotient set.
    -- The set of equivalence classes.
    _/_ : Domain → BinaryRelator → Domain

    -- Equivalence class
    -- The set of elements which are equivalent to the specified one.
    [_of_] : Domain → (Domain ⨯ₘ BinaryRelator) → Domain

  field
    [/]-membership : ∀{T}{_≅_} → Proof(∀ₗ(x ↦ (x ∈ (T / (_≅_))) ⟷ (∃ₗ(y ↦ x ≡ [ y of (T ,ₘ (_≅_)) ]))))
    eqClass-membership : ∀{T}{_≅_} → Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (a ∈ [ b of (T ,ₘ (_≅_)) ]) ⟷ (a ≅ b))))

  -- module Quotient {T : Domain} {_≅_ : BinaryRelator} ⦃ equivalence : Proof(Structure.Relator.Properties.Equivalence(T)(_≅_)) ⦄ where
  --   open Structure.Relator.Properties

  --   postulate [/]-membership : Proof(∀ₗ(x ↦ (x ∈ (T / (_≅_))) ⟷ (∃ₗ(y ↦ x ≡ [ y of T , (_≅_) ]))))
  --   postulate [/]-pairwise-disjoint : Proof(∀ₗ(x ↦ (x ∈ (T / (_≅_))) ⟷ (∃ₗ(y ↦ x ≡ [ y of T , (_≅_) ]))))
  --   postulate [/]-not-containing-[∅] : Proof(∀ₗ(x ↦ ∅ ∉ (T / (_≅_))))
  --   postulate [/]-cover : Proof(⋃(T / (_≅_)) ≡ T)
  --   postulate eqClass-membership : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (a ∈ [ b of T , (_≅_) ]) ⟷ (a ≅ b))))
  --   postulate eqClass-containing-self : Proof(∀ₗ(a ↦ a ∈ [ a of T , (_≅_) ]))
  --   postulate eqClass-nonempty : Proof(∀ₗ(a ↦ NonEmpty([ a of T , (_≅_) ])))
  --   postulate eqClass-equal-disjoint : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ([ a of T , (_≅_) ] ≡ [ b of T , (_≅_) ]) ⟷ ¬ Disjoint([ a of T , (_≅_) ])([ b of T , (_≅_) ]))))
  --   postulate eqClass-equal-equivalent : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ([ a of T , (_≅_) ] ≡ [ b of T , (_≅_) ]) ⟷ (a ≅ b))))
  --   postulate eqClass-equal-containingₗ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ([ a of T , (_≅_) ] ≡ [ b of T , (_≅_) ]) ⟷ (b ∈ [ a of T , (_≅_) ]))))
  --   postulate eqClass-equal-containingᵣ : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ([ a of T , (_≅_) ] ≡ [ b of T , (_≅_) ]) ⟷ (a ∈ [ b of T , (_≅_) ]))))

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:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

module Dijkstra.All where

open import Dijkstra.Syntax public
open import Dijkstra.RWS public
open import Dijkstra.RWS.Syntax public
open import Dijkstra.EitherD public
open import Dijkstra.EitherD.Syntax public
open import Dijkstra.EitherLike public


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

module Categories.Functor.Monoidal where

open import Level
open import Data.Product using (Σ; _,_)

open import Categories.Category
open import Categories.Category.Product
open import Categories.Category.Monoidal

open import Categories.Functor hiding (id)
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.NaturalIsomorphism

import Categories.Morphism as Mor

private
  variable
    o o′ ℓ ℓ′ e e′ : Level

module _  (C : MonoidalCategory o ℓ e) (D : MonoidalCategory o′ ℓ′ e′) where
  private
    module C = MonoidalCategory C
    module D = MonoidalCategory D
    open Mor D.U

  -- lax monoidal functor
  record IsMonoidalFunctor (F : Functor C.U D.U) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F

    field
      ε      : D.U [ D.unit , F₀ C.unit ]
      ⊗-homo : NaturalTransformation (D.⊗ ∘F (F ⁂ F)) (F ∘F C.⊗)

    module ⊗-homo = NaturalTransformation ⊗-homo

    -- coherence condition
    open D
    open Commutation D.U

    field
      associativity : ∀ {X Y Z} →
                      [ (F₀ X ⊗₀ F₀ Y) ⊗₀ F₀ Z ⇒ F₀ (X C.⊗₀ Y C.⊗₀ Z) ]⟨
                        ⊗-homo.η (X , Y) ⊗₁ id                        ⇒⟨ F₀ (X C.⊗₀ Y) ⊗₀ F₀ Z ⟩
                        ⊗-homo.η (X C.⊗₀ Y , Z)                       ⇒⟨ F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ⟩
                        F₁ C.associator.from
                      ≈ associator.from                               ⇒⟨ F₀ X ⊗₀ F₀ Y ⊗₀ F₀ Z ⟩
                        id ⊗₁ ⊗-homo.η (Y , Z)                        ⇒⟨ F₀ X ⊗₀ F₀ (Y C.⊗₀ Z) ⟩
                        ⊗-homo.η (X , Y C.⊗₀ Z)
                      ⟩
      unitaryˡ      : ∀ {X} →
                      [ unit ⊗₀ F₀ X ⇒ F₀ X   ]⟨
                        ε ⊗₁ id               ⇒⟨ F₀ C.unit ⊗₀ F₀ X ⟩
                        ⊗-homo.η (C.unit , X) ⇒⟨ F₀ (C.unit C.⊗₀ X) ⟩
                        F₁ C.unitorˡ.from
                      ≈ unitorˡ.from
                      ⟩
      unitaryʳ      : ∀ {X} →
                      [ F₀ X ⊗₀ unit ⇒ F₀ X   ]⟨
                        id ⊗₁ ε               ⇒⟨ F₀ X ⊗₀ F₀ C.unit ⟩
                        ⊗-homo.η (X , C.unit) ⇒⟨ F₀ (X C.⊗₀ C.unit) ⟩
                        F₁ C.unitorʳ.from
                      ≈ unitorʳ.from
                      ⟩

  record MonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F          : Functor C.U D.U
      isMonoidal : IsMonoidalFunctor F

    open Functor F public
    open IsMonoidalFunctor isMonoidal public

  -- strong monoidal functor
  record IsStrongMonoidalFunctor (F : Functor C.U D.U) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
    open Functor F

    field
      ε      : D.unit ≅ F₀ C.unit
      ⊗-homo : D.⊗ ∘F (F ⁂ F) ≃ F ∘F C.⊗

    module ε      = _≅_ ε
    module ⊗-homo = NaturalIsomorphism ⊗-homo

    -- coherence condition
    open D
    open Commutation D.U

    field
      associativity : ∀ {X Y Z} →
                      [ (F₀ X ⊗₀ F₀ Y) ⊗₀ F₀ Z ⇒ F₀ (X C.⊗₀ Y C.⊗₀ Z) ]⟨
                        ⊗-homo.⇒.η (X , Y) ⊗₁ id                        ⇒⟨ F₀ (X C.⊗₀ Y) ⊗₀ F₀ Z ⟩
                        ⊗-homo.⇒.η (X C.⊗₀ Y , Z)                      ⇒⟨ F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ⟩
                        F₁ C.associator.from
                      ≈ associator.from                                 ⇒⟨ F₀ X ⊗₀ F₀ Y ⊗₀ F₀ Z ⟩
                        id ⊗₁ ⊗-homo.⇒.η (Y , Z)                        ⇒⟨ F₀ X ⊗₀ F₀ (Y C.⊗₀ Z) ⟩
                        ⊗-homo.⇒.η (X , Y C.⊗₀ Z)
                      ⟩
      unitaryˡ      : ∀ {X} →
                      [ unit ⊗₀ F₀ X ⇒ F₀ X      ]⟨
                        ε.from ⊗₁ id             ⇒⟨ F₀ C.unit ⊗₀ F₀ X ⟩
                        ⊗-homo.⇒.η (C.unit , X) ⇒⟨ F₀ (C.unit C.⊗₀ X) ⟩
                        F₁ C.unitorˡ.from
                      ≈ unitorˡ.from
                      ⟩
      unitaryʳ      : ∀ {X} →
                      [ F₀ X ⊗₀ unit ⇒ F₀ X      ]⟨
                        id ⊗₁ ε.from             ⇒⟨ F₀ X ⊗₀ F₀ C.unit ⟩
                        ⊗-homo.⇒.η (X , C.unit) ⇒⟨ F₀ (X C.⊗₀ C.unit) ⟩
                        F₁ C.unitorʳ.from
                      ≈ unitorʳ.from
                      ⟩

    isMonoidal : IsMonoidalFunctor F
    isMonoidal = record
      { ε             = ε.from
      ; ⊗-homo        = ⊗-homo.F⇒G
      ; associativity = associativity
      ; unitaryˡ      = unitaryˡ
      ; unitaryʳ      = unitaryʳ
      }

  record StrongMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      F : Functor C.U D.U
      isStrongMonoidal : IsStrongMonoidalFunctor F

    open Functor F public
    open IsStrongMonoidalFunctor isStrongMonoidal public

    monoidalFunctor : MonoidalFunctor
    monoidalFunctor = record { F = F ; isMonoidal = isMonoidal }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Issue2880 where

app : {A : Set} → (A → A) → (A → A)
app f x = f x

{-# COMPILE GHC app = \ A f x -> f (app A f x) #-}

mutual

  id : {A : Set} → A → A
  id x = x

  {-# COMPILE GHC id = id' #-}

  id' : {A : Set} → A → A
  id' x = x

  {-# COMPILE GHC id' = id #-}


text:
------------------------------------------------------------------------------
-----                                                                    -----
-----     Relevant.Abstraction                                           -----
-----                                                                    -----
------------------------------------------------------------------------------

module Relevant.Abstraction where

open import Lib.Equality
open import Lib.Sigma
open import Lib.Bwd
open import Thin.Data
open import Thin.Thinned

module _ {B : Set} where

 open THIN {B}

{-
A scoped notion of abstraction brings a newly bound variable into scope at the
local end of the context.
-}

------------------------------------------------------------------------------
-- relevance-aware abstraction
------------------------------------------------------------------------------

{-
CodeBruijn syntax is not necessarily intended to restrict the use of variables
more or less than ordinary syntax-with-binding, but it is intended to ensure
greater awareness of how variables are used.

In particular, we use types Foo ga to mean the type of Foos with support ga,
i.e., that the variables from ga not only may but must occur free in the Foo.

Now, when we bind a variable to make an abstraction of some sort, there is
nobody to tell us whether the bound variable must be used. But we must make
our minds up: if we bring it into scope, it must be used; if we do not, it
cannot be used. Let us therefore offer the choice of which to do.
-}

 infixr 8 _|-_
 data _|-_ (b : B)(T : Scope -> Set)(ga : Scope) : Set where
   ll : T (ga -, b) -> (b |- T) ga    -- two-l llambda, he's a beast
   kk : T ga        -> (b |- T) ga    -- two-k kkonstant, he's the least

------------------------------------------------------------------------------
-- smart constructor for thinned abstraction
------------------------------------------------------------------------------

 infixr 4 _\\_
 _\\_ : forall b {T : Scope -> Set}{ga} -> T :< ga -, b -> (b |- T) :< ga
 b \\ t ^ th -, .b = ll t ^ th
 b \\ t ^ th -^ .b = kk t ^ th

{-
We can tell the support of t by looking at the thinning that it is paired
with. We learn which constructor we should then use.
-}

------------------------------------------------------------------------------
-- smart destructor for thinned abstraction
------------------------------------------------------------------------------

 data Under {b T ga} : (b |- T) :< ga -> Set where
   un\\ : forall t -> Under (b \\ t)

 under : forall {b T ga}(x : (b |- T) :< ga) -> Under x
 under (ll t ^ th) = un\\ (t ^ th -, _)
 under (kk t ^ th) = un\\ (t ^ th -^ _)

 under\\ : forall b {T ga}(t : T :< ga -, b) -> under (b \\ t) ~ un\\ t
 under\\ b (_ ^ th -, .b) = r~
 under\\ b (_ ^ th -^ .b) = r~

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module ProofRep where

import Prelude
import Logic.Relations
import Logic.Identity
import Data.Nat
import Data.Nat.Properties

open Prelude
open Data.Nat hiding (_==_; _≡_)
open Data.Nat.Properties
open Logic.Relations

module Foo (Var : Set) where

  data _==_ : (x y : Var) -> Set where
    cRefl  : {x : Var} -> x == x
    cSym   : {x y : Var} -> y == x -> x == y
    cTrans : {x y z : Var} -> x == z -> z == y -> x == y
    cAxiom : {x y : Var} -> x == y

  data Axioms {A : Set}(_≈_ : Rel A)([_] : Var -> A) : Set where
    noAxioms   : Axioms _≈_ [_]
    anAxiom    : (x y : Var) -> [ x ] ≈ [ y ] -> Axioms _≈_ [_]
    manyAxioms : Axioms _≈_ [_] -> Axioms _≈_ [_] -> Axioms _≈_ [_]

  refl : {x : Var} -> x == x
  refl = cRefl

  sym : {x y : Var} -> x == y -> y == x
  sym (cRefl xy)     = cRefl (Var.sym xy)
  sym  cAxiom        = cSym cAxiom
  sym (cSym p)       = p
  sym (cTrans z p q) = cTrans z (sym q) (sym p)

  trans : {x y z : Var} -> x == y -> y == z -> x == z
  trans {x}{y}{z} (cRefl xy) q     = Var.subst (\w -> w == z) (Var.sym xy) q
  trans {x}{y}{z} p (cRefl yz)     = Var.subst (\w -> x == w) yz p
  trans {x}{y}{z} (cTrans w p q) r = cTrans w p (trans q r)
  trans           p q              = cTrans _ p q


text:
------------------------------------------------------------------------------
-- The ABP using the Agda standard library
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.ABP.ABP-SL where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Data.Bool
open import Data.Product
open import Relation.Nullary

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

Bit : Set
Bit = Bool

-- Data type used to model the fair unreliable transmission channel.
data Err (A : Set) : Set where
  ok    : (x : A) → Err A
  error : Err A

-- The mutual sender functions.

-- TODO (2019-01-04): Agda doesn't accept this definition which was
-- accepted by a previous version.
{-# TERMINATING #-}

sendA  : {A : Set} → Bit → Stream A → Stream (Err Bit) → Stream (A × Bool)
awaitA : {A : Set} → Bit → Stream A → Stream (Err Bit) → Stream (A × Bit)

sendA b (i ∷ is) ds = (i , b) ∷ ♯ awaitA b (i ∷ is) ds

awaitA b (i ∷ is) (ok b' ∷ ds) with b ≟ b'
... | yes p = sendA (not b) (♭ is) (♭ ds)
... | no ¬p = (i , b) ∷ ♯ (awaitA b (i ∷ is) (♭ ds))
awaitA b (i ∷ is) (error ∷ ds) = (i , b) ∷ ♯ (awaitA b (i ∷ is) (♭ ds))

-- The receiver functions.

-- TODO (2019-01-04): Agda doesn't accept this definition which was
-- accepted by a previous version.
{-# TERMINATING #-}
ackA : {A : Set} → Bit → Stream (Err (A × Bit)) → Stream Bit
ackA b (ok (_ , b') ∷ bs) with b ≟ b'
... | yes p = b ∷ ♯ (ackA (not b) (♭ bs))
... | no ¬p = not b ∷ ♯ (ackA b (♭ bs))
ackA b (error ∷ bs) = not b ∷ ♯ (ackA b (♭ bs))

-- 25 June 2014. Requires the TERMINATING flag when using
-- --without-K. See Agda Issue 1214.

-- TODO (03 December 2015): Report the issue.

{-# TERMINATING #-}
outA : {A : Set} → Bit → Stream (Err (A × Bit)) → Stream A
outA b (ok (i , b') ∷ bs) with b ≟ b'
... | yes p = i ∷ ♯ (outA (not b) (♭ bs))
... | no ¬p = outA b (♭ bs)
outA b (error ∷ bs) = outA b (♭ bs)

-- Model the fair unreliable tranmission channel.

-- TODO (2019-01-04): Agda doesn't accept this definition which was
-- accepted by a previous version.
{-# TERMINATING #-}
corruptA : {A : Set} → Stream Bit → Stream A → Stream (Err A)
corruptA (true ∷ os)  (_ ∷ xs) = error ∷ ♯ (corruptA (♭ os) (♭ xs))
corruptA (false ∷ os) (x ∷ xs) = ok x ∷ ♯ (corruptA (♭ os) (♭ xs))

-- 25 June 2014. Requires the TERMINATING flag when using
-- --without-K. See Agda Issue 1214.

-- TODO (03 December 2015): Report the issue.

-- The ABP transfer function.
{-# TERMINATING #-}
abpTransA : {A : Set} → Bit → Stream Bit → Stream Bit → Stream A → Stream A
abpTransA {A} b os₁ os₂ is = outA b bs
  where
  as : Stream (A × Bit)
  bs : Stream (Err (A × Bit))
  cs : Stream Bit
  ds : Stream (Err Bit)

  as = sendA b is ds
  bs = corruptA os₁ as
  cs = ackA b bs
  ds = corruptA os₂ cs

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Encode
open import Util.PKCS                            as PKCS hiding (sign)
open import Util.Prelude

module LibraBFT.Impl.Types.ValidatorSigner where

sign : {C : Set} ⦃ enc : Encoder C ⦄ → ValidatorSigner → C → Signature
sign (ValidatorSigner∙new _ sk) c = PKCS.sign-encodable c sk

postulate -- TODO-1: publicKey_USE_ONLY_AT_INIT
  publicKey_USE_ONLY_AT_INIT : ValidatorSigner → PK

obmGetValidatorSigner : AuthorName → List ValidatorSigner → Either ErrLog ValidatorSigner
obmGetValidatorSigner name vss =
  case List-filter go vss of λ where
    (vs ∷ []) → pure vs
    _         → Left fakeErr -- [ "ValidatorSigner", "obmGetValidatorSigner"
                             -- , name , "not found in"
                             -- , show (fmap (^.vsAuthor.aAuthorName) vss) ]
 where
  go : (vs : ValidatorSigner) → Dec (vs ^∙ vsAuthor ≡ name)
  go (ValidatorSigner∙new _vsAuthor _) = _vsAuthor ≟ name


text:
module JMEq where

data _==_ {A : Set}(x : A) : {B : Set}(y : B) -> Set where
  refl : x == x

subst : {A : Set}{x y : A}(P : A -> Set) -> x == y -> P x -> P y
subst {A} P refl px = px