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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.NType2
open import lib.PathGroupoid

open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas

module nicolai.pseudotruncations.SeqColim where

Sequence : ∀ {i} → Type (lsucc i)
Sequence {i} = Σ (ℕ → Type i)
              (λ A → (n : ℕ) → A n → A (S n))

module _ {i} where

  private
    data #SeqCo-aux (C : Sequence {i}) : Type i where
      #ins : (n : ℕ) → (fst C n) → #SeqCo-aux C

    data #SeqCo (C : Sequence {i}) : Type i where
      #trick-aux : #SeqCo-aux C → (Unit → Unit) → #SeqCo C

  SeqCo : (C : Sequence {i}) → Type i
  SeqCo = #SeqCo

  ins : {C : Sequence {i}} → (n : ℕ) → (fst C n) → SeqCo C
  ins {C} n a = #trick-aux (#ins n a) _

  postulate
    glue : {C : Sequence {i}} → (n : ℕ) → (a : fst C n)
                           → (ins {C} n a) == (ins (S n) (snd C n a))

  module SeqCoInduction {C : Sequence {i}} {j} {P : SeqCo C → Type j}
                   (Ins : (n : ℕ) → (a : fst C n) → P (ins n a))
                   (Glue : (n : ℕ) → (a : fst C n)
                   → (Ins n a) == (Ins (S n) (snd C n a)) [ P ↓ (glue n a) ])
                   where
    f : Π (SeqCo C) P
    f = f-aux phantom where
      f-aux : Phantom Glue → Π (SeqCo C) P
      f-aux phantom (#trick-aux (#ins n a) _) = Ins n a

    postulate
      pathβ : (n : ℕ) → (a : fst C n) → apd f (glue n a) == (Glue n a)

open SeqCoInduction public renaming (f to SeqCo-ind ; pathβ to SeqCo-ind-pathβ)

{- we now have the induction principle [SeqCo-ind] with judgmental computation
   on points and 'homotopy' computation [SeqCo-ind-pathβ] on paths.
-}

module SeqCoRec {i j} {C : Sequence {i}} {B : Type j}
                (Ins : (n : ℕ) → (fst C n) → B)
                (Glue : (n : ℕ) → (a : fst C n)
                → (Ins n a) == (Ins (S n) (snd C n a)))
                where

  private
    module M = SeqCoInduction {C = C} {P = λ _ → B} Ins (λ n a → ↓-cst-in (Glue n a))

  f : SeqCo C → B
  f = M.f

  pathβ : (n : ℕ) → (a : fst C n) → ap f (glue n a) == (Glue n a)
  pathβ n a = apd=cst-in {f = f} (M.pathβ n a)

open SeqCoRec public renaming (f to SeqCo-rec ; pathβ to SeqCo-rec-pathβ)

{- we now further have the recursion principle [SeqCo-rec],
   which of course is just a special case of [SeqCo-ind]
-}

{- remove the first segment of a sequence -}
removeFst : ∀ {i} → Sequence {i} → Sequence {i}
removeFst (A , f) = (λ n → A (S n)) , (λ n → f (S n))

{- removing the first segment does not change the colimit -}
module ignoreFst {i} (C : Sequence {i}) where

  A = fst C
  f = snd C
  SC = SeqCo C

  C' = removeFst C
  A' = fst C'
  f' = snd C'
  SC' = SeqCo C'

  k-ins : (n : ℕ) → A n → SC'
  k-ins O a = ins O (f O a)
  k-ins (S n) a = ins n a

  k-glue : (n : ℕ) (a : A n) → k-ins n a == k-ins (S n) (f n a)
  k-glue O a = idp
  k-glue (S n) a = glue n a

  -- the first map
  k : SC → SC'
  k = SeqCo-rec {C = C} {B = SC'} k-ins k-glue

  m-ins : (n : ℕ) → A' n → SC
  m-ins n a' = ins (S n) a'

  m-glue : (n : ℕ) (a' : A' n) → m-ins n a' == m-ins (S n) (f' n a')
  m-glue n a' = glue (S n) a'

  -- the second map
  m : SC' → SC
  m = SeqCo-rec {C = C'} {B = SC} m-ins m-glue

  -- aux
  km-glue-comp : (n : ℕ) (a' : A' n) → ap (k ∘ m) (glue n a') == glue n a'
  km-glue-comp n a' =
    ap (k ∘ m) (glue n a')
      =⟨ ap-∘ _ _ _ ⟩
    ap k (ap m (glue n a'))
      =⟨ ap (λ p → ap k p) (SeqCo-rec-pathβ m-ins m-glue _ _) ⟩
    ap k (glue (S n) a')
      =⟨ SeqCo-rec-pathβ k-ins k-glue _ _ ⟩
    glue n a'
      ∎

  -- one direction, preparation
  km-ins : (n : ℕ) → (a' : A' n) → k (m (ins n a')) == ins n a'
  km-ins n a' = idp

  km-glue : (n : ℕ) → (a' : A' n) → (km-ins n a') == (km-ins (S n) (f' n a')) [(λ x' → k (m x') == x') ↓ (glue n a')]
  km-glue n a' = from-transp (λ x' → k (m x') == x') (glue n a')
                   (transport (λ x' → k (m x') == x') (glue n a') (km-ins n a')
                     =⟨ trans-ap {A = SC'} {B = SC'} (k ∘ m) (idf SC') (glue n a') (km-ins n a') ⟩
                   ! (ap (k ∘ m) (glue n a')) ∙ ap (idf SC') (glue n a')
                     =⟨ ap (λ p → (! (ap (k ∘ m) (glue n a'))) ∙ p) (ap-idf _) ⟩
                   ! (ap (k ∘ m) (glue n a')) ∙ (glue n a')
                     =⟨ ap (λ p → ! p ∙ (glue n a')) (km-glue-comp n a') ⟩
                   ! (glue n a') ∙ (glue n a')
                     =⟨ !-inv-l (glue n a') ⟩
                   km-ins (S n) (f' n a')
                     ∎ )

  -- one direction
  km : (x' : SC') → k (m x') == x'
  km = SeqCo-ind {P = λ x' → k (m x') == x'} km-ins km-glue

  -- other direction, preparation
  mk-ins : (n : ℕ) → (a : A n) → m (k (ins n a)) == ins n a
  mk-ins O a = ! (glue 0 a)
  mk-ins (S n) a = idp

  -- auxiliary calculation
  mk-glue-comp : (n : ℕ) → (a : A n) → mk-ins n a ∙ glue n a == ap (m ∘ k) (glue n a)
  mk-glue-comp O a =
    mk-ins O a ∙ glue O a
      =⟨ !-inv-l (glue O a) ⟩
    idp
      =⟨ idp ⟩
    ap m (idp {a = ins O (f O a)})
      =⟨ ap (λ p → ap m p) (! (SeqCo-rec-pathβ k-ins k-glue O a)) ⟩
    ap m (ap k (glue O a))
      =⟨ ! (ap-∘ m k _) ⟩
    ap (m ∘ k) (glue O a)
      ∎
  mk-glue-comp (S n) a =
    mk-ins (S n) a ∙ glue (S n) a
      =⟨ idp ⟩
    glue (S n) a
      =⟨ ! (SeqCo-rec-pathβ m-ins m-glue n a) ⟩
    ap m (glue n a)
      =⟨ ap (λ p → ap m p) (! (SeqCo-rec-pathβ k-ins k-glue (S n) a)) ⟩
    ap m (ap k (glue (S n) a))
      =⟨ ! (ap-∘ m k _) ⟩
    ap (m ∘ k) (glue (S n) a)
      ∎

  mk-glue : (n : ℕ) → (a : A n) → (mk-ins n a) == (mk-ins (S n) (f n a)) [(λ x → m (k x) == x) ↓ (glue n a)]
  mk-glue n a = from-transp (λ x → m (k x) == x) (glue n a)
                  (transport (λ x → m (k x) == x) (glue n a) (mk-ins n a)
                    =⟨ trans-ap (m ∘ k) (idf _) (glue n a) (mk-ins n a) ⟩
                  ! (ap (m ∘ k) (glue n a)) ∙ mk-ins n a ∙ ap (idf SC) (glue n a)
                    =⟨ ap (λ p → ! (ap (m ∘ k) (glue n a)) ∙ (mk-ins n a) ∙ p) (ap-idf (glue n a)) ⟩
                  ! (ap (m ∘ k) (glue n a)) ∙ mk-ins n a ∙ (glue n a)
                    =⟨ ap (λ p → (! (ap (m ∘ k) (glue n a))) ∙ p) (mk-glue-comp n a) ⟩
                  ! (ap (m ∘ k) (glue n a)) ∙ ap (m ∘ k) (glue n a)
                    =⟨ !-inv-l (ap (m ∘ k) (glue n a)) ⟩
                  idp
                    =⟨ idp ⟩
                  mk-ins (S n) (f n a)
                    ∎)

  -- other direction
  mk : (x : SC) → m (k x) == x
  mk = SeqCo-ind {P = λ x → m (k x) == x} mk-ins mk-glue

  remove : SC ≃ SC'
  remove = equiv k m km mk

{- summarized -}
ignore-fst : ∀ {i} → (C : Sequence {i}) → (SeqCo C) ≃ (SeqCo (removeFst C))
ignore-fst C = ignoreFst.remove C

{- Now, we do this n times instead of once ...-}

removeInit : ∀ {i} → (C : Sequence {i}) → (n : ℕ) → Sequence {i}
removeInit C O = C
removeInit C (S n) = removeInit (removeFst C) n

ignore-init-aux : ∀ {i} → (C C' : Sequence {i}) → (SeqCo C) ≃ (SeqCo C') → (n : ℕ) → (SeqCo C) ≃ (SeqCo (removeInit C' n))
ignore-init-aux C C' e O = e
ignore-init-aux C C' e (S n) =
  ignore-init-aux C (removeFst C') (ignore-fst C' ∘e e) n

{- Result: the sequential colimit of a sequence stays the same if we remove
   an initial finite segment of the sequence.
-}
ignore-init : ∀ {i} → (C : Sequence {i}) → (n : ℕ) → (SeqCo C) ≃ (SeqCo (removeInit C n))
ignore-init C = ignore-init-aux C C (ide _)

-- TODO do we need this?
{- if we have a sequence and a point of the first type,
   we get a point of the type after removing some initial segment
-}
new-initial : ∀ {i} (C : Sequence {i}) (n : ℕ) →  (fst C n) → fst (removeInit C n) O
new-initial C O a₀ = a₀
new-initial C (S n) a₀ = new-initial (removeFst C) n a₀

module _ {i} (C : Sequence {i}) (a₀ : fst C O) where

  {- nearly the same as above:
     lift the 'starting point' a₀ to any later type -}
  lift-point : (n : ℕ) → fst C n
  lift-point O = a₀
  lift-point (S n) = snd C n (lift-point n)

  {- this is more special than in the text, as we only consider (0,n), not (k,n) -}
  {- In the colimit, the lifted point is equal to the 'starting point' -}
  lift-point-= : (n : ℕ) → ins {C = C} O a₀ == ins n (lift-point n)
  lift-point-= O = idp
  lift-point-= (S n) = (lift-point-= n) ∙ glue n _

{- Finally, an important definition: We say that a sequence is weakly constant
   if each map is weakly constant. -}
wconst-chain : ∀ {i} → Sequence {i} → Type i
wconst-chain (A , f) = (n : ℕ) → wconst (f n)

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-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
-}
open import LibraBFT.Lemmas
open import LibraBFT.Prelude
open import LibraBFT.Base.Encode
open import LibraBFT.Base.ByteString

-- This module contains a model of cryptographic signatures on
-- certain data structures, and creation and verification
-- thereof.  These data structures, defined by the WithVerSig
-- type, can be optionally signed, and if they are signed, the
-- signature covers a ByteString derived from the data structure,
-- enabling support for signature that cover only (functions of)
-- specific parts of the data structure.  The module also
-- contains some properties we have found useful in other
-- contexts, though they are not yet used in this repo.

module LibraBFT.Base.PKCS where

 postulate -- valid assumption
   signature-size : ℕ

 Signature : Set
 Signature = Σ ByteString (λ s → length s ≡ signature-size)

 postulate -- valid assumptions
   PK : Set
   SK : Set
   IsKeyPair : PK → SK → Set
   _≟PK_ : (pk1 pk2 : PK) → Dec (pk1 ≡ pk2)

   instance
     enc-PK    : Encoder PK
     enc-SigMB : Encoder (Maybe Signature)

   sign-raw : ByteString → SK → Signature
   verify   : ByteString → Signature → PK → Bool

   -- We assume no "signature collisions", as represented by verify-pk-inj
   verify-pk-inj : ∀{bs sig pk pk'}
                 → verify bs sig pk  ≡ true
                 → verify bs sig pk' ≡ true
                 → pk ≡ pk'

   verify-bs-inj : ∀{bs bs' sig pk}
                 → verify bs  sig pk ≡ true
                 → verify bs' sig pk ≡ true
                 → bs ≡ bs'

   verify-sign : ∀{bs pk sk}
               → IsKeyPair pk sk
               → verify bs (sign-raw bs sk) pk ≡ true

   verify-fail : ∀{bs pk sk}
               → ¬ IsKeyPair pk sk
               → verify bs (sign-raw bs sk) pk ≡ false

   -- We consider a PK to be (permanently) either honest or not,
   -- respresented by the following postulate.  This is relevant
   -- in reasoning about possible behaviours of a modeled system.
   -- Specifically, the secret key corresponding to an honest PK
   -- is assumed not to be leaked, ensuring that cheaters cannot
   -- forge new signatures for honest PKs.  Furthermore, if a peer
   -- is assigned we use possession
   -- of an honest PK in a given epoch to modelWe will postulate that, among
   -- the PKs chosen for a particular epoch, the number of them
   -- that are dishonest is at most the number of faults to be
   -- tolerated for that epoch.  This definition is /meta/: the
   -- information about which PKs are (dis)honest should never be
   -- used by the implementation -- it is only for modeling and
   -- proofs.
   Meta-Dishonest-PK : PK → Set

   Meta-DishonestPK? : (pk : PK) → Dec (Meta-Dishonest-PK pk)

 verify-pi : ∀{bs sig pk}
           → (v1 : verify bs sig pk ≡ true)
           → (v2 : verify bs sig pk ≡ true)
           → v1 ≡ v2
 verify-pi {bs} {sig} {pk} _ _
    with verify bs sig pk
 verify-pi {bs} {sig} {pk} refl refl | .true = refl

 Meta-Honest-PK : PK → Set
 Meta-Honest-PK  = ¬_ ∘ Meta-Dishonest-PK

 -- A datatype C might that might carry values with
 -- signatures should be an instance of 'WithSig' below.
 record WithSig (C : Set) : Set₁ where
   field
     -- A decidable predicate indicates whether values have
     -- been signed
     Signed         : C → Set
     Signed-pi      : ∀ (c : C)
                    → (is1 : Signed c)
                    → (is2 : Signed c)
                    → is1 ≡ is2
     isSigned?      : (c : C) → Dec (Signed c)

     -- Signed values must have a signature
     signature      : (c : C)(hasSig : Signed c) → Signature

     -- All values must be /encoded/ into a ByteString that
     -- is supposed to be verified against a signature.
     signableFields : C → ByteString
 open WithSig {{...}} public

 sign : {C : Set} ⦃ ws : WithSig C ⦄ → C → SK → Signature
 sign c = sign-raw (signableFields c)

 Signature≡ : {C : Set} ⦃ ws : WithSig C ⦄ → C → Signature → Set
 Signature≡ c sig = Σ (Signed c) (λ s → signature c s ≡ sig)

 -- A value of a datatype C can have its signature
 -- verified; A value of type WithVerSig c is a proof of that.
 -- Hence; the set (Σ C WithVerSig) is the set of values of
 -- type C with verified signatures.
 record WithVerSig {C : Set} ⦃ ws : WithSig C ⦄ (pk : PK) (c : C) : Set where
   constructor mkWithVerSig
   field
     isSigned  : Signed c
     verified  : verify (signableFields c) (signature c isSigned) pk
               ≡ true
 open WithVerSig public

 ver-signature : ∀{C pk}⦃ ws : WithSig C ⦄{c : C} → WithVerSig pk c → Signature
 ver-signature {c = c} wvs = signature c (isSigned wvs)

 verCast : {C : Set} ⦃ ws : WithSig C ⦄ {c : C} {is1 is2 : Signed c} {pk1 pk2 : PK}
         → verify (signableFields c) (signature c is1) pk1 ≡ true
         → pk1 ≡ pk2
         → is1 ≡ is2
         → verify (signableFields c) (signature c is2) pk2 ≡ true
 verCast prf refl refl = prf

 wvsCast : {C : Set} ⦃ ws : WithSig C ⦄ {c : C} {pk1 pk2 : PK}
         → WithVerSig pk1 c
         → pk2 ≡ pk1
         → WithVerSig pk2 c
 wvsCast {c = c} wvs refl = wvs

 withVerSig-≡ : {C : Set} ⦃ ws : WithSig C ⦄ {pk : PK} {c : C}
              → {wvs1 : WithVerSig pk c}
              → {wvs2 : WithVerSig pk c}
              → isSigned  wvs1 ≡ isSigned  wvs2
              → wvs1 ≡ wvs2
 withVerSig-≡ {wvs1 = wvs1} {wvs2 = wvs2} refl
    with verified wvs2 | inspect verified wvs2 | verCast (verified wvs1) refl refl
 ...| vwvs2 | [ R ] | vwvs1 rewrite verify-pi vwvs1 vwvs2 | sym R = refl

 withVerSig-pi : {C : Set} {pk : PK} {c : C} ⦃ ws : WithSig C ⦄
               → (wvs1 : WithVerSig pk c)
               → (wvs2 : WithVerSig pk c)
               → wvs2 ≡ wvs1
 withVerSig-pi {C} {pk} {c} ⦃ ws ⦄ wvs2 wvs1
    with isSigned? c
 ...| no ¬Signed = ⊥-elim (¬Signed (isSigned wvs1))
 ...| yes sc = withVerSig-≡ {wvs1 = wvs1} {wvs2 = wvs2} (Signed-pi c (isSigned wvs1) (isSigned wvs2))

 data SigCheckResult {C : Set} ⦃ ws : WithSig C ⦄ (pk : PK) (c : C) : Set where
   notSigned   : ¬ Signed c → SigCheckResult pk c
   checkFailed : (sc : Signed c) → verify (signableFields c) (signature c sc) pk ≡ false → SigCheckResult pk c
   sigVerified : WithVerSig pk c → SigCheckResult pk c

 checkFailed≢sigVerified : {C : Set} ⦃ ws : WithSig C ⦄ {pk : PK} {c : C}
                           {wvs : WithVerSig ⦃ ws ⦄ pk c}
                           {sc : Signed c} {v : verify (signableFields c) (signature c sc) pk ≡ false}
                         → checkFailed sc v ≡ sigVerified wvs → ⊥
 checkFailed≢sigVerified ()

 data SigCheckOutcome : Set where
   notSigned   : SigCheckOutcome
   checkFailed : SigCheckOutcome
   sigVerified : SigCheckOutcome

 data SigCheckFailed : Set where
   notSigned   : SigCheckFailed
   checkFailed : SigCheckFailed

 check-signature : {C : Set} ⦃ ws : WithSig C ⦄ → (pk : PK) → (c : C) → SigCheckResult pk c
 check-signature pk c with isSigned? c
 ...| no  ns  = notSigned ns
 ...| yes sc with verify (signableFields c) (signature c sc) pk
                | inspect (verify (signableFields c) (signature c sc)) pk
 ...| false | [ nv ] = checkFailed sc nv
 ...| true  | [ v  ] = sigVerified (record { isSigned  = sc
                                           ; verified  = v })

 sigCheckOutcomeFor : {C : Set} ⦃ ws : WithSig C ⦄ (pk : PK) (c : C) → SigCheckOutcome
 sigCheckOutcomeFor pk c with check-signature pk c
 ...| notSigned _     = notSigned
 ...| checkFailed _ _ = checkFailed
 ...| sigVerified _   = sigVerified

 sigVerifiedVerSigCS : {C : Set} ⦃ ws : WithSig C ⦄ {pk : PK} {c : C}
                     → sigCheckOutcomeFor pk c ≡ sigVerified
                     → ∃[ wvs ] (check-signature ⦃ ws ⦄ pk c ≡ sigVerified wvs)
 sigVerifiedVerSigCS {pk = pk} {c = c} prf
    with  check-signature pk  c | inspect
         (check-signature pk) c
 ...| sigVerified verSig | [ R ] rewrite R =  verSig , refl

 sigVerifiedVerSig : {C : Set} ⦃ ws : WithSig C ⦄ {pk : PK} {c : C}
                   → sigCheckOutcomeFor pk c ≡ sigVerified
                   → WithVerSig pk c
 sigVerifiedVerSig = proj₁ ∘ sigVerifiedVerSigCS

 sigVerifiedSCO : {C : Set} ⦃ ws : WithSig C ⦄ {pk : PK} {c : C}
                   → (wvs : WithVerSig pk c)
                   → sigCheckOutcomeFor pk c ≡ sigVerified
 sigVerifiedSCO {pk = pk} {c = c} wvs
   with check-signature pk c
 ...| notSigned  ns      = ⊥-elim (ns (isSigned wvs))
 ...| checkFailed xx xxs rewrite Signed-pi c xx (isSigned wvs) = ⊥-elim (false≢true (trans (sym xxs) (verified wvs)))
 ...| sigVerified wvs' = refl

 failedSigCheckOutcome : {C : Set} ⦃ ws : WithSig C ⦄ (pk : PK) (c : C)
                       → sigCheckOutcomeFor pk c ≢ sigVerified
                       → SigCheckFailed
 failedSigCheckOutcome pk c prf with sigCheckOutcomeFor pk c
 ...| notSigned   = notSigned
 ...| checkFailed = checkFailed
 ...| sigVerified = ⊥-elim (prf refl)

ext: agda

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

module Dodo.Binary.Identity where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; subst; sym)
open import Level using (Level; _⊔_)
open import Function.Base using (flip)
open import Data.Product using (_×_; _,_; ∃; ∃-syntax; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel)
open import Relation.Binary using (Symmetric; Transitive; IsStrictTotalOrder)
-- Local imports
open import Dodo.Binary.Equality
open import Dodo.Binary.Composition
open import Dodo.Binary.Intersection
open import Dodo.Binary.Union
open import Dodo.Unary.Equality
open import Dodo.Unary.Intersection
open import Dodo.Unary.Union

-- # Definitions

-- | Identity relation over some set
--
-- Iff `P x` holds then `⦗ P ⦘ x x` holds.
⦗_⦘ : ∀ {a ℓ : Level} {A : Set a}
  → Pred A ℓ
    -------------
  → Rel A (a ⊔ ℓ)
⦗ p ⦘ x y = x ≡ y × p x

-- # Properties

module _ {a ℓ : Level} {A : Set a} {p : Pred A ℓ} where

  ⦗⦘-sym : Symmetric ⦗ p ⦘
  ⦗⦘-sym (refl , px) = (refl , px)

  ⦗⦘-trans : Transitive ⦗ p ⦘
  ⦗⦘-trans (refl , pi) (refl , _) = (refl , pi)

  ⦗⦘-flip : ⦗ p ⦘ ⇔₂ flip ⦗ p ⦘
  ⦗⦘-flip = ⇔: (λ{_ _ → ⦗⦘-sym}) (λ{_ _ → ⦗⦘-sym})

-- # Operations

module _ {a ℓ : Level} {A : Set a} {p : Pred A ℓ} where

  ⦗⦘-combine-⨾ : ⦗ p ⦘ ⨾ ⦗ p ⦘ ⇔₂ ⦗ p ⦘
  ⦗⦘-combine-⨾ = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : ⦗ p ⦘ ⨾ ⦗ p ⦘ ⊆₂' ⦗ p ⦘
    ⊆-proof _ _ ((refl , Px) ⨾[ x ]⨾ (refl , _)) = (refl , Px)
    ⊇-proof : ⦗ p ⦘ ⊆₂' ⦗ p ⦘ ⨾ ⦗ p ⦘
    ⊇-proof x _ (refl , Px) = (refl , Px) ⨾[ _ ]⨾ (refl , Px)

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {p : Pred A ℓ₁} {q : Pred A ℓ₂} where

  ⦗⦘-lift-⊆₂ : p ⊆₁ q → ⦗ p ⦘ ⊆₂ ⦗ q ⦘
  ⦗⦘-lift-⊆₂ (⊆: p⊆q) = ⊆: lemma
    where
    lemma : ⦗ p ⦘ ⊆₂' ⦗ q ⦘
    lemma x .x (refl , px) = (refl , p⊆q x px)

  ⦗⦘-unlift-⊆₂ : ⦗ p ⦘ ⊆₂ ⦗ q ⦘ → p ⊆₁ q
  ⦗⦘-unlift-⊆₂ (⊆: ⦗p⦘⊆⦗q⦘) = ⊆: lemma
    where
    lemma : p ⊆₁' q
    lemma x px = proj₂ (⦗p⦘⊆⦗q⦘ x x (refl , px))

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {p : Pred A ℓ₁} {q : Pred A ℓ₂} where

  ⦗⦘-lift : p ⇔₁ q → ⦗ p ⦘ ⇔₂ ⦗ q ⦘
  ⦗⦘-lift = ⇔₂-compose-⇔₁ ⦗⦘-lift-⊆₂ ⦗⦘-lift-⊆₂

  ⦗⦘-unlift : ⦗ p ⦘ ⇔₂ ⦗ q ⦘ → p ⇔₁ q
  ⦗⦘-unlift = ⇔₁-compose-⇔₂ ⦗⦘-unlift-⊆₂ ⦗⦘-unlift-⊆₂

  ⦗⦘-dist-∪ : ⦗ p ∪₁ q ⦘ ⇔₂ ⦗ p ⦘ ∪₂ ⦗ q ⦘
  ⦗⦘-dist-∪ = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : ⦗ p ∪₁ q ⦘ ⊆₂' ⦗ p ⦘ ∪₂ ⦗ q ⦘
    ⊆-proof _ _ (refl , inj₁ px) = inj₁ (refl , px)
    ⊆-proof _ _ (refl , inj₂ qx) = inj₂ (refl , qx)
    ⊇-proof : ⦗ p ⦘ ∪₂ ⦗ q ⦘ ⊆₂' ⦗ p ∪₁ q ⦘
    ⊇-proof _ _ (inj₁ (refl , px)) = (refl , inj₁ px)
    ⊇-proof _ _ (inj₂ (refl , qx)) = (refl , inj₂ qx)

  ⦗⦘-dist-∩ : ⦗ p ∩₁ q ⦘ ⇔₂ ⦗ p ⦘ ∩₂ ⦗ q ⦘
  ⦗⦘-dist-∩ = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : ⦗ p ∩₁ q ⦘ ⊆₂' ⦗ p ⦘ ∩₂ ⦗ q ⦘
    ⊆-proof x .x (refl , Px , Qx) = (refl , Px) , (refl , Qx)

    ⊇-proof : ⦗ p ⦘ ∩₂ ⦗ q ⦘ ⊆₂' ⦗ p ∩₁ q ⦘
    ⊇-proof x .x ((refl , Px) , (_ , Qx)) = refl , (Px , Qx)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
primitive
  primLevelZero : _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Text.Printf where

open import Prelude hiding (parseNat)
open import Builtin.Float

private
  data Padding : Set where
    noPad     : Padding
    lPad rPad : Nat → Padding

  record Flags : Set where
    field
      padding   : Padding
      padChar   : Char
      alternate : Bool
      precision : Maybe Nat

  defaultFlags : Flags
  Flags.padding   defaultFlags = noPad
  Flags.padChar   defaultFlags = ' '
  Flags.alternate defaultFlags = false
  Flags.precision defaultFlags = nothing

  data Format : Set where
    natArg    : Flags → Format
    strArg    : Flags → Format
    ustrArg   : Flags → Format
    floatArg  : Flags → Format
    charArg   : Format
    hexArg    : Bool → Flags → Format
    litString : String → Format
    badFormat : String → Format

data BadFormat (s : String) : Set where

private
  BadFormat′ : String → Set
  BadFormat′ "" = ⊥
  BadFormat′ s = BadFormat s

private
  consLit : String → List Format → List Format
  consLit s (litString s′ ∷ fmt) = litString (s & s′) ∷ fmt
  consLit s fmt = litString s ∷ fmt

private
  parseFormat : List Char → List Format
  parseFormatWithFlags : Flags → List Char → List Format

  parseNat′ : (Nat → Flags) → Nat → List Char → List Format
  parseNat′ flags n [] = parseFormatWithFlags (flags n) []
  parseNat′ flags n (c ∷ s) =
    if isDigit c then parseNat′ flags (n * 10 + charToNat c - charToNat '0') s
                 else parseFormatWithFlags (flags n) (c ∷ s)

  parseNat : (Nat → Flags) → List Char → List Format
  parseNat p s = parseNat′ p 0 s

  parsePadding : Flags → List Char → List Format
  parsePadding f [] = parseFormatWithFlags f []
  parsePadding f ('-' ∷ c ∷ s) =
    if isDigit c then parseNat (λ n → record f { padding = rPad n }) (c ∷ s)
                 else badFormat (packString ('-' ∷ c ∷ [])) ∷ parseFormat s
  parsePadding f ('0' ∷ s) = parsePadding (record f { padChar = '0' }) s
  parsePadding f ('.' ∷ c ∷ s) =
    if isDigit c then parseNat (λ n → record f { precision = just n }) (c ∷ s)
                 else badFormat (packString ('.' ∷ c ∷ [])) ∷ parseFormat s
  parsePadding f (c ∷ s) =
    if isDigit c then parseNat (λ n → record f { padding = lPad n }) (c ∷ s)
                 else parseFormatWithFlags f (c ∷ s)

  parseFlags : Flags → List Char → List Format
  parseFlags f ('#' ∷ s) = parseFlags (record f { alternate = true }) s
  parseFlags f s = parsePadding f s

  parseFormatWithFlags f [] = badFormat "" ∷ []
  parseFormatWithFlags f ('d' ∷ s) = natArg f ∷ parseFormat s
  parseFormatWithFlags f ('x' ∷ s) = hexArg false f ∷ parseFormat s
  parseFormatWithFlags f ('X' ∷ s) = hexArg true  f ∷ parseFormat s
  parseFormatWithFlags f ('c' ∷ s) = charArg ∷ parseFormat s
  parseFormatWithFlags f ('s' ∷ s) = strArg f ∷ parseFormat s
  parseFormatWithFlags f ('S' ∷ s) = ustrArg f ∷ parseFormat s
  parseFormatWithFlags f ('f' ∷ s) = floatArg f ∷ parseFormat s
  parseFormatWithFlags f ('%' ∷ s) = consLit "%" $ parseFormat s
  parseFormatWithFlags f ( c  ∷ s) = badFormat (packString ('%' ∷ c ∷ [])) ∷ parseFormat s

  parseFormat [] = []
  parseFormat ('%' ∷ fmt) = parseFlags defaultFlags fmt
  parseFormat (c   ∷ fmt) = consLit (packString [ c ]) $ parseFormat fmt

private
  pad : (String → String → String) → Char → Nat → String → String
  pad _+_ c n s =
    case n - length (unpackString s) of
    λ { 0 → s ; d → packString (replicate d c) + s}

  padLeft padRight : Char → Nat → String → String
  padLeft  = pad _&_
  padRight = pad (flip _&_)

  hexDigit : Char → Nat → String
  hexDigit a n = if n <? 10 then packString [ natToChar (n + charToNat '0') ]
                            else packString [ natToChar (n - 10 + charToNat a) ]

  {-# TERMINATING #-}
  showHex′ : Char → Nat → String
  showHex′ _ 0 = ""
  showHex′ a n = showHex′ a (n div 16) & hexDigit a (n mod 16)

  add0x : Flags → String → String
  add0x flags s = if Flags.alternate flags then "0x" & s else s

  pad0 : Flags → String → String
  pad0 flags s =
    let c = Flags.padChar flags in
    ifYes c == ' ' then s else
    case Flags.padding flags of
    λ { noPad → s ; (lPad n) → padLeft c (n - 2) s ; (rPad _) → s }

  showHex : Flags → Bool → Nat → String
  showHex f _ 0 = add0x f $ pad0 f $ "0"
  showHex f u n = add0x f $ pad0 f $ showHex′ (if u then 'A' else 'a') n

  showFrac : Nat → Float → String
  showFrac 0       _ = ""
  showFrac 1       x = show (round (10 * x))
  showFrac (suc p) x = show n & showFrac p (x′ - intToFloat n)
    where x′ = 10 * x
          n  = floor x′

  showPosFloat : Flags → Float → String
  showPosFloat f x =
    case Flags.precision f of λ
    { nothing  → show x
    ; (just 0) → show (floor x)
    ; (just p) → show (floor x) & "." & showFrac p (x - intToFloat (floor x))
    }

  showFloat : Flags → Float → String
  showFloat f x with x <? 0.0
  ... | true = "-" & showPosFloat f (negate x)
  ... | false = showPosFloat f x

  withPad : Flags → String → ShowS
  withPad flags s =
    let c = Flags.padChar flags in
    case Flags.padding flags of
    λ { noPad → showString s
      ; (lPad n) → showString (padLeft  c n s)
      ; (rPad n) → showString (padRight c n s)
      }

private
  Printf′ : List Format → Set
  Printf′ []                  = String
  Printf′ (natArg _    ∷ fmt) = Nat → Printf′ fmt
  Printf′ (hexArg _ _  ∷ fmt) = Nat → Printf′ fmt
  Printf′ (strArg _    ∷ fmt) = String → Printf′ fmt
  Printf′ (ustrArg _   ∷ fmt) = List Char → Printf′ fmt
  Printf′ (charArg     ∷ fmt) = Char → Printf′ fmt
  Printf′ (floatArg _  ∷ fmt) = Float → Printf′ fmt
  Printf′ (litString _ ∷ fmt) = Printf′ fmt
  Printf′ (badFormat e ∷ fmt) = BadFormat′ e → Printf′ fmt

  printf′ : (fmt : List Format) → ShowS → Printf′ fmt
  printf′ [] acc = acc ""
  printf′ (natArg p    ∷ fmt) acc n = printf′ fmt (acc ∘ withPad p (show n))
  printf′ (hexArg u p  ∷ fmt) acc n = printf′ fmt (acc ∘ withPad p (showHex p u n))
  printf′ (strArg p    ∷ fmt) acc s = printf′ fmt (acc ∘ withPad p s)
  printf′ (ustrArg p   ∷ fmt) acc s = printf′ fmt (acc ∘ withPad p (packString s))
  printf′ (floatArg p  ∷ fmt) acc x = printf′ fmt (acc ∘ withPad p (showFloat p x))
  printf′ (charArg     ∷ fmt) acc c = printf′ fmt (acc ∘ showString (packString [ c ]))
  printf′ (litString s ∷ fmt) acc   = printf′ fmt (acc ∘ showString s)
  printf′ (badFormat _ ∷ fmt) acc _ = printf′ fmt acc

Printf : String → Set
Printf = Printf′ ∘ parseFormat ∘ unpackString

printf : (fmt : String) → Printf fmt
printf fmt = printf′ (parseFormat $ unpackString fmt) id

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
------------------------------------------------------------------------------
-- Arithmetic properties (using induction on the FOTC natural numbers type)
------------------------------------------------------------------------------

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

-- Usually our proofs use pattern matching instead of the induction
-- principle associated with the FOTC natural numbers. The following
-- examples show some proofs using it.

module FOTC.Data.Nat.PropertiesByInductionI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- Congruence properties

+-leftCong : ∀ {a b c} → a ≡ b → a + c ≡ b + c
+-leftCong refl = refl

+-rightCong : ∀ {a b c} → b ≡ c → a + b ≡ a + c
+-rightCong refl = refl

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

N→0∨S : ∀ {n} → N n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n')
N→0∨S = N-ind A A0 is
  where
  A : D → Set
  A i = i ≡ zero ∨ (∃[ i' ] i ≡ succ₁ i' ∧ N i')

  A0 : A zero
  A0 = inj₁ refl

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = case prf₁ prf₂ Ai
    where
    prf₁ : i ≡ zero → succ₁ i ≡ zero ∨ (∃[ i' ] succ₁ i ≡ succ₁ i' ∧ N i')
    prf₁ h' = inj₂ (i , refl , (subst N (sym h') nzero))

    prf₂ : ∃[ i' ] i ≡ succ₁ i' ∧ N i' →
           succ₁ i ≡ zero ∨ (∃[ i' ] succ₁ i ≡ succ₁ i' ∧ N i')
    prf₂ (i' , prf , Ni') = inj₂ (i , refl , subst N (sym prf) (nsucc Ni'))

Sx≢x : ∀ {n} → N n → succ₁ n ≢ n
Sx≢x = N-ind A A0 is
  where
  A : D → Set
  A i = succ₁ i ≢ i

  A0 : A zero
  A0 = S≢0

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = →-trans succInjective Ai

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity n = +-0x n

+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity = N-ind A A0 is
  where
  A : D → Set
  A i = i + zero ≡ i

  A0 : A zero
  A0 = +-leftIdentity zero

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = trans (+-Sx i zero) (succCong Ai)

pred-N : ∀ {n} → N n → N (pred₁ n)
pred-N {n} Nn = case h₁ h₂ (N→0∨S Nn)
  where
  h₁ : n ≡ zero → N (pred₁ n)
  h₁ n≡0 = subst N (sym (trans (predCong n≡0) pred-0)) nzero

  h₂ : ∃[ n' ] n ≡ succ₁ n' ∧ N n' → N (pred₁ n)
  h₂ (n' , prf , Nn') = subst N (sym (trans (predCong prf) (pred-S n'))) Nn'

+-N : ∀ {m n} → N m → N n → N (m + n)
+-N {n = n} Nm Nn = N-ind A A0 is Nm
  where
  A : D → Set
  A i = N (i + n)

  A0 : A zero
  A0 = subst N (sym (+-leftIdentity n)) Nn

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = subst N (sym (+-Sx i n)) (nsucc Ai)

∸-N : ∀ {m n} → N m → N n → N (m ∸ n)
∸-N {m} Nm Nn = N-ind A A0 is Nn
  where
  A : D → Set
  A i = N (m ∸ i)

  A0 : A zero
  A0 = subst N (sym (∸-x0 m)) Nm

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = subst N (sym (∸-xS m i)) (pred-N Ai)

+-assoc : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
+-assoc Nm n o = N-ind A A0 is Nm
  where
  A : D → Set
  A i = i + n + o ≡ i + (n + o)

  A0 : A zero
  A0 = zero + n + o   ≡⟨ +-leftCong (+-leftIdentity n) ⟩
       n + o          ≡⟨ sym (+-leftIdentity (n + o)) ⟩
       zero + (n + o) ∎

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = succ₁ i + n + o     ≡⟨ +-leftCong (+-Sx i n) ⟩
              succ₁ (i + n) + o   ≡⟨ +-Sx (i + n) o ⟩
              succ₁ (i + n + o)   ≡⟨ succCong Ai ⟩
              succ₁ (i + (n + o)) ≡⟨ sym (+-Sx i (n + o)) ⟩
              succ₁ i + (n + o)   ∎

x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y] Nm n = N-ind A A0 is Nm
  where
  A : D → Set
  A i = i + succ₁ n ≡ succ₁ (i + n)

  A0 : A zero
  A0 = zero + succ₁ n   ≡⟨ +-leftIdentity (succ₁ n) ⟩
       succ₁ n          ≡⟨ succCong (sym (+-leftIdentity n)) ⟩
       succ₁ (zero + n) ∎

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = succ₁ i + succ₁ n     ≡⟨ +-Sx i (succ₁ n) ⟩
              succ₁ (i + succ₁ n)   ≡⟨ succCong Ai ⟩
              succ₁ (succ₁ (i + n)) ≡⟨ succCong (sym (+-Sx i n)) ⟩
              succ₁ (succ₁ i + n)   ∎

+-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
+-comm {n = n} Nm Nn = N-ind A A0 is Nm
  where
  A : D → Set
  A i = i + n ≡ n + i

  A0 : A zero
  A0 = zero + n ≡⟨ +-leftIdentity n ⟩
       n        ≡⟨ sym (+-rightIdentity Nn) ⟩
       n + zero ∎

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = succ₁ i + n   ≡⟨ +-Sx i n ⟩
              succ₁ (i + n) ≡⟨ succCong Ai ⟩
              succ₁ (n + i) ≡⟨ sym (x+Sy≡S[x+y] Nn i) ⟩
              n + succ₁ i   ∎

0∸x : ∀ {n} → N n → zero ∸ n ≡ zero
0∸x = N-ind A A0 is
  where
  A : D → Set
  A i = zero ∸ i ≡ zero

  A0 : A zero
  A0 = ∸-x0 zero

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = zero ∸ succ₁ i   ≡⟨ ∸-xS zero i ⟩
              pred₁ (zero ∸ i) ≡⟨ predCong Ai ⟩
              pred₁ zero       ≡⟨ pred-0 ⟩
              zero ∎

S∸S : ∀ {m n} → N m → N n → succ₁ m ∸ succ₁ n ≡ m ∸ n
S∸S {m} Nm = N-ind A A0 is
  where
  A : D → Set
  A i = succ₁ m ∸ succ₁ i ≡ m ∸ i

  A0 : A zero
  A0 = succ₁ m ∸ succ₁ zero   ≡⟨ ∸-xS (succ₁ m) zero ⟩
       pred₁ (succ₁ m ∸ zero) ≡⟨ predCong (∸-x0 (succ₁ m)) ⟩
       pred₁ (succ₁ m)        ≡⟨ pred-S m ⟩
       m                      ≡⟨ sym (∸-x0 m) ⟩
       m ∸ zero               ∎

  is : ∀ {i} → A i → A (succ₁ i)
  is {i} Ai = succ₁ m ∸ succ₁ (succ₁ i) ≡⟨ ∸-xS (succ₁ m) (succ₁ i) ⟩
              pred₁ (succ₁ m ∸ succ₁ i) ≡⟨ predCong Ai ⟩
              pred₁ (m ∸ i)             ≡⟨ sym (∸-xS m i) ⟩
              m ∸ succ₁ i               ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{- This file exports the primitives of cubical Id types -}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Core.Id where

open import Cubical.Core.Primitives hiding ( _≡_ )

open import Agda.Builtin.Cubical.Id public
  renaming ( conid to ⟨_,_⟩
           -- TODO: should the user really be able to access these two?
           ; primIdFace to faceId  -- ∀ {ℓ} {A : Type ℓ} {x y : A} → Id x y → I
           ; primIdPath to pathId  -- ∀ {ℓ} {A : Type ℓ} {x y : A} → Id x y → Path A x y

           ; primIdElim to elimId  -- ∀ {ℓ ℓ'} {A : Type ℓ} {x : A}
                                   -- (P : ∀ (y : A) → x ≡ y → Type ℓ')
                                   -- (h : ∀ (φ : I) (y : A [ φ ↦ (λ _ → x) ])
                                   --        (w : (Path _ x (outS y)) [ φ ↦ (λ { (φ = i1) → λ _ → x}) ] ) →
                                   --        P (outS y) ⟨ φ , outS w ⟩) →
                                   -- {y : A} (w' : x ≡ y) → P y w'
           )
  hiding ( primIdJ ) -- this should not be used as it is using compCCHM

{- BUILTIN ID Id -}
_≡_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ
_≡_ = Id

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:
open import Prelude
open import dynamics-core

module grounding where
  grounding : ∀{τ1 τ2} →
              τ1 ▸gnd τ2 →
              ((τ2 ground) × (τ1 ~ τ2) × (τ1 ≠ τ2))
  grounding (MGArr x) = GArrHole , TCArr TCHole1 TCHole1 , x
  grounding (MGSum x) = GSumHole , TCSum TCHole1 TCHole1 , x
  grounding (MGProd x) = GProdHole , TCProd TCHole1 TCHole1 , x

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Selective.EnvironmentOperations where
open import Selective.ActorMonad
open import Selective.SimulationEnvironment
open import Prelude

open import Data.List.All.Properties using (++⁺ ; drop⁺)
open import Data.List.Properties using (map-++-commute)
open import Data.Nat.Properties using (≤-reflexive)
open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax)

open Actor
open ValidActor
open Env
open NamedInbox
open NameSupplyStream

-- We can create a new Actor from an ActorM if we know its name.
-- This is used when spawning an actor.
new-actor : ∀ {IS A post} → ActorM ∞ IS A [] post → Name → Actor
new-actor {IS} {A} {post} m name = record
                                        { inbox-shape = IS
                                        ; A = A
                                        ; references = []
                                        ; pre = []
                                        ; pre-eq-refs = refl
                                        ; post = post
                                        ; computation = m ⟶ []
                                        ; name = name
                                        }

-- An actor can be lifted to run sub-programs that need less references
lift-actor : (actor : Actor) → {pre : TypingContext} →
             (references : Store) →
             (pre-eq-refs : (map shape references) ≡ pre) →
             ActorState ∞ (inbox-shape actor) (A actor) pre (post actor) →
             Actor
lift-actor actor {pre} references pre-eq-refs m = record
                                              { inbox-shape = inbox-shape actor
                                              ; A = actor .A
                                              ; references = references
                                              ; pre = pre
                                              ; pre-eq-refs = pre-eq-refs
                                              ; post = actor .post
                                              ; computation = m
                                              ; name = actor .name
                                              }

-- Replace the monadic part of an actor
-- Many of the bind-operations don't change anything except what the next step should be.
replace-actorM : (actor : Actor) → ActorState ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor
replace-actorM actor m = record
                           { inbox-shape = inbox-shape actor
                           ; A = A actor
                           ; references = references actor
                           ; pre = pre actor
                           ; pre-eq-refs = pre-eq-refs actor
                           ; post = post actor
                           ; computation = m
                           ; name = name actor
                           }

-- Add one reference to an actor.
-- Used when receiving a reference, spawn, or self.
-- The precondition and references are equal via the congruence relation on consing the shape of the reference.
add-reference : (actor : Actor) → (nm : NamedInbox) → ActorState ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor
add-reference actor nm m = record
                             { inbox-shape = inbox-shape actor
                             ; A = A actor
                             ; references = nm ∷ references actor
                             ; pre = shape nm ∷ pre actor
                             ; pre-eq-refs = cong (_∷_ (shape nm)) (pre-eq-refs actor)
                             ; post = post actor
                             ; computation = m
                             ; name = name actor
                             }

add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorState ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor
add-references-to-actor actor nms m = record
                                        { inbox-shape = inbox-shape actor
                                        ; A = A actor
                                        ; references = nms ++ references actor
                                        ; pre = map shape nms ++ pre actor
                                        ; pre-eq-refs = trans (map-++-commute shape nms (references actor)) (cong (_++_ (map shape nms)) (pre-eq-refs actor))
                                        ; post = post actor
                                        ; computation = m
                                        ; name = name actor
                                        }
add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} →
  map shape nms ++ pre actor ≡ add-references (pre actor) x →
  ActorState ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) →
  Actor
add-references-rewrite actor nms {x} p m = record
                             { inbox-shape = inbox-shape actor
                             ; A = A actor
                             ; references = nms ++ references actor
                             ; pre = add-references (pre actor) x
                             ; pre-eq-refs = trans (trans (map-++-commute shape nms (references actor)) (cong (_++_ (map shape nms)) (pre-eq-refs actor))) p
                             ; post = post actor
                             ; computation = m
                             ; name = name actor
                             }

data SameValidityProof : Actor → Actor → Set₁ where
  AreSame :
    ∀ {A A' pre pre' post post'}
    {IS name references}
    {per per'}
    {computation computation'} →
    SameValidityProof
    (record
    { inbox-shape = IS
    ; A = A
    ; references = references
    ; pre = pre
    ; pre-eq-refs = per
    ; post = post
    ; computation = computation
    ; name = name
    })
    (record
    { inbox-shape = IS
    ; A = A'
    ; references = references
    ; pre = pre'
    ; pre-eq-refs = per'
    ; post = post'
    ; computation = computation'
    ; name = name
    })

-- A proof of an actor being valid is also valid for another actor if
-- * they have the same name
-- * they have the same references
-- * they have the same inbox type
rewrap-valid-actor : {store : Store} → {actorPre : Actor} → {actorPost : Actor} →
                     SameValidityProof actorPre actorPost →
                     ValidActor store actorPre →
                     ValidActor store actorPost
rewrap-valid-actor AreSame va = record { actor-has-inbox = va .actor-has-inbox ; references-have-pointer = va .references-have-pointer }

data ReferenceAdded (ref : NamedInbox) : Actor → Actor → Set₁ where
  RefAdded :
    ∀ {A A' pre pre' post post'}
    {IS name references}
    {per per'}
    {computation computation'} →
    ReferenceAdded ref
    (record
    { inbox-shape = IS
    ; A = A
    ; references = references
    ; pre = pre
    ; pre-eq-refs = per
    ; post = post
    ; computation = computation
    ; name = name
    })
    (record
    { inbox-shape = IS
    ; A = A'
    ; references = ref ∷ references
    ; pre = pre'
    ; pre-eq-refs = per'
    ; post = post'
    ; computation = computation'
    ; name = name
    })

add-reference-valid : {store : Store} → {actorPre : Actor} → {actorPost : Actor} →
                    {ref : NamedInbox} →
                    ReferenceAdded ref actorPre actorPost →
                    ValidActor store actorPre →
                    reference-has-pointer store ref →
                    ValidActor store actorPost
add-reference-valid RefAdded va p = record { actor-has-inbox = va .actor-has-inbox ; references-have-pointer = p ∷ (va .references-have-pointer) }

record ValidMessageList (store : Store) (S : InboxShape) : Set₁ where
  field
    inbox : Inbox S
    valid : All (message-valid store) inbox

InboxUpdater : (store : Store) (IS : InboxShape) → Set₁
InboxUpdater store IS = ValidMessageList store IS → ValidMessageList store IS

record UpdatedInbox (store : Store) {store' : Store} (original : Inboxes store') (name : Name) : Set₂ where
  field
    updated-inboxes : Inboxes store'
    inboxes-valid : InboxesValid store updated-inboxes
    others-unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' original p' → InboxForPointer inb store' updated-inboxes p'

open ValidMessageList
open UpdatedInbox
open NameSupply

-- Update one of the inboxes in a list of inboxes.
-- All the inboxes have been proven to be valid in the context of a store,
-- and the goal is to return a new list of inboxes which are also valid for the same store.
-- We know what inbox to update via an index using the inbox name into the list.
-- The update function receives both a list of messages from the inbox we pointed out,
-- and a proof that all the messages are valid for the store.
-- The update function returns a new list of the same type,
-- and has to provide a proof that this list is also valid for the store
update-inbox : {name : Name} → {IS : InboxShape} →
  (store : Store) →
  {store' : Store} →
  (inboxes : Inboxes store') →
  (InboxesValid store inboxes) →
  (name ↦ IS ∈ store') →
  (f : InboxUpdater store IS) →
  UpdatedInbox store inboxes name
update-inbox _ _ [] () _
update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) zero f =
  record { updated-inboxes = inbox updated ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs ; others-unaffected = unaffected }
  where
    updated = (f (record { inbox = x ; valid = px }))
    unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (inbox updated ∷ inboxes) p'
    unaffected pr zero = ⊥-elim (pr refl)
    unaffected pr (suc ifp) = suc ifp
update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) (suc p) f =
  record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ inboxes-valid updated ; others-unaffected = unaffected }
  where
    updated = (update-inbox store inboxes proofs p f)
    unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (x ∷ updated-inboxes updated) p'
    unaffected pr  zero = zero
    unaffected pr (suc ifp) = suc (others-unaffected updated pr ifp)

-- Move the actor that is at the top of the list, to the back of the list
-- This is done to create a round-robin system for the actors, since run-env always picks the actor at the top
-- Uses the insight that the order of the inboxes soes not correspond to the order of the Actors,
-- and that moving an actor to the back doesn't change any of the proofs about actors being valid.
top-actor-to-back : Env → Env
top-actor-to-back env with (acts env) | (actors-valid env)
top-actor-to-back env | [] | _ = env
top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record
                             { acts = acts ++ [ x ]ˡ
                             ; blocked = blocked env
                             ; env-inboxes = env-inboxes env
                             ; store = store env
                             ; actors-valid = ++⁺ prfs [ y ]ᵃ
                             ; blocked-valid = blocked-valid env
                             ; messages-valid = messages-valid env
                             ; name-supply = name-supply env
                             ; blocked-no-progress = blocked-no-progress env
                             }

-- An actor is still valid if we add a new inbox to the store, as long as that name is not used in the store before
valid-actor-suc : ∀ {store actor IS} → (ns : NameSupply store) → ValidActor store actor → ValidActor (inbox# ns .name [ IS ] ∷ store) actor
valid-actor-suc ns va =
  let open ValidActor
      open _comp↦_∈_
  in record {
    actor-has-inbox = suc {pr = ns .name-is-fresh (actor-has-inbox va)} (actor-has-inbox va)
    ; references-have-pointer = ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) (references-have-pointer va)
    }

valid-references-suc : ∀ {store references IS} →
                     (ns : NameSupply store) →
                     All (reference-has-pointer store) references →
                     All (reference-has-pointer (inbox# (ns .name) [ IS ] ∷ store)) references
valid-references-suc ns pointers =
  let open _comp↦_∈_
  in ∀map (λ p → suc-p (ns .name-is-fresh (actual-has-pointer p)) p) pointers

-- All the messages in an inbox are still valid if we add a new inbox to the store, as long as that name is not used in the store before
messages-valid-suc : ∀ {store IS x} {inb : Inbox IS} → (ns : NameSupply store) → all-messages-valid store inb → all-messages-valid (inbox# ns .name [ x ] ∷ store) inb
messages-valid-suc {store} {IS} {x} ns [] = []
messages-valid-suc {store} {IS} {x} {nx ∷ _} ns (px ∷ vi) = message-valid-suc nx px ∷ (messages-valid-suc ns vi)
  where
    open _comp↦_∈_
    fields-valid-suc : ∀ {MT} {fields : All named-field-content MT} →
      FieldsHavePointer store fields →
      FieldsHavePointer (inbox# ns .name [ x ] ∷ store) fields
    fields-valid-suc [] = []
    fields-valid-suc (FhpV ∷ valid) = FhpV ∷ fields-valid-suc valid
    fields-valid-suc (FhpR x ∷ valid) = FhpR (suc-p (ns .name-is-fresh (actual-has-pointer x)) x) ∷ (fields-valid-suc valid)
    message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# ns .name [ x ] ∷ store) nx
    message-valid-suc (NamedM x₁ x₂) px = fields-valid-suc px

is-blocked-suc : ∀ {store actor IS} {inbs : Inboxes store} {inb : Inbox IS} → (ns : NameSupply store) → IsBlocked store inbs actor → IsBlocked (inbox# ns .name [ IS ] ∷ store) (inb ∷ inbs) actor
is-blocked-suc ns (BlockedReturn at-return no-cont) = BlockedReturn at-return no-cont
is-blocked-suc ns (BlockedReceive at-receive p inbox-for-pointer) = BlockedReceive at-receive (suc {pr = ns .name-is-fresh p} p) (suc inbox-for-pointer)
is-blocked-suc ns (BlockedSelective at-selective p inb inbox-for-pointer filter-empty) = BlockedSelective at-selective (suc {pr = ns .name-is-fresh p} p) inb (suc inbox-for-pointer) filter-empty

-- Add a new actor to the environment.
-- The actor is added to the top of the list of actors.
add-top : ∀ {IS A post} → ActorState ∞ IS A [] post → Env → Env
add-top {IS} {A} {post} m env = record
                 { acts = record
                        { inbox-shape = IS
                        ; A = A
                        ; references = []
                        ; pre = []
                        ; pre-eq-refs = refl
                        ; post = post
                        ; computation = m
                        ; name = env .name-supply .supply .name
                        } ∷ acts env
                   ; blocked = blocked env
                   ; env-inboxes = [] ∷ env-inboxes env
                   ; store = inbox# env .name-supply .supply .name [ IS ] ∷ store env
                   ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (env .name-supply .supply)) (actors-valid env)
                   ; blocked-valid = ∀map (valid-actor-suc (env .name-supply .supply)) (blocked-valid env)
                   ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (env .name-supply .supply)
                   ; name-supply = env .name-supply .next IS
                   ; blocked-no-progress = ∀map (is-blocked-suc (env .name-supply .supply)) (env .blocked-no-progress)
                   }
  where
    -- ad-hoc ∀map, because we are not using All here
    map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → (ns : NameSupply store) → InboxesValid (inbox# ns .name [ IS ] ∷ store) inbs
    map-suc store [] _ = []
    map-suc store (x ∷ valid) ns = messages-valid-suc ns x ∷ (map-suc store valid ns)

record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {name : Name} {S : InboxShape} (p : name ↦ S ∈ store') : Set₂ where
  field
    messages : Inbox S
    valid : all-messages-valid store messages
    right-inbox : InboxForPointer messages store' inboxes p

-- Get the messages of an inbox pointed to in the environment.
-- This is just a simple lookup into the list of inboxes.
get-inbox : ∀ {name IS} → (env : Env) → (p : name ↦ IS ∈ (store env)) → GetInbox (env .store) (env .env-inboxes) p
get-inbox env point = loop (env-inboxes env) (messages-valid env) point
  where
    loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → (p : name ↦ IS ∈ store') → GetInbox store inbs p
    loop _ [] ()
    loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px ; right-inbox = zero }
    loop (_ ∷ inbs) (_ ∷ inb-valid) (suc point) =
      let rec = loop inbs inb-valid point
          open GetInbox
      in record { messages = rec .messages ; valid = rec .valid ; right-inbox = suc (rec .right-inbox) }

open GetInbox

record UnblockedActors {store store' : Store} {original : Inboxes store'} {n : Name} (updated : UpdatedInbox store original n) : Set₂ where
  field
    unblocked : List Actor
    unblocked-updated : All (λ act → n ≡ name act) unblocked
    unblocked-valid : All (ValidActor store) unblocked
    still-blocked : List Actor
    blocked-no-prog : All (IsBlocked store' (updated-inboxes updated)) still-blocked
    blocked-valid : All (ValidActor store) still-blocked

open UnblockedActors

unblock-actors :
  {store : Store} →
  {original : Inboxes store} →
  {n : Name} →
  (updated : UpdatedInbox store original n) →
  (blocked : List Actor) →
  All (ValidActor store) blocked →
  All (IsBlocked store original) blocked →
  UnblockedActors updated
unblock-actors updated [] [] [] = record
                                            { unblocked = []
                                            ; unblocked-updated = []
                                            ; unblocked-valid = []
                                            ; still-blocked = []
                                            ; blocked-no-prog = []
                                            ; blocked-valid = []
                                            }
unblock-actors {store} {original} {n} updated (x ∷ blckd) (v ∷ blckd-valid) (ib ∷ is-blocked) with (n ≟ (name x))
... | yes p =
  let rec = unblock-actors updated blckd blckd-valid is-blocked
  in record
       { unblocked = x ∷ rec .unblocked
       ; unblocked-updated = p ∷ rec .unblocked-updated
       ; unblocked-valid = v ∷ rec .unblocked-valid
       ; still-blocked = rec .still-blocked
       ; blocked-no-prog = rec .blocked-no-prog
       ; blocked-valid = rec .blocked-valid
       }
... | no ¬p =
  let rec = unblock-actors updated blckd blckd-valid is-blocked
  in record
       { unblocked = rec .unblocked
       ; unblocked-updated = rec .unblocked-updated
       ; unblocked-valid = rec .unblocked-valid
       ; still-blocked = x ∷ rec .still-blocked
       ; blocked-no-prog = blocked-unaffected ib ∷ rec .blocked-no-prog
       ; blocked-valid = v ∷ rec .blocked-valid
       }
    where
      blocked-unaffected : IsBlocked store original x → IsBlocked store (updated-inboxes updated) x
      blocked-unaffected (BlockedReturn x y) = BlockedReturn x y
      blocked-unaffected (BlockedReceive x p y) = BlockedReceive x p (others-unaffected updated ¬p y)
      blocked-unaffected (BlockedSelective x p a b c) = BlockedSelective x p a (others-unaffected updated ¬p b) c

update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈ (store env) →
                 (f : ValidMessageList (store env) IS → ValidMessageList (store env) IS) → Env
update-inbox-env {name} {IS} env p f =
  let
    updated = update-inbox (store env) (env-inboxes env) (messages-valid env) p f
    unblock-split = unblock-actors updated (blocked env) (blocked-valid env) (blocked-no-progress env)
  in record {
    acts = (unblocked unblock-split) ++ acts env
    ; blocked = still-blocked unblock-split
    ; env-inboxes = updated-inboxes updated
    ; store = store env
    ; actors-valid = ++⁺ (unblock-split .unblocked-valid) (env .actors-valid)
    ; blocked-valid = unblock-split .blocked-valid
    ; messages-valid = inboxes-valid updated
    ; name-supply = env .name-supply
    ; blocked-no-progress = unblock-split .blocked-no-prog
    }

record FoundReference (store : Store) (S : InboxShape) : Set₂ where
  field
    name : Name
    reference : name comp↦ S ∈ store

lookup-reference : ∀ {store ToIS} → (pre : TypingContext) → (refs : List NamedInbox) → All (reference-has-pointer store) refs → map shape refs ≡ pre → ToIS ∈ pre → FoundReference store ToIS
lookup-reference [] refs prfs eq ()
lookup-reference (x ∷ pre₁) [] prfs () Z
lookup-reference (x ∷ pre₁) [] prfs () (S px)
lookup-reference _ (inbox# name [ shape ] ∷ refs) (reference ∷ prfs) refl Z = record { name = name ; reference = reference }
lookup-reference _ (_ ∷ refs) (_ ∷ prfs) refl (S px) = lookup-reference _ refs prfs refl px

-- looks up the pointer for one of the references known by an actor
lookup-reference-act : ∀ {store actor ToIS} → ValidActor store actor → ToIS ∈ (pre actor) → FoundReference store ToIS
lookup-reference-act {store} {actor} {ToIS} va ref = lookup-reference (pre actor) (Actor.references actor) (ValidActor.references-have-pointer va) (pre-eq-refs actor) ref

open _comp↦_∈_
open FoundReference

-- Extract the found pointer
underlying-pointer : ∀ {IS store} → (ref : FoundReference store IS) → (name ref ↦ actual (reference ref) ∈ store )
underlying-pointer ref = actual-has-pointer (reference ref)

translate-message-pointer : ∀ {ToIS A store} →
  (w : FoundReference store ToIS) →
  A ∈ ToIS →
  A ∈ (actual (reference w))
translate-message-pointer w x = translate-⊆ (actual-handles-wanted (reference w)) x

record LiftedReferences (lss gss : TypingContext) (references : List NamedInbox) : Set₂ where
  field
    subset-inbox : lss ⊆ gss
    contained : List NamedInbox
    subset : contained ⊆ references
    contained-eq-inboxes : map shape contained ≡ lss

open LiftedReferences

-- Convert a subset for preconditions to a subset for references
lift-references : ∀ {lss gss} → lss ⊆ gss → (references : List NamedInbox) → map shape references ≡ gss → LiftedReferences lss gss references
lift-references [] refs refl = record {
  subset-inbox = []
  ; contained = []
  ; subset = []
  ; contained-eq-inboxes = refl
  }
lift-references (_∷_ {y} {xs} x₁ subs) refs refl with (lift-references subs refs refl)
... | q  = record {
  subset-inbox = x₁ ∷ subs
  ; contained = contained-el ∷ contained q
  ; subset = (translate-∈ x₁ refs shape refl) ∷ (subset q)
  ; contained-eq-inboxes = combine contained-el-shape y (map shape (contained q)) xs (sym contained-el-ok) (contained-eq-inboxes q)
  }
  where
    contained-el : NamedInbox
    contained-el = lookup-parallel x₁ refs shape refl
    contained-el-shape = shape contained-el
    contained-el-ok : y ≡ contained-el-shape
    contained-el-ok = lookup-parallel-≡ x₁ refs shape refl
    combine : (a b : InboxShape) → (as bs : TypingContext) → (a ≡ b) → (as ≡ bs) → (a ∷ as ≡ b ∷ bs)
    combine a .a as .as refl refl = refl

data LiftActor : Actor → Actor → Set₂ where
  CanBeLifted :
    ∀ {A A' post post'}
    {IS name references}
    {lss gss}
    {per}
    {computation computation'} →
    (lr : LiftedReferences lss gss references) →
    LiftActor
    (record
    { inbox-shape = IS
    ; A = A
    ; references = references
    ; pre = gss
    ; pre-eq-refs = per
    ; post = post
    ; computation = computation
    ; name = name
    })
    (record
    { inbox-shape = IS
    ; A = A'
    ; references = lr .contained
    ; pre = lss
    ; pre-eq-refs = lr .contained-eq-inboxes
    ; post = post'
    ; computation = computation'
    ; name = name
    })

lift-valid-actor : ∀ {store} {act act' : Actor} →
                   LiftActor act act' →
                   ValidActor store act →
                   ValidActor store act'
lift-valid-actor (CanBeLifted lr) va =
  record {
    actor-has-inbox = va .actor-has-inbox
    ; references-have-pointer = All-⊆ (lr .subset) (va .references-have-pointer)
    }

-- We can replace the actors in an environment if they all are valid for the current store.
replace-actors : (env : Env) → (actors : List Actor) → All (ValidActor (store env)) actors → Env
replace-actors env actors actorsValid = record {
  acts = actors
  ; blocked = env .blocked
  ; env-inboxes = env .env-inboxes
  ; store = env .store
  ; actors-valid = actorsValid
  ; blocked-valid = env .blocked-valid
  ; messages-valid = env .messages-valid
  ; name-supply = env .name-supply
  ; blocked-no-progress = env .blocked-no-progress
  }

replace-focused : {act : Actor} → (env : Env) → Focus act env →
                  (act' : Actor) →
                  (valid' : ValidActor (env .store) act') →
                  Env
replace-focused env@record {
  acts = _ ∷ rest
  ; actors-valid = _ ∷ rest-valid
  } Focused act' valid' =
  replace-actors env (act' ∷ rest) (valid' ∷ rest-valid)

block-focused : {act : Actor} → (env : Env) → Focus act env → IsBlocked (env .store) (env .env-inboxes) act → Env
block-focused env@record {
  acts = actor ∷ rest
  ; blocked = blocked
  ; actors-valid = actor-valid ∷ rest-valid
  ; blocked-valid = blocked-valid
  } Focused blckd = record {
  acts = rest
  ; blocked = actor ∷ blocked
  ; store = env .store
  ; env-inboxes = env .env-inboxes
  ; name-supply = env .name-supply
  ; actors-valid = rest-valid
  ; blocked-valid = actor-valid ∷ blocked-valid
  ; messages-valid = env .messages-valid
  ; blocked-no-progress = blckd ∷ env .blocked-no-progress
  }

-- Takes a named message and a proof that the named message is valid for the store.
-- Values are valid for any store and references need a proof that the pointer is valid.
add-message : {S : InboxShape} → {store : Store} → (message : NamedMessage S) → message-valid store message → (ValidMessageList store S → ValidMessageList store S)
add-message message valid vml = record {
  inbox = inbox vml ++ [ message ]ˡ
  ; valid = ++⁺ (ValidMessageList.valid vml) [ valid ]ᵃ
  }

-- Removes the next message from an inbox.
-- This is a no-op if there are no messages in the inbox.
remove-message : {S : InboxShape} → {store : Store} → (ValidMessageList store S → ValidMessageList store S)
remove-message vml = record { inbox = drop 1 (inbox vml) ; valid = drop⁺ 1 (ValidMessageList.valid vml) }

name-fields : ∀ {MT store} → (pre : TypingContext) →
               (refs : List NamedInbox) →
               All (reference-has-pointer store) refs →
               All (send-field-content pre) MT →
               map shape refs ≡ pre →
               All named-field-content MT
name-fields pre refs rhp [] eq = []
name-fields _ refs rhp (_∷_ {ValueType x} (lift lower) sfc) refl = lower ∷ (name-fields _ refs rhp sfc refl)
name-fields {store = store} _ refs rhp (_∷_ {ReferenceType x} px sfc) refl = name (lookup-reference _ refs rhp refl (_⊢>:_.actual-is-sendable px)) ∷ (name-fields _ refs rhp sfc refl)

name-fields-act : ∀ {MT} store → ∀ actor →
              All (send-field-content (pre actor)) MT →
              ValidActor store actor → All named-field-content MT
name-fields-act store actor sfc valid = name-fields (pre actor) (Actor.references actor) (references-have-pointer valid) sfc (pre-eq-refs actor)

unname-field : ∀ {x} → named-field-content x → receive-field-content x
unname-field {ValueType x₁} nfc = nfc
unname-field {ReferenceType x₁} nfc = _

extract-inboxes : ∀ {MT} → All named-field-content MT → List NamedInbox
extract-inboxes [] = []
extract-inboxes (_∷_ {ValueType _} _ ps) = extract-inboxes ps
extract-inboxes (_∷_ {ReferenceType x} name ps) = inbox# name [ x ] ∷ extract-inboxes ps

named-inboxes : ∀ {S} → (nm : NamedMessage S) → List NamedInbox
named-inboxes (NamedM x x₁) = extract-inboxes x₁

reference-names : {MT : MessageType} → All named-field-content MT → List Name
reference-names [] = []
reference-names (_∷_ {ValueType x} px ps) = reference-names ps
reference-names (_∷_ {ReferenceType x} name ps) = name ∷ reference-names ps

++-diff : (a b c : List InboxShape) → a ≡ b → a ++ c ≡ b ++ c
++-diff [] .[] c refl = refl
++-diff (x ∷ a) .(x ∷ a) c refl = refl

add-fields++ : ∀ MT → (x₁ : All named-field-content MT) → map shape (extract-inboxes x₁) ≡ extract-references MT
add-fields++ [] [] = refl
add-fields++ (ValueType x ∷ MT) (px ∷ x₁) = add-fields++ MT x₁
add-fields++ (ReferenceType x ∷ MT) (px ∷ x₁) = cong (_∷_ x) (add-fields++ MT x₁)

add-references++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ w → map shape (named-inboxes nm) ++ w ≡ add-references w (unname-message nm)
add-references++ msg@(NamedM {MT} x x₁) p w = halp (add-fields++ MT x₁)
  where
    halp : map shape (extract-inboxes x₁) ≡ extract-references MT → map shape (extract-inboxes x₁) ++ w ≡ extract-references MT ++ w
    halp p = ++-diff (map shape (extract-inboxes x₁)) (extract-references MT) w p

valid++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ {w} →
        All (reference-has-pointer store) w →
        All (reference-has-pointer store) (named-inboxes nm ++ w)
valid++ (NamedM x x₁) v = valid-fields v
  where
    valid-fields : ∀ {MT store} →
                   {fields : All named-field-content MT} →
                   FieldsHavePointer store fields → ∀ {p} →
                   All (reference-has-pointer store) p →
                   All (reference-has-pointer store) (extract-inboxes fields ++ p)
    valid-fields [] ps = ps
    valid-fields (FhpV ∷ fhp) ps = valid-fields fhp ps
    valid-fields (FhpR px ∷ fhp) ps = px ∷ (valid-fields fhp ps)

open _⊢>:_

compatible-handles : ∀ store x refs
                     (px : (map shape refs) ⊢>: x)
                     (w : FoundReference store (actual px)) →
                     x ⊆ actual (reference w)
compatible-handles store x refs px w =
  let a = actual-handles-requested px
      b = actual-handles-wanted (reference w)
  in ⊆-trans a b

make-pointer-compatible : ∀ store x refs
                       (px : (map shape refs) ⊢>: x) →
                       (All (reference-has-pointer store) refs) →
                       (w : FoundReference store (actual px)) →
                       name w comp↦ x ∈ store
make-pointer-compatible store x refs px rhp w = [p: actual-has-pointer (reference w) ][handles: compatible-handles store x refs px w ]

open FieldsHavePointer

make-pointers-compatible : ∀ {MT} store pre refs (eq : map shape refs ≡ pre)
                           (fields : All (send-field-content pre) MT)
                           (rhp : All (reference-has-pointer store) refs) →
                         FieldsHavePointer store (name-fields pre refs rhp fields eq)
make-pointers-compatible store pre refs eq [] rhp = []
make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = FhpV ∷ make-pointers-compatible store _ refs refl fields rhp
make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp =
  let foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px)
  in FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (make-pointers-compatible store _ refs refl fields rhp)

-- Removes the next message from an inbox.
-- This is a no-op if there are no messages in the inbox.
remove-found-message : {S : InboxShape} → {store : Store} → (filter : MessageFilter S) → (ValidMessageList store S → ValidMessageList store S)
remove-found-message f record { inbox = [] ; valid = [] } = record { inbox = [] ; valid = [] }
remove-found-message {s} {store} f record { inbox = (x ∷ inbox₁) ; valid = vx ∷ valid₁ } with (f (unname-message x))
... | false =
  let vml = remove-found-message f (record { inbox = inbox₁ ; valid = valid₁ })
      open ValidMessageList
  in record { inbox = x ∷ vml .inbox ; valid = vx ∷ vml .valid }
... | true = record { inbox = inbox₁ ; valid = valid₁ }

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


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

module Harmony where

open import Data.Bool       using (Bool; true; false; if_then_else_; _∨_; not; _∧_)
open import Data.Fin        using (#_; toℕ) renaming (zero to fz; suc to fs)
open import Data.List       using (List; map; []; _∷_; concatMap; foldr; head; zip; null)
open import Data.Maybe      using (fromMaybe; is-nothing; Maybe; just; nothing)
open import Data.Nat        using (ℕ; suc; _∸_; _<ᵇ_)
open import Data.Nat.DivMod using (_mod_; _div_)
open import Data.Product    using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.Vec        using (Vec; toList; []; _∷_)
open import Function        using (_∘_)

open import BitVec          using (BitVec; empty; insert; elements; _∩_; _∈_)
open import Counterpoint
open import Diatonic        using (DiatonicDegree; thirdUp; _≡ᵈ_; degree→PC; major; pitch→DegreeCMajor)
open import Interval
open import Music
open import Note
open import Pitch           hiding (I)
open import Util            using (filter; concatMaybe)

-- either 0 or 1 pitch class
pointToPC : Point → List PC
pointToPC (tone p) = pitchToClass p ∷ []
pointToPC (hold p) = pitchToClass p ∷ []
pointToPC rest     = []

chordToPCes : {n : ℕ} → Chord n → List PC
chordToPCes (chord ps) = concatMap pointToPC (toList ps)

pitchClassListToSet : List PC → PCSet
pitchClassListToSet = foldr insert empty

pitchClassSetToList : PCSet → List PC
pitchClassSetToList ps = fn 0 (toList ps)
  where fn : ℕ → List Bool → List PC
        fn i []           = []
        fn i (false ∷ bs) = fn (suc i) bs
        fn i (true  ∷ bs) = i mod s12 ∷ fn (suc i) bs

-- Primary chords, assuming the tonic is pitch class 0.

I-maj I-min IV-maj V-maj : PCSet

I-maj  = pitchClassListToSet (# 0 ∷ # 4 ∷ # 7  ∷ [])
I-min  = pitchClassListToSet (# 0 ∷ # 3 ∷ # 7  ∷ [])
IV-maj = pitchClassListToSet (# 0 ∷ # 5 ∷ # 9  ∷ [])
V-maj  = pitchClassListToSet (# 2 ∷ # 7 ∷ # 11 ∷ [])

-- Triads, without quality
data Triad : Set where
  I   : Triad
  II  : Triad
  III : Triad
  IV  : Triad
  V   : Triad
  VI  : Triad
  VII : Triad

--data Triad : Set where
--  I : Triad; II : Triad; III : Triad; IV : Triad; V : Triad; VI : Triad; VII : Triad

allTriads : List Triad
allTriads = I ∷ II ∷ III ∷ IV ∷ V ∷ VI ∷ VII ∷ []

triadRoot : Triad → DiatonicDegree
triadRoot I   = (# 0)
triadRoot II  = (# 1)
triadRoot III = (# 2)
triadRoot IV  = (# 3)
triadRoot V   = (# 4)
triadRoot VI  = (# 5)
triadRoot VII = (# 6)

rootTriad : DiatonicDegree → Triad
rootTriad fz                                 = I
rootTriad ((fs fz))                          = II
rootTriad ((fs (fs fz)))                     = III
rootTriad ((fs (fs (fs fz))))                = IV
rootTriad ((fs (fs (fs (fs fz)))))           = V
rootTriad ((fs (fs (fs (fs (fs fz))))))      = VI
rootTriad ((fs (fs (fs (fs (fs (fs fz))))))) = VII

triadDegrees : Triad → Vec DiatonicDegree 3
triadDegrees t =
  let root = triadRoot t
      third = thirdUp root
      fifth = thirdUp third
  in root ∷ third ∷ fifth ∷ []

infix 4 _≡ᵗ_
_≡ᵗ_ : Triad → Triad → Bool
t ≡ᵗ u = triadRoot t ≡ᵈ triadRoot u

TriadSet : Set
TriadSet = BitVec s7

triadListToSet : List Triad → TriadSet
triadListToSet []       = empty
triadListToSet (t ∷ ts) = insert (triadRoot t) (triadListToSet ts)

triadSetToList : TriadSet → List Triad
triadSetToList ts = map rootTriad (elements ts)

containingTriads : DiatonicDegree → List Triad
containingTriads fz                                 = I   ∷ IV  ∷ VI  ∷ []
containingTriads ((fs fz))                          = II  ∷ V   ∷ VII ∷ []
containingTriads ((fs (fs fz)))                     = III ∷ VI  ∷ I   ∷ []
containingTriads ((fs (fs (fs fz))))                = IV  ∷ VII ∷ II  ∷ []
containingTriads ((fs (fs (fs (fs fz)))))           = V   ∷ I   ∷ III ∷ []
containingTriads ((fs (fs (fs (fs (fs fz))))))      = VI  ∷ II  ∷ IV  ∷ []
containingTriads ((fs (fs (fs (fs (fs (fs fz))))))) = VII ∷ III ∷ V   ∷ []

-- from Table of Usual Root Progressions (Major Mode), Harmony (Piston 5e), page 23
record NextTriad : Set where
  constructor nextTriad
  field
    usual     : List Triad
    sometimes : List Triad
    rare      : List Triad
open NextTriad

rootProgression : Triad → NextTriad
rootProgression I   = nextTriad (IV ∷ V   ∷ []) (VI       ∷ []) (II  ∷ III     ∷ [])
rootProgression II  = nextTriad (V        ∷ []) (IV  ∷ VI ∷ []) (I   ∷ III     ∷ [])
rootProgression III = nextTriad (VI       ∷ []) (IV       ∷ []) (I   ∷ II  ∷ V ∷ [])
rootProgression IV  = nextTriad (V        ∷ []) (I   ∷ II ∷ []) (III ∷ VI      ∷ [])
rootProgression V   = nextTriad (I        ∷ []) (IV  ∷ VI ∷ []) (II  ∷ III     ∷ [])
rootProgression VI  = nextTriad (II ∷ V   ∷ []) (III ∷ IV ∷ []) (I             ∷ [])
rootProgression VII = nextTriad (I  ∷ III ∷ []) (VI       ∷ []) (II  ∷ IV  ∷ V ∷ [])

previousTriads : Triad → List Triad
previousTriads I   = V ∷ IV ∷ VII ∷ []
previousTriads II  = VI ∷ IV ∷ []
previousTriads III = VI ∷ VII ∷ []
previousTriads IV  = I ∷ V ∷ II ∷ III ∷ []
previousTriads V   = I ∷ IV ∷ II ∷ VI ∷ []
previousTriads VI  = IV ∷ I ∷ II ∷ V ∷ VII ∷ []
previousTriads VII = []

harmonizations : {n : ℕ} → Vec DiatonicDegree n → List (Vec Triad n)
harmonizations [] = []
harmonizations (d ∷ []) = map (_∷ []) (containingTriads d)
harmonizations (d ∷ d' ∷ ds) =
  let tss = harmonizations (d' ∷ ds)
      dTriads  = containingTriads d
  in concatMap (λ t → concatMaybe (map (prependTriad t) tss)) dTriads
  where
    prevOk : Triad → Triad → Bool
    prevOk t x = (triadRoot t) ∈ triadListToSet (previousTriads x)
    prependTriad : {n : ℕ} → Triad → Vec Triad (suc n) → Maybe (Vec Triad (suc (suc n)))
    prependTriad t ts = if prevOk t (Data.Vec.head ts) then just (t ∷ ts) else nothing

halfCadence : {n : ℕ} → Vec Triad n → Bool
halfCadence []           = false
halfCadence (t ∷ [])     = t ≡ᵗ V
halfCadence (_ ∷ t ∷ ts) = halfCadence (t ∷ ts)

-- Given a pitch p and a diatontic degree d, return a pitch that
-- has degree d and is 1-2 octaves lower than p.
pitchLower : Pitch → DiatonicDegree → Pitch
pitchLower p d =
  let (c , o) = absoluteToRelative p
      c'      = degree→PC major d
  in relativeToAbsolute (c' , o ∸ 2)

-- Given a soporano voice s a pitch and the other voices
-- as diatonic degrees of a major scale, voice the
-- accompaniment in close position.
voiceChord : Pitch → Vec DiatonicDegree 3 → Vec Pitch 3
voiceChord s (a ∷ t ∷ b ∷ [])  =
  let (s' , o) = absoluteToRelative s
      a'       = degree→PC major a
      t'       = degree→PC major t
      b'       = degree→PC major b
      ao       = downOctave a' s' o
      to       = downOctave t' a' ao
      bo       = downOctave b' t' to
  in relativeToAbsolute (a' , ao) ∷
     relativeToAbsolute (t' , to) ∷
     relativeToAbsolute (b' , bo) ∷ []
  where downOctave : PC → PC → Octave → Octave
        downOctave pc₁ pc₂ o =
          if toℕ pc₁ <ᵇ toℕ pc₂ then o
          else (o ∸ 1)

-- Given a soprano pitch p and a triad harmonization t,
-- generate a list of possible bass notes.
-- Assumes p is in t. Only the root of the triad is
-- allowed to be doubled.
-- Each bass note is pitched 1-2 octaves below p.
bassNotes : Pitch → Triad → List Pitch
bassNotes p t =
  let sop  = pitch→DegreeCMajor p
      root = triadRoot t
      ds   = toList (triadDegrees t)
      ds'  = filter (λ d → (sop ≡ᵈ root) ∨ not (sop ≡ᵈ d)) ds
  in map (pitchLower p) ds'

-- Given a soprano pitch p and a triad harmonization t,
-- generate a harmonizing chord in root position.
-- Assumes p is in t. Only the root of the triad is
-- allowed to be doubled.
-- Each bass note is pitched 1-2 octaves below p.
-- Alto and Tenor fit inside.
-- Currently root or third is preferred for alto.
harmonizingChord : Pitch → Triad → Vec Pitch 3
harmonizingChord p t =
  let sop   = pitch→DegreeCMajor p
      root  = triadRoot t
      third = thirdUp root
      fifth = thirdUp third
      alto  = if sop ≡ᵈ root then third else root
      tenor = if sop ≡ᵈ fifth then third else fifth
  in voiceChord p (alto ∷ tenor ∷ root ∷ [])
  where
    remove : DiatonicDegree → Vec DiatonicDegree 3 → Vec DiatonicDegree 2
    remove sop (d ∷ d₁ ∷ d₂ ∷ []) =
      if d ≡ᵈ sop then d₁ ∷ d₂ ∷ []
      else (if d₁ ≡ᵈ sop then d ∷ d₂ ∷ [] else d ∷ d₁ ∷ [])

-- Create 4 part harmonizations ending in V for a melody in C major.
voicedHarmonizations : {n : ℕ} → Vec Pitch n → List (Vec (Vec Pitch 4) n)
voicedHarmonizations {n} ps =
  let ds = Data.Vec.map pitch→DegreeCMajor ps
      hs : List (Vec Triad n)
      hs = filter halfCadence (harmonizations ds)
  in map (λ ts → Data.Vec.map (λ pt → proj₁ pt ∷ harmonizingChord (proj₁ pt) (proj₂ pt))
                              (Data.Vec.zip ps ts)) hs

-- Check interval between each pair of voices.
intervalsOkFilter : Vec Pitch 4 → Bool
intervalsOkFilter (s ∷ a ∷ t ∷ b ∷ []) =
  null (concatMaybe (map (intervalCheck ∘ toPitchInterval)
--                         ((s , a) ∷ (s , t) ∷ (s , b) ∷ (a , t) ∷ (a , b) ∷ (t , b) ∷ [])))
                         ((s , a) ∷ (s , b) ∷ (s , t) ∷ [])))

filterIntervalsOk : {n : ℕ} → List (Vec (Vec Pitch 4) n) → List (Vec (Vec Pitch 4) n)
filterIntervalsOk xs =
  let f : List (Vec Pitch 4) → Bool
      f xs = foldr _∧_ true (map intervalsOkFilter xs)
  in filter (f ∘ toList) xs

motionErrors : {n : ℕ} → Vec (Vec Pitch 4) n → List MotionError
motionErrors xs =
  let ss = Data.Vec.map (Data.Vec.head) xs
      as = Data.Vec.map (Data.Vec.head ∘ Data.Vec.tail) xs
      ts = Data.Vec.map (Data.Vec.head ∘ Data.Vec.tail ∘ Data.Vec.tail) xs
      bs = Data.Vec.map (Data.Vec.head ∘ Data.Vec.tail ∘ Data.Vec.tail ∘ Data.Vec.tail) xs

      sas = map toPitchInterval (toList (Data.Vec.zip as ss))
      sts = map toPitchInterval (toList (Data.Vec.zip ts ss))
      sbs = map toPitchInterval (toList (Data.Vec.zip bs ss))
      ats = map toPitchInterval (toList (Data.Vec.zip ts as))
      abs = map toPitchInterval (toList (Data.Vec.zip bs as))
      tbs = map toPitchInterval (toList (Data.Vec.zip bs ts))
  in concatMap checkMotion (sas ∷ sts ∷ sbs ∷ ats ∷ abs ∷ tbs ∷ [])

--filterSBMotionOk : {n : ℕ} → List (Vec (Vec Pitch 4) n) → List (Vec (Vec Pitch 4) n)
--filterSBMotionOk = filter motionOkFilter

-- Given a soprano line with harmonization, generate
-- a list of possible bass lines 1-1 with soprano notes.
-- The SB counterpoint must satisfy 1st species
-- interval and motion rules.
bassLines : List (Pitch × Triad) → List (List Pitch)
-- We need to make the base case a singleton list of an empty list for
-- the general case to work. Possibly look into modifying the general
-- case to handle a base case of an empty list.
bassLines [] = [] ∷ []
bassLines ((sop , triad) ∷ pts) =
  let pss = bassLines pts
      basses  = bassNotes sop triad
      intervalOkSBs : List PitchInterval -- list of bass notes with interval (to sop) that pass intervalCheck
      intervalOkSBs = filter (is-nothing ∘ intervalCheck) (map (toPitchInterval ∘ (_, sop)) basses)
      intervalOkBs = map proj₁ intervalOkSBs
      intervalOkBassLines = concatMap (λ ps → (map (_∷ ps) intervalOkBs)) pss
  in filter (mCheck sop (Data.Maybe.map proj₁ (head pts))) intervalOkBassLines
  where
    -- Given a soprano pitch, possibly a second soprano pitch and a list of
    -- bass pitches, if the second soprano pitch exists and there are at
    -- least two bass pitches, check that the motion from the first SB pair to
    -- the second is allowed. If there aren't two SB pairs, return true.
    mCheck : Pitch → Maybe Pitch → List Pitch → Bool
    mCheck _ nothing  _               = true
    mCheck _ (just _) []              = true
    mCheck _ (just _) (_ ∷ [])        = true
    mCheck s₁ (just s₂) (b₁ ∷ b₂ ∷ _) =
      let sb₁ = toPitchInterval (b₁ , s₁)
          sb₂ = toPitchInterval (b₂ , s₂)
      in (is-nothing ∘ uncurry motionCheck) (sb₁ , sb₂)

-- Given a soprano line with harmonization, generate
-- a list of possible triads 1-1 with soprano notes.
-- All pairwise counterpoint must satisfy 1st species
-- interval and motion rules.
chordProg : List (Pitch × Triad) → List (List Pitch)
-- We need to make the base case a singleton list of an empty list for
-- the general case to work. Possibly look into modifying the general
-- case to handle a base case of an empty list.
chordProg [] = [] ∷ []
chordProg ((sop , triad) ∷ pts) =
  let pss = chordProg pts
      basses  = bassNotes sop triad
      intervalOkSBs : List PitchInterval -- list of bass notes with interval (to sop) that pass intervalCheck
      intervalOkSBs = filter (is-nothing ∘ intervalCheck) (map (toPitchInterval ∘ (_, sop)) basses)
      intervalOkBs = map proj₁ intervalOkSBs
      intervalOkBassLines = concatMap (λ ps → (map (_∷ ps) intervalOkBs)) pss
  in filter (mCheck sop (Data.Maybe.map proj₁ (head pts))) intervalOkBassLines
  where
    -- Given a soprano pitch, possibly a second soprano pitch and a list of
    -- bass pitches, if the second soprano pitch exists and there are at
    -- least two bass pitches, check that the motion from the first SB pair to
    -- the second is allowed. If there aren't two SB pairs, return true.
    mCheck : Pitch → Maybe Pitch → List Pitch → Bool
    mCheck _ nothing  _               = true
    mCheck _ (just _) []              = true
    mCheck _ (just _) (_ ∷ [])        = true
    mCheck s₁ (just s₂) (b₁ ∷ b₂ ∷ _) =
      let sb₁ = toPitchInterval (b₁ , s₁)
          sb₂ = toPitchInterval (b₂ , s₂)
      in (is-nothing ∘ uncurry motionCheck) (sb₁ , sb₂)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
{-# OPTIONS --verbose=10 #-}

module lemmas where

  open import Data.Nat
  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)

  +-suc : (n₁ n₂ : ℕ) -> (n₁ + (1 + n₂)) ≡ (1 + (n₁ + n₂))
  +-suc zero n2 = refl
  +-suc (suc n1) n2 rewrite +-suc n1 n2 = refl

max_stars_repo_name: hablapps/safeoptics

max_issues_repo_name: hablapps/safeoptics

max_forks_repo_name: hablapps/safeoptics


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

open import HoTT
open import cohomology.FunctionOver
open import cohomology.Theory

{- Cohomology groups are independent of basepoint, and the action of
 - the cohomology is independent of the basepoint-preservation path -}

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

open CohomologyTheory CT

C-base-indep : (n : ℤ) {A : Type i} (a₀ a₁ : A)
  → C n (A , a₀) ≃ᴳ C n (A , a₁)
C-base-indep n a₀ a₁ =
  C-Susp n (_ , a₁) ∘eᴳ (C-Susp n (_ , a₀))⁻¹ᴳ

CF-base-indep : (n : ℤ) {X Y : Ptd i}
  (f : fst X → fst Y) (p₁ p₂ : f (snd X) == snd Y)
  → CF-hom n (f , p₁) == CF-hom n (f , p₂)
CF-base-indep n {X} {Y} f p₁ p₂ = transport
  (λ q → CF-hom n (f , p₁) == CF-hom n (f , p₂) [ uncurry _→ᴳ_ ↓ q ])
  (!-inv-l (pair×= (group-ua (C-Susp n Y)) (group-ua (C-Susp n X))))
  (!ᵈ (C-Susp-↓ n (f , p₁)) ∙ᵈ C-Susp-↓ n (f , p₂))

CF-λ= : (n : ℤ) {X Y : Ptd i} {f g : fst (X ⊙→ Y)}
  → (∀ x → fst f x == fst g x)
  → CF-hom n f == CF-hom n g
CF-λ= n h = CF-base-indep n _ _ _ ∙ ap (CF-hom n) (⊙λ= h idp)

CF-↓dom= : (n : ℤ) {X Y Z : Ptd i}
  {f : fst (X ⊙→ Y)} {g : fst (X ⊙→ Z)} {p : Y == Z}
  → fst f == fst g [ (λ V → fst X → fst V) ↓ p ]
  → CF-hom n f == CF-hom n g [ (λ G → G →ᴳ C n X) ↓ ap (C n) p ]
CF-↓dom= n {p = idp} r =
  CF-base-indep n _ _ _ ∙ ap (CF-hom n) (pair= r (from-transp! _ _ idp))

CF-↓cod= : (n : ℤ) {X Y Z : Ptd i}
  {f : fst (X ⊙→ Z)} {g : fst (Y ⊙→ Z)} {p : X == Y}
  → fst f == fst g [ (λ U → fst U → fst Z) ↓ p ]
  → CF-hom n f == CF-hom n g [ (λ G → C n Z →ᴳ G) ↓ ap (C n) p ]
CF-↓cod= n {p = idp} r =
  CF-base-indep n _ _ _ ∙ ap (CF-hom n) (pair= r (from-transp! _ _ idp))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


text:
module PatternSynonymOverapplied2 where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

pattern suc' x = suc x

f : Nat -> Nat
f zero       = zero
f (suc' m n) = n

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Structure.Function.Linear where

import      Lvl
open import Logic
open import Logic.Propositional
open import Relator.Equals
open import Relator.Equals.Proofs
open import Type

-- TODO: Remove this
module _ {ℓ₁}{ℓ₂}{ℓ₃} {V₁ : Type{ℓ₁}} {V₂ : Type{ℓ₂}} {S : Type{ℓ₃}} where
  record LinearMap  (_+₁_ : V₁ → V₁ → V₁) (_⋅₁_ : S → V₁ → V₁)  (_+₂_ : V₂ → V₂ → V₂) (_⋅₂_ : S → V₂ → V₂) (f : V₁ → V₂) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field
      additivity   : ∀{v₁ v₂ : V₁} → (f(v₁ +₁ v₂) ≡ f(v₁) +₂ f(v₂))
      homogeneity1 : ∀{s : S} → ∀{v : V₁} → (f(s ⋅₁ v) ≡ s ⋅₂ f(v))

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:
module Relation.Ternary.Separation.Monad.Identity where

open import Level
open import Function
open import Function using (_∘_; case_of_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
open import Relation.Unary.PredicateTransformer hiding (_⊔_)
open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Morphisms

open import Data.Unit
open Monads

module Identity {ℓ}
  {C : Set ℓ} {u}
  {{r : RawSep C}}
  {{us : IsUnitalSep r u}}
 where

  Id : ∀ {ℓ} → Pt C ℓ
  Id P = P

  instance
    id-monad : Monad ⊤ ℓ (λ _ _ → Id)
    Monad.return id-monad = id
    app (Monad.bind id-monad f) px = app f px


text:
module Data.Nat where

import Prelude
import Data.Bool as Bool

open Prelude
open Bool

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN SUC suc #-}
{-# BUILTIN ZERO zero #-}

infix 40 _==_ _<_ _≤_ _>_ _≥_
infixl 60 _+_ _-_
infixl 70 _*_
infixr 80 _^_
infix 100 _!

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

_-_ : Nat -> Nat -> Nat
zero  - m     = zero
suc n - zero  = suc n
suc n - suc m = n - m

_*_ : Nat -> Nat -> Nat
zero  * m = zero
suc n * m = m + n * m

_^_ : Nat -> Nat -> Nat
n ^ zero  = 1
n ^ suc m = n * n ^ m

_! : Nat -> Nat
zero  ! = 1
suc n ! = suc n * n !

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATMINUS _-_ #-}
{-# BUILTIN NATTIMES _*_ #-}

_==_ : Nat -> Nat -> Bool
zero  == zero  = true
zero  == suc _ = false
suc _ == zero  = false
suc n == suc m = n == m

_<_ : Nat -> Nat -> Bool
n     < zero  = false
zero  < suc m = true
suc n < suc m = n < m

_≤_ : Nat -> Nat -> Bool
n ≤ m = n < suc m

_>_ = flip _<_
_≥_ = flip _≤_

{-# BUILTIN NATEQUALS _==_ #-}
{-# BUILTIN NATLESS   _<_  #-}

divSuc : Nat -> Nat -> Nat
divSuc  zero   _ = zero
divSuc (suc n) m = 1 + divSuc (n - m) m

modSuc : Nat -> Nat -> Nat
modSuc  zero   _ = zero
modSuc (suc n) m =
  ! n ≤ m  => suc n
  ! otherwise modSuc (n - m) m

{-# BUILTIN NATDIVSUC divSuc #-}
-- {-# BUILTIN NATMODSUC modSuc #-}

div : Nat -> Nat -> Nat
div n  zero   = zero
div n (suc m) = divSuc n m

mod : Nat -> Nat -> Nat
mod n  zero   = zero
mod n (suc m) = modSuc n m

gcd : Nat -> Nat -> Nat
gcd a 0 = a
gcd a b = gcd b (mod a b)

lcm : Nat -> Nat -> Nat
lcm a b = div (a * b) (gcd a b)

even : Nat -> Bool
even n = mod n 2 == 0

odd : Nat -> Bool
odd n = mod n 2 == 1

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists with fast append
------------------------------------------------------------------------

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

module Data.DifferenceList where

open import Data.List.Base as L using (List)
open import Function
open import Data.Nat.Base

infixr 5 _∷_ _++_

DiffList : ∀ {ℓ} → Set ℓ → Set ℓ
DiffList A = List A → List A

lift : ∀ {a} {A : Set a} →
       (List A → List A) → (DiffList A → DiffList A)
lift f xs = λ k → f (xs k)

[] : ∀ {a} {A : Set a} → DiffList A
[] = λ k → k

_∷_ : ∀ {a} {A : Set a} → A → DiffList A → DiffList A
_∷_ x = lift (L._∷_ x)

[_] : ∀ {a} {A : Set a} → A → DiffList A
[ x ] = x ∷ []

_++_ : ∀ {a} {A : Set a} → DiffList A → DiffList A → DiffList A
xs ++ ys = λ k → xs (ys k)

toList : ∀ {a} {A : Set a} → DiffList A → List A
toList xs = xs L.[]

-- fromList xs is linear in the length of xs.

fromList : ∀ {a} {A : Set a} → List A → DiffList A
fromList xs = λ k → xs ⟨ L._++_ ⟩ k

-- It is OK to use L._++_ here, since map is linear in the length of
-- the list anyway.

map : ∀ {a b} {A : Set a} {B : Set b} →
      (A → B) → DiffList A → DiffList B
map f xs = λ k → L.map f (toList xs) ⟨ L._++_ ⟩ k

-- concat is linear in the length of the outer list.

concat : ∀ {a} {A : Set a} → DiffList (DiffList A) → DiffList A
concat xs = concat' (toList xs)
  where
  concat' : ∀ {a} {A : Set a} → List (DiffList A) → DiffList A
  concat' = L.foldr _++_ []

take : ∀ {a} {A : Set a} → ℕ → DiffList A → DiffList A
take n = lift (L.take n)

drop : ∀ {a} {A : Set a} → ℕ → DiffList A → DiffList A
drop n = lift (L.drop n)


text:
module Issue665 where

postulate
  A : Set

record I : Set where
  constructor i
  field
    f : A

data Wrap : (j : I) → Set where
  con : ∀ {j} → Wrap j

postulate
  C : Set
  anything : C

works1 : ∀ {X} -> Wrap X -> C
works1 (con {i _}) with anything
... | z = z

works2 : ∀ {X} -> Wrap X -> C
works2 (con {_}) with anything
... | z = z

bugged : ∀ {X} -> Wrap X -> C
bugged con with anything
... | z = z


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

module F1 where

open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Product hiding (map)
open import Data.List

open import Data.Nat
open import Data.Bool

{--
infixr 90 _⊗_
infixr 80 _⊕_
infixr 60 _∘_
infix  30 _⟷_
--}

---------------------------------------------------------------------------
-- Paths

-- Path relation should be an equivalence
data Path (A : Set) : Set where
  _↝_ : (a : A) → (b : A) → Path A

id↝ : {A : Set} → (a : A) → Path A
id↝ a = a ↝ a

ap : {A B : Set} → (f : A → B) → Path A → Path B
ap f (a ↝ a') = f a ↝ f a'

pathProd : {A B : Set} → Path A → Path B → Path (A × B)
pathProd (a ↝ a') (b ↝ b') = (a , b) ↝ (a' , b')

pathProdL : {A B : Set} → List (Path A) → List (Path B) → List (Path (A × B))
pathProdL pas pbs = concatMap (λ pa → map (pathProd pa) pbs) pas

-- pi types with exactly one level of reciprocals

data B0 : Set where
  ONE    : B0
  PLUS0  : B0 → B0 → B0
  TIMES0 : B0 → B0 → B0

data B1 : Set where
  LIFT0  : B0 → B1
  PLUS1  : B1 → B1 → B1
  TIMES1 : B1 → B1 → B1
  RECIP1 : B0 → B1

-- interpretation of B0 as discrete groupoids

record 0-type : Set₁ where
  constructor G₀
  field
    ∣_∣₀ : Set

open 0-type public

plus : 0-type → 0-type → 0-type
plus t₁ t₂ = G₀ (∣ t₁ ∣₀ ⊎ ∣ t₂ ∣₀)

times : 0-type → 0-type → 0-type
times t₁ t₂ = G₀ (∣ t₁ ∣₀ × ∣ t₂ ∣₀)

⟦_⟧₀ : B0 → 0-type
⟦ ONE ⟧₀ = G₀ ⊤
⟦ PLUS0 b₁ b₂ ⟧₀ = plus ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀
⟦ TIMES0 b₁ b₂ ⟧₀ = times ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀

elems0 : (b : B0) → List ∣ ⟦ b ⟧₀ ∣₀
elems0 ONE = [ tt ]
elems0 (PLUS0 b b') = map inj₁ (elems0 b) ++ map inj₂ (elems0 b')
elems0 (TIMES0 b b') =
  concatMap (λ a → map (λ b → (a , b)) (elems0 b')) (elems0 b)

-- interpretation of B1 types as 2-types

record 2-type : Set₁ where
  constructor G₂
  field
    ∣_∣₁ : Set
    1-paths : List (Path ∣_∣₁)
    2-paths : List (Path (Path ∣_∣₁))

open 2-type public

_⊎↝_ : {A B : Set} → List (Path A) → List (Path B) → List (Path (A ⊎ B))
p₁ ⊎↝ p₂ = map (ap inj₁) p₁ ++ map (ap inj₂) p₂

⟦_⟧₁ : B1 → 2-type
⟦ LIFT0 b0 ⟧₁ = G₂ ∣ ⟦ b0 ⟧₀ ∣₀ (map id↝ (elems0 b0)) []
⟦ PLUS1 b₁ b₂ ⟧₁ with ⟦ b₁ ⟧₁ | ⟦ b₂ ⟧₁
... | G₂ 0p₁ 1p₁ 2p₁ | G₂ 0p₂ 1p₂ 2p₂ = G₂ (0p₁ ⊎ 0p₂) (1p₁ ⊎↝ 1p₂) []
⟦ TIMES1 b₁ b₂ ⟧₁ = G₂ {!!} {!!} []
⟦ RECIP1 b0 ⟧₁ = G₂ ⊤ (map (λ _ → tt ↝ tt) (elems0 b0)) []

test10 = ⟦ LIFT0 ONE ⟧₁
test11 = ⟦ LIFT0 (PLUS0 ONE ONE) ⟧₁
test12 = ⟦ RECIP1 (PLUS0 ONE ONE) ⟧₁

{--

-- isos

data _⟷_ : B → B → Set where
  -- +
  swap₊   : { b₁ b₂ : B } → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  -- *
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  -- congruence
  id⟷   : { b : B } → b ⟷ b
  sym    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _∘_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)

-- interpret isos as functors

record 0-functor (A B : 0-type) : Set where
  constructor F₀
  field
    fobj : ∣ A ∣ → ∣ B ∣
  fmor : {a b : ∣ A ∣} → (a ≡ b) → (fobj a ≡ fobj b)
  fmor {a} {.a} (refl .a) = refl (fobj a)

open 0-functor public

swap⊎ : {A B : Set} → A ⊎ B → B ⊎ A
swap⊎ (inj₁ a) = inj₂ a
swap⊎ (inj₂ b) = inj₁ b

eval : {b₁ b₂ : B} → (b₁ ⟷ b₂) → 0-functor ⟦ b₁ ⟧ ⟦ b₂ ⟧
eval swap₊ = F₀ swap⊎
eval assocl₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
eval assocr₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
eval unite⋆ = ? -- : { b : B } → TIMES ONE b ⟷ b
eval uniti⋆ = ? -- : { b : B } → b ⟷ TIMES ONE b
eval swap⋆ = ? --  : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
eval assocl⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
eval assocr⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
eval dist = ? -- : { b₁ b₂ b₃ : B } → TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
eval factor = ? -- : { b₁ b₂ b₃ : B } → PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
eval id⟷ = ? --  : { b : B } → b ⟷ b
eval (sym c) = ? -- : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
eval (c₁ ∘ c₂) = ? -- : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
eval (c₁ ⊕ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
eval (c₁ ⊗ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)

---------------------------------------------------------------------------
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Generic.Reflection.ReadData where

open import Generic.Core
open import Generic.Function.FoldMono

‵π : ArgInfo -> String -> Term -> Term -> Term
‵π i s a b = sate π (reify i) (sate refl) ∘ sate coerce ∘ sate _,_ a $
  appDef (quote appRel) (implRelArg (reify (relevance i)) ∷ explRelArg (explLam s b) ∷ [])

quoteHyp : Name -> ℕ -> Type -> Maybe (Maybe Term)
quoteHyp d p   (pi s (arg i a) b) =
  quoteHyp d p a >>= maybe (const nothing) (fmap (‵π i s a) <$> quoteHyp d p b)
quoteHyp d p t@(appDef n is)      = just $ d == n ?> sate var (toTuple ∘ map argVal $ drop p is)
quoteHyp d p t                    = just nothing

quoteDesc : Name -> ℕ -> Type -> Maybe Term
quoteDesc d p (pi s (arg i a) b) =
  (λ ma' b' -> maybe (λ a' -> sate _⊛_ a' (unshift′ b')) (‵π i s a b') ma')
    <$> quoteHyp d p a <*> quoteDesc d p b
quoteDesc d p  t                 = join $ quoteHyp d p t

-- We didn't need that `β` previously. Why do we need it now?
-- Or, perhaps, why didn't we need it earlier? It kinda makes sense.
quoteData : Data Type -> TC Term
quoteData (packData d a b cs ns) =
  case termLevelOf (monoLastType b) ⊗ mapM (quoteDesc d (countPis a)) cs of λ
    {  nothing         -> throw "can't read a data type"
    ; (just (β , cs′)) -> (λ qa qb -> explLamsBy a ∘ curryBy b ∘ appDef (quote μ)
           $ implRelArg unknown
           ∷ implRelArg β
           ∷ explRelArg (sate packData (reify d) qa qb (reify cs′) (reify ns))
           ∷ [])
         <$> quoteTC a <*> quoteTC b
    }

onFinalMu : ∀ {α} {A : Set α} -> (∀ {ι β} {I : Set ι} -> Data (Desc I β) -> TC A) -> Type -> TC A
onFinalMu k = monoLastType >>> λ
  { (appDef (quote μ) (implRelArg qι ∷ implRelArg qβ ∷ implRelArg qI ∷ explRelArg qD ∷ _)) ->
       bindTC (unquoteTC qι) λ ι ->
       bindTC (unquoteTC qβ) λ β ->
       bindTC (unquoteTC qI) λ I ->
       bindTC (unquoteTC qD) λ D -> k {ι} {β} {I} D
  ;  _                                                                                ->
       throw "the return type must be μ"
  }

guncoercePure : Data Type -> Term
guncoercePure (packData d a b cs ns) = explLam "x" ∘ vis appDef (quote curryFoldMono)
  $ explUncurryBy b (vis appDef d (replicate (countExplPis a) unknown))
  ∷ pureVar 0
  ∷ unmap pureCon ns

macro
  readData : Name -> Term -> TC _
  readData d ?r = getData d >>= quoteData >>= unify ?r

  gcoerce : Name -> Term -> TC _
  gcoerce fd ?r = inferNormType ?r >>= onFinalMu λ{ D@(packData _ _ b _ _) ->
      quoteTC (μ D) >>= λ μD ->
      traverseAll quoteTC (allCons D) >>= λ cs′ ->
      unify ?r $ vis appDef fd (curryBy b μD ∷ allToList cs′)
    }

  guncoerce : ∀ {ι β} {I : Set ι} {D : Data (Desc I β)} {j} -> μ D j -> Term -> TC _
  guncoerce {D = packData d a b cs ns} e ?r =
    quoteTC e >>= λ qe -> unify ?r ∘ vis appDef (quote curryFoldMono)
      $ explUncurryBy b (vis appDef d (replicate (countExplPis a) unknown))
      ∷ qe
      ∷ unmap pureCon ns

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
-- Context extension of presheaves
module SOAS.Families.Delta {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Sorting
open import SOAS.Construction.Structure
open import SOAS.Families.Core {T}

-- | General context extension by a context Θ

module Unsorted where

  -- Concatenate Θ to the context of a family
  δ : Ctx → Family → Family
  δ Θ X Γ = X (Θ ∔ Γ)

  δF : Ctx → Functor 𝔽amilies 𝔽amilies
  δF Θ = record { F₀ = δ Θ ; F₁ = λ f → f ; identity = refl
                 ; homomorphism = refl ; F-resp-≈ = λ z → z }

  -- | Context extension by a single type τ, a special case of δ with ⌊ τ ⌋
  δ₁ : T → Family → Family
  δ₁ τ = δ ⌈ τ ⌋

  δ₁F_ : T → Functor 𝔽amilies 𝔽amilies
  δ₁F τ = δF ⌈ τ ⌋

private
  variable
    Γ Δ : Ctx
    α : T

module Sorted where
  -- Concatenate Θ to the context of a family
  δ : Ctx → Familyₛ → Familyₛ
  δ Θ 𝒳 α Γ = 𝒳 α (Θ ∔ Γ)

  δF : Ctx → Functor 𝔽amiliesₛ 𝔽amiliesₛ
  δF Θ = record { F₀ = δ Θ ; F₁ = λ f → f ; identity = refl
                 ; homomorphism = refl ; F-resp-≈ = λ z → z }

  -- | Context extension by a single type τ, a special case of δ with ⌊ τ ⌋
  δ₁ : T → Familyₛ → Familyₛ
  δ₁ τ = δ ⌈ τ ⌋

  δ₁F_ : T → Functor 𝔽amiliesₛ 𝔽amiliesₛ
  δ₁F τ = δF ⌈ τ ⌋

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas