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.Base.Types
open import LibraBFT.Impl.OBM.Rust.Duration
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Base.Types
open import Optics.All
open import Util.ByteString
open import Util.Encode
open import Util.Hash
open import Util.KVMap                        as Map
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String using (String)

-- Defines the types that /DO NOT/ depend on an epoch config.
-- TODO-3: update types to reflect more recent version of LibraBFT.  This is
-- a substantial undertaking that should probably be led by someone who can
-- access our internal implementation.

module LibraBFT.ImplShared.Consensus.Types.EpochIndep where
  -- Below here is incremental progress towards something
  -- that will eventually mirror the types in LBFT.Consensus.Types
  -- that /DO NOT/ depend on the set of active authors
  -- or safety rules, which we call the /EpochConfig/.

  Author : Set
  Author = NodeId

  AccountAddress : Set
  AccountAddress = Author

  AuthorName : Set
  AuthorName = Author

  aAuthorName : Lens Author AuthorName
  aAuthorName = mkLens' (λ x → x) (λ x → const x)

  HashValue : Set
  HashValue = Hash

  TX : Set
  TX = ByteString

  Instant : Set
  Instant = ℕ   -- TODO-2: should eventually be a time stamp

  postulate -- TODO-1: implement/prove PK equality
    _≟-PK_ : (pk1 pk2 : PK) → Dec (pk1 ≡ pk2)
  instance
    Eq-PK : Eq PK
    Eq._≟_ Eq-PK = _≟-PK_

  -- LBFT-OBM-DIFF: We do not have world state.  We just count the Epoch/Round as the version.
  record Version : Set where
    constructor Version∙new
    field
      _vVE : Epoch
      _vVR : Round
  open Version public
  postulate instance enc-Version : Encoder Version

  postulate -- TODO-1: implement/prove Version equality
    _≟-Version_ : (v1 v2 : Version) → Dec (v1 ≡ v2)
  instance
    Eq-Version : Eq Version
    Eq._≟_ Eq-Version = _≟-Version_

  _≤-Version_ : Version → Version → Set
  v1 ≤-Version v2 = _vVE v1 < _vVE v2
                  ⊎ _vVE v1 ≡ _vVE v2 × _vVR v1 ≤ _vVR v2

  _≤?-Version_ : (v1 v2 : Version) → Dec (v1 ≤-Version v2)
  v1 ≤?-Version v2
     with _vVE v1 <? _vVE v2
  ...| yes prf = yes (inj₁ prf)
  ...| no  ege
     with _vVE v1 ≟ _vVE v2
  ...| no  rneq = no (⊥-elim ∘ λ { (inj₁ x) → ege x
                                 ; (inj₂ (x , _)) → rneq x })
  ...| yes refl
     with _vVR v1 ≤? _vVR v2
  ...| yes rleq = yes (inj₂ (refl , rleq))
  ...| no  rgt  = no (⊥-elim ∘ λ { (inj₁ x) → ege x
                                 ; (inj₂ (_ , x)) → rgt x })

  _<-Version_ : Version → Version → Set
  v1 <-Version v2 = _vVE v1 < _vVE v2
                  ⊎ _vVE v1 ≡ _vVE v2 × _vVR v1 < _vVR v2

  _<?-Version_ : (v1 v2 : Version) → Dec (v1 <-Version v2)
  v1 <?-Version v2
     with _vVE v1 <? _vVE v2
  ...| yes prf = yes (inj₁ prf)
  ...| no  ege
     with _vVE v1 ≟ _vVE v2
  ...| no  rneq = no (⊥-elim ∘ λ { (inj₁ x) → ege x
                                 ; (inj₂ (x , _)) → rneq x })
  ...| yes refl
     with _vVR v1 <? _vVR v2
  ...| yes rleq = yes (inj₂ (refl , rleq))
  ...| no  rgt  = no (⊥-elim ∘ λ { (inj₁ x) → ege x
                                 ; (inj₂ (_ , x)) → rgt x })

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

  record ValidatorSigner : Set where
    constructor ValidatorSigner∙new
    field
      _vsAuthor     : AccountAddress
      _vsPrivateKey : SK      -- Note that the SystemModel doesn't
                              -- allow one node to examine another's
                              -- state, so we don't model someone being
                              -- able to impersonate someone else unless
                              -- PK is "dishonest", which models the
                              -- possibility that the corresponding secret
                              -- key may have been leaked.
  open ValidatorSigner public
  unquoteDecl  vsAuthor   vsPrivateKey = mkLens (quote ValidatorSigner)
              (vsAuthor ∷ vsPrivateKey ∷ [])

  RawEncNetworkAddress = Author

  record ValidatorConfig : Set where
    constructor ValidatorConfig∙new
    field
      _vcConsensusPublicKey      : PK
      _vcValidatorNetworkAddress : RawEncNetworkAddress
  open ValidatorConfig public
  unquoteDecl vcConsensusPublicKey   vcValidatorNetworkAddress = mkLens (quote ValidatorConfig)
             (vcConsensusPublicKey ∷ vcValidatorNetworkAddress ∷ [])

  record ValidatorInfo : Set where
    constructor ValidatorInfo∙new
    field
      _viAccountAddress       : AccountAddress
      _viConsensusVotingPower : U64
      _viConfig               : ValidatorConfig
  open ValidatorInfo public
  unquoteDecl viAccountAddress   viConsensusVotingPower   viConfig = mkLens (quote ValidatorInfo)
             (viAccountAddress ∷ viConsensusVotingPower ∷ viConfig ∷ [])

  -- getter only in Haskell
  -- key for validating signed messages from this validator
  viConsensusPublicKey : Lens ValidatorInfo PK
  viConsensusPublicKey = viConfig ∙ vcConsensusPublicKey

  record ValidatorConsensusInfo : Set where
    constructor ValidatorConsensusInfo∙new
    field
     _vciPublicKey   : PK
     _vciVotingPower : U64
  open ValidatorConsensusInfo public
  unquoteDecl vciPublicKey   vciVotingPower = mkLens (quote ValidatorConsensusInfo)
             (vciPublicKey ∷ vciVotingPower ∷ [])

  record ValidatorVerifier : Set where
    constructor mkValidatorVerifier
    field
      _vvAddressToValidatorInfo : KVMap AccountAddress ValidatorConsensusInfo
      _vvQuorumVotingPower      : ℕ  -- TODO-2: see above; for now, this is QuorumSize
      _vvTotalVotingPower       : ℕ  -- TODO-2: see above; for now, this is number of peers in EpochConfig
  open ValidatorVerifier public
  unquoteDecl vvAddressToValidatorInfo   vvQuorumVotingPower   vvTotalVotingPower = mkLens (quote ValidatorVerifier)
             (vvAddressToValidatorInfo ∷ vvQuorumVotingPower ∷ vvTotalVotingPower ∷ [])

  -- getter only in Haskell
  vvObmAuthors : Lens ValidatorVerifier (List AccountAddress)
  vvObmAuthors = mkLens' g s
   where
    g : ValidatorVerifier → List AccountAddress
    g vv = Map.kvm-keys (vv ^∙ vvAddressToValidatorInfo)
    s : ValidatorVerifier → List AccountAddress → ValidatorVerifier
    s vv _ = vv -- TODO-1 : cannot be done: need a way to defined only getters

  data ConsensusScheme : Set where ConsensusScheme∙new : ConsensusScheme
  -- instance S.Serialize ConsensusScheme

  record ValidatorSet : Set where
    constructor ValidatorSet∙new
    field
      _vsScheme  : ConsensusScheme
      _vsPayload : List ValidatorInfo
  -- instance S.Serialize ValidatorSet
  open ValidatorSet public
  unquoteDecl vsScheme   vsPayload = mkLens (quote ValidatorSet)
             (vsScheme ∷ vsPayload ∷ [])

  record EpochState : Set where
    constructor EpochState∙new
    field
      _esEpoch    : Epoch
      _esVerifier : ValidatorVerifier
  open EpochState public
  unquoteDecl esEpoch   esVerifier = mkLens (quote EpochState)
             (esEpoch ∷ esVerifier ∷ [])

  postulate -- one valid assumption, one that can be proved using it
    instance
      Enc-EpochState   : Encoder EpochState
      Enc-EpochStateMB : Encoder (Maybe EpochState)  -- TODO-1: make combinator to build this

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

  record BlockInfo : Set where
    constructor BlockInfo∙new
    field
      _biEpoch           : Epoch
      _biRound           : Round
      _biId              : HashValue
      _biExecutedStateId : HashValue -- aka liTransactionAccumulatorHash
      _biVersion         : Version
      --, _biTimestamp       :: Instant
      _biNextEpochState  : Maybe EpochState
  open BlockInfo public
  unquoteDecl biEpoch   biRound   biId   biExecutedStateId   biVersion   biNextEpochState = mkLens (quote BlockInfo)
             (biEpoch ∷ biRound ∷ biId ∷ biExecutedStateId ∷ biVersion ∷ biNextEpochState ∷ [])
  postulate instance enc-BlockInfo : Encoder BlockInfo

  postulate
    _≟-BlockInfo_ : (bi1 bi2 : BlockInfo) → Dec (bi1 ≡ bi2)

  instance
    Eq-BlockInfo : Eq BlockInfo
    Eq._≟_ Eq-BlockInfo = _≟-BlockInfo_

  BlockInfo-η : ∀{e1 e2 r1 r2 i1 i2 x1 x2 v1 v2 n1 n2}
              → e1 ≡ e2 → r1 ≡ r2 → i1 ≡ i2 → x1 ≡ x2 → v1 ≡ v2 → n1 ≡ n2
              → BlockInfo∙new e1 r1 i1 x1 v1 n1 ≡ BlockInfo∙new e2 r2 i2 x2 v2 n2
  BlockInfo-η refl refl refl refl refl refl = refl

  instance
    Eq-ByteString : Eq ByteString
    Eq._≟_ Eq-ByteString = _≟ByteString_

{-
  _≟BlockInfo_ : (b₁ b₂ : BlockInfo) → Dec (b₁ ≡ b₂)
  l ≟BlockInfo r with ((l ^∙ biEpoch) ≟ (r ^∙ biEpoch))
  ...| no  no-e = no  λ where refl → no-e refl
  ...| yes refl with ((l ^∙ biRound)  ≟ (r ^∙ biRound))
  ...| no  no-r = no  λ where refl → no-r refl
  ...| yes refl with ((l ^∙ biId)     ≟ (r ^∙ biId))
  ...| no  no-i = no  λ where refl → no-i refl
  ...| yes refl = yes refl

  instance
    Eq-BlockInfo : Eq BlockInfo
    Eq._≟_ Eq-BlockInfo = _≟BlockInfo_

  BlockInfo-η : ∀{e1 e2 r1 r2 i1 i2} → e1 ≡ e2 → r1 ≡ r2 → i1 ≡ i2
              → BlockInfo∙new e1 r1 i1 ≡ BlockInfo∙new e2 r2 i2
  BlockInfo-η refl refl refl = refl
-}

  biNextBlockEpoch : Lens BlockInfo Epoch
  biNextBlockEpoch = mkLens' g s
   where
    g : BlockInfo → Epoch
    g bi = maybeS (bi ^∙ biNextEpochState)
                  (bi ^∙ biEpoch)
                  (  _^∙ esEpoch)
    s : BlockInfo → Epoch → BlockInfo
    s bi _ = bi -- TODO-1 : cannot be done: need a way to defined only getters

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

  record LedgerInfo : Set where
    constructor LedgerInfo∙new
    field
      _liCommitInfo        : BlockInfo
      _liConsensusDataHash : HashValue
  open LedgerInfo public
  unquoteDecl liCommitInfo   liConsensusDataHash = mkLens (quote LedgerInfo)
             (liCommitInfo ∷ liConsensusDataHash ∷ [])
  postulate instance enc-LedgerInfo : Encoder LedgerInfo
  postulate instance ws-LedgerInfo  : WithSig LedgerInfo

  -- GETTER only in Haskell
  liEpoch : Lens LedgerInfo Epoch
  liEpoch = liCommitInfo ∙ biEpoch

  -- GETTER only in Haskell
  liNextBlockEpoch : Lens LedgerInfo Epoch
  liNextBlockEpoch = liCommitInfo ∙ biNextBlockEpoch

  -- GETTER only in Haskell
  liConsensusBlockId : Lens LedgerInfo HashValue
  liConsensusBlockId = liCommitInfo ∙ biId

  -- GETTER only in Haskell
  liTransactionAccumulatorHash : Lens LedgerInfo HashValue
  liTransactionAccumulatorHash = liCommitInfo ∙ biExecutedStateId

  -- GETTER only in Haskell
  liVersion : Lens LedgerInfo Version
  liVersion = liCommitInfo ∙ biVersion

  -- GETTER only in Haskell
  liNextEpochState : Lens LedgerInfo (Maybe EpochState)
  liNextEpochState = mkLens' g s
   where
    g : LedgerInfo → Maybe EpochState
    g = (_^∙ liCommitInfo ∙ biNextEpochState)
    s : LedgerInfo → Maybe EpochState → LedgerInfo
    s l _ = l -- TODO-1 : cannot be done: need a way to defined only getters

  -- GETTER only in Haskell
  liEndsEpoch : Lens LedgerInfo Bool
  liEndsEpoch = mkLens' g s
   where
    g : LedgerInfo → Bool
    g = is-just ∘ (_^∙ liNextEpochState)
    s : LedgerInfo → Bool → LedgerInfo
    s l _ = l -- TODO-1 : cannot be done: need a way to defined only getters

  LedgerInfo-η : ∀ {ci1 ci2 : BlockInfo} {cdh1 cdh2 : Hash}
             → ci1  ≡ ci2
             → cdh1 ≡ cdh2
             → (LedgerInfo∙new ci1 cdh1) ≡ (LedgerInfo∙new ci2 cdh2)
  LedgerInfo-η refl refl = refl

  record LedgerInfoWithSignatures : Set where
    constructor LedgerInfoWithSignatures∙new
    field
      _liwsLedgerInfo : LedgerInfo
      _liwsSignatures : KVMap Author Signature
  open LedgerInfoWithSignatures public
  unquoteDecl liwsLedgerInfo   liwsSignatures = mkLens (quote LedgerInfoWithSignatures)
             (liwsLedgerInfo ∷ liwsSignatures ∷ [])
  postulate instance enc-LedgerInfoWithSignatures : Encoder LedgerInfoWithSignatures

  -- GETTER only in Haskell
  liwsEpoch : Lens LedgerInfoWithSignatures Epoch
  liwsEpoch = liwsLedgerInfo ∙ liEpoch

  -- GETTER only in Haskell
  liwsVersion : Lens LedgerInfoWithSignatures Version
  liwsVersion = liwsLedgerInfo ∙ liVersion

  -- GETTER only in Haskell
  liwsNextEpochState : Lens LedgerInfoWithSignatures (Maybe EpochState)
  liwsNextEpochState = liwsLedgerInfo ∙ liNextEpochState

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

  record Timeout : Set where
    constructor Timeout∙new
    field
      _toEpoch : Epoch
      _toRound : Round
  open Timeout public
  unquoteDecl toEpoch   toRound = mkLens (quote Timeout)
             (toEpoch ∷ toRound ∷ [])
  postulate instance enc-Timeout : Encoder Timeout

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

  record VoteData : Set where
    constructor VoteData∙new
    field
      _vdProposed : BlockInfo
      _vdParent   : BlockInfo
  open VoteData public
  unquoteDecl vdProposed   vdParent = mkLens (quote VoteData)
             (vdProposed ∷ vdParent ∷ [])
  postulate instance enc-VoteData : Encoder VoteData

  VoteData-η : ∀ {pr1 par1 pr2 par2 : BlockInfo} → pr1  ≡ pr2 → par1 ≡ par2
             → (VoteData∙new pr1 par1) ≡ (VoteData∙new pr2 par2)
  VoteData-η refl refl = refl

  -- DESIGN NOTE: The _vAuthor field is included only to facilitate lookup of the public key against
  -- which to verify the signature.  An alternative would be to use an index into the members of the
  -- epoch config, which would save message space and therefore bandwidth.
  record Vote : Set where
    constructor Vote∙new
    field
      _vVoteData         : VoteData
      _vAuthor           : Author
      _vLedgerInfo       : LedgerInfo
      _vSignature        : Signature
      _vTimeoutSignature : Maybe Signature
  open Vote public
  unquoteDecl vVoteData   vAuthor   vLedgerInfo   vSignature   vTimeoutSignature = mkLens (quote Vote)
             (vVoteData ∷ vAuthor ∷ vLedgerInfo ∷ vSignature ∷ vTimeoutSignature ∷ [])
  postulate instance enc-Vote     : Encoder Vote

  -- not defined in Haskell
  vParent : Lens Vote BlockInfo
  vParent = vVoteData ∙ vdParent

  -- not defined in Haskell
  vProposed : Lens Vote BlockInfo
  vProposed = vVoteData ∙ vdProposed

  -- not defined in Haskell
  vParentId : Lens Vote Hash
  vParentId = vVoteData ∙ vdParent ∙ biId

  -- not defined in Haskell
  vParentRound : Lens Vote Round
  vParentRound = vVoteData ∙ vdParent ∙ biRound

  -- not defined in Haskell
  vProposedId : Lens Vote Hash
  vProposedId = vVoteData ∙ vdProposed ∙ biId

  -- getter only in Haskell
  vEpoch : Lens Vote Epoch
  vEpoch = vVoteData ∙ vdProposed ∙ biEpoch

  -- getter only in Haskell
  vRound : Lens Vote Round
  vRound = vVoteData ∙ vdProposed ∙ biRound

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

  record QuorumCert : Set where
    constructor QuorumCert∙new
    field
      _qcVoteData         : VoteData
      _qcSignedLedgerInfo : LedgerInfoWithSignatures
  open QuorumCert public
  unquoteDecl qcVoteData   qcSignedLedgerInfo = mkLens (quote QuorumCert)
             (qcVoteData ∷ qcSignedLedgerInfo ∷ [])
  postulate instance enc-QuorumCert : Encoder QuorumCert

  -- Because QuorumCert has an injective encoding (postulated, for now),
  -- we can use it to determine equality of QuorumCerts.
  _≟QC_ : (q1 q2 : QuorumCert) → Dec (q1 ≡ q2)
  _≟QC_ = ≡-Encoder enc-QuorumCert

  _QCBoolEq_ : QuorumCert → QuorumCert → Bool
  _QCBoolEq_ q1 q2 = does (q1 ≟QC q2)

  -- getter only in Haskell
  qcCertifiedBlock : Lens QuorumCert BlockInfo
  qcCertifiedBlock = qcVoteData ∙ vdProposed

  -- getter only in Haskell
  qcParentBlock : Lens QuorumCert BlockInfo
  qcParentBlock = qcVoteData ∙ vdParent

  -- getter only in Haskell
  qcLedgerInfo : Lens QuorumCert LedgerInfoWithSignatures
  qcLedgerInfo = qcSignedLedgerInfo

  -- getter only in Haskell
  qcCommitInfo : Lens QuorumCert BlockInfo
  qcCommitInfo = qcSignedLedgerInfo ∙ liwsLedgerInfo ∙ liCommitInfo

  -- getter only in Haskell
  qcEndsEpoch : Lens QuorumCert Bool
  qcEndsEpoch = mkLens' g s
   where
    g : QuorumCert → Bool
    g q = is-just (q ^∙ qcSignedLedgerInfo ∙ liwsLedgerInfo ∙ liNextEpochState)

    s : QuorumCert → Bool → QuorumCert
    s q _ = q -- TODO-1 : cannot be done: need a way to defined only getters

  -- Constructs a 'vote' that was gathered in a QC.
  rebuildVote : QuorumCert → Author × Signature → Vote
  rebuildVote qc (α , sig)
    = record { _vVoteData         = _qcVoteData qc
             ; _vAuthor           = α
             ; _vLedgerInfo       = qc ^∙ (qcSignedLedgerInfo ∙ liwsLedgerInfo)
             ; _vSignature        = sig
             ; _vTimeoutSignature = nothing -- Is this correct?  The original vote may have had a
                                            -- timeout signature, but we don't know.  Does it
                                            -- matter?
             }

  -- Two votes are equivalent if they are identical except they may differ on timeout signature
  _≈Vote_ : (v1 v2 : Vote) → Set
  v1 ≈Vote v2 = v2 ≡ record v1 { _vTimeoutSignature = _vTimeoutSignature v2 }

  qcVotesKV : QuorumCert → KVMap Author Signature
  qcVotesKV = _liwsSignatures ∘ _qcSignedLedgerInfo

  qcVotes : QuorumCert → List (Author × Signature)
  qcVotes qc = kvm-toList (qcVotesKV qc)

  -- not defined in Haskell
  qcCertifies : Lens QuorumCert  Hash
  qcCertifies = qcVoteData ∙ vdProposed ∙ biId

  -- not defined in Haskell
  qcRound : Lens QuorumCert Round
  qcRound = qcVoteData ∙ vdProposed ∙ biRound

  _qcCertifies : QuorumCert → Hash
  _qcCertifies q = q ^∙ qcCertifies

  _qcRound : QuorumCert → Round
  _qcRound q = q ^∙ qcRound

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

  record TimeoutCertificate : Set where
    constructor mkTimeoutCertificate
    field
      _tcTimeout    : Timeout
      _tcSignatures : KVMap Author Signature
  open TimeoutCertificate public
  unquoteDecl tcTimeout   tcSignatures = mkLens (quote TimeoutCertificate)
             (tcTimeout ∷ tcSignatures ∷ [])

  TimeoutCertificate∙new : Timeout → TimeoutCertificate
  TimeoutCertificate∙new to = mkTimeoutCertificate to Map.empty

  -- getter only in haskell
  tcEpoch : Lens TimeoutCertificate Epoch
  tcEpoch = tcTimeout ∙ toEpoch

  -- getter only in haskell
  tcRound : Lens TimeoutCertificate Round
  tcRound = tcTimeout ∙ toRound

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

  data BlockType : Set where
    Proposal : TX → Author → BlockType
    NilBlock : BlockType
    Genesis  : BlockType
  postulate instance enc-BlockType : Encoder BlockType

  postulate -- Valid assumption, payloadIsEmpty
    -- TODO-1 : Need to decide what empty means.
    --          Only important on epoch change.
    payloadIsEmpty : TX → Bool

  _≟BlockType_ : (b₁ b₂ : BlockType) → Dec (b₁ ≡ b₂)
  Genesis          ≟BlockType Genesis          = true because ofʸ refl
  NilBlock         ≟BlockType NilBlock         = true because ofʸ refl
  (Proposal t₁ a₁) ≟BlockType (Proposal t₂ a₂) with t₁ ≟ t₂
  ...| no  no-t = no λ where refl → no-t refl
  ...| yes refl with a₁ ≟ a₂
  ...| no  no-a = no λ where refl → no-a refl
  ...| yes refl = yes refl
  Genesis          ≟BlockType NilBlock       = no (λ ())
  Genesis          ≟BlockType (Proposal _ _) = no (λ ())
  NilBlock         ≟BlockType Genesis        = no (λ ())
  NilBlock         ≟BlockType (Proposal _ _) = no (λ ())
  (Proposal _ _)   ≟BlockType Genesis        = no (λ ())
  (Proposal _ _)   ≟BlockType NilBlock       = no (λ ())

  instance
    Eq-BlockType : Eq BlockType
    Eq._≟_ Eq-BlockType = _≟BlockType_

  record BlockData : Set where
    constructor BlockData∙new
    field
      _bdEpoch      : Epoch
      _bdRound      : Round
      -- QUESTION: How do we represent a block that extends the
      -- genesis block, which doesn't come with a QC.  Maybe the
      -- genesis block has an associated QC established for the epoch?
      _bdQuorumCert : QuorumCert
      _bdBlockType  : BlockType
  open BlockData public
  unquoteDecl bdEpoch   bdRound   bdQuorumCert   bdBlockType = mkLens (quote BlockData)
             (bdEpoch ∷ bdRound ∷ bdQuorumCert ∷ bdBlockType ∷ [])
  postulate instance enc-BlockData : Encoder BlockData

  -- not defined in Haskell
  bdParentId : Lens BlockData Hash
  bdParentId = bdQuorumCert ∙ qcVoteData ∙ vdParent ∙ biId

  -- not defined in Haskell
  -- This is the id of a block
  bdBlockId : Lens BlockData Hash
  bdBlockId = bdQuorumCert ∙ qcVoteData ∙ vdProposed ∙ biId

  -- getter only in Haskell
  bdAuthor : Lens BlockData (Maybe Author)
  bdAuthor = mkLens' g s
    where
    g : BlockData → Maybe Author
    g bd = case (bd ^∙ bdBlockType) of λ where
             (Proposal _ author) → just author
             _                   → nothing

    s : BlockData → Maybe Author → BlockData
    s bd nothing     = bd
    s bd (just auth) =
      bd & bdBlockType %~ λ where
        (Proposal tx _) → Proposal tx auth
        bdt → bdt

  -- getter only in Haskell
  bdPayload : Lens BlockData (Maybe TX)
  bdPayload = mkLens' g s
    where
    g : BlockData → Maybe TX
    g bd = case bd ^∙ bdBlockType of λ where
             (Proposal a _) → just a
             _              → nothing

    s : BlockData → Maybe TX → BlockData
    s bd _ = bd -- TODO-1 : cannot be done: need a way to define only getters

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

  -- The signature is a Maybe to allow us to use 'nothing' as the
  -- 'bSignature' when constructing a block to sign later.  Also,
  -- "nil" blocks are not signed because they are produced
  -- independently by different validators.  This is to enable
  -- committing after an epoch-changing command is processed: we
  -- cannot add more commands, but we need to add some quorum
  -- certificates in order to commit the epoch-changing command.
  record Block : Set where
    constructor Block∙new
    field
      _bId        : HashValue
      _bBlockData : BlockData
      _bSignature : Maybe Signature
  open Block public
  unquoteDecl bId   bBlockData   bSignature = mkLens (quote Block)
             (bId ∷ bBlockData ∷ bSignature ∷ [])

  postulate instance enc : Encoder Block

  -- getter only in Haskell
  bAuthor : Lens Block (Maybe Author)
  bAuthor = bBlockData ∙ bdAuthor

  -- getter only in Haskell
  bEpoch : Lens Block Epoch
  bEpoch = bBlockData ∙ bdEpoch

  -- getter only in Haskell
  bRound : Lens Block Round
  bRound = bBlockData ∙ bdRound

  -- getter only in Haskell
  bQuorumCert : Lens Block QuorumCert
  bQuorumCert  = bBlockData ∙ bdQuorumCert

  -- getter only in Haskell
  bParentId : Lens Block HashValue
  bParentId = bQuorumCert ∙ qcCertifiedBlock ∙ biId

  -- getter only in Haskell
  bPayload : Lens Block (Maybe TX)
  bPayload = bBlockData ∙ bdPayload

  bdQcSigs : Lens Block (KVMap Author Signature)
  bdQcSigs = bBlockData ∙ bdQuorumCert ∙ qcLedgerInfo ∙ liwsSignatures

  -- Equivalence of Blocks modulo signatures (both on the Block and in the QuorumCert it contains)
  infix 4 _≈Block_
  _≈Block_ : (b₁ b₂ : Block) → Set
  b₁ ≈Block b₂ = b₁ ≡ (b₂ & bSignature ∙~ (b₁ ^∙ bSignature)
                          & bdQcSigs   ∙~ (b₁ ^∙ bdQcSigs))

  sym≈Block : Symmetric _≈Block_
  sym≈Block refl = refl

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

  record AccumulatorExtensionProof : Set where
    constructor AccumulatorExtensionProof∙new
    field
      _aepObmNumLeaves : Version
  open AccumulatorExtensionProof public
  unquoteDecl aepObmNumLeaves = mkLens (quote AccumulatorExtensionProof)
             (aepObmNumLeaves ∷ [])

  record VoteProposal : Set where
    constructor VoteProposal∙new
    field
      _vpAccumulatorExtensionProof : AccumulatorExtensionProof
      _vpBlock : Block
      _vpNextEpochState : Maybe EpochState
  open VoteProposal public
  unquoteDecl  vpAccumulatorExtensionProof   vpBlock   vpNextEpochState = mkLens (quote VoteProposal)
              (vpAccumulatorExtensionProof ∷ vpBlock ∷ vpNextEpochState ∷ [])

  record MaybeSignedVoteProposal : Set where
    constructor MaybeSignedVoteProposal∙new
    field
      _msvpVoteProposal : VoteProposal
  open MaybeSignedVoteProposal public
  unquoteDecl  msvpVoteProposal = mkLens (quote MaybeSignedVoteProposal)
              (msvpVoteProposal ∷ [])

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

  record LastVoteInfo : Set where
    constructor LastVoteInfo∙new
    field
      _lviLiDigest  : HashValue
      _lviRound     : Round
      _lviIsTimeout : Bool
  open LastVoteInfo public

  record PendingVotes : Set where
    constructor mkPendingVotes
    field
      _pvLiDigestToVotes   : KVMap HashValue LedgerInfoWithSignatures
      _pvMaybePartialTC    : Maybe TimeoutCertificate
      _pvAuthorToVote      : KVMap Author Vote
  open PendingVotes public
  unquoteDecl pvLiDigestToVotes   pvMaybePartialTC   pvAuthorToVote = mkLens (quote PendingVotes)
             (pvLiDigestToVotes ∷ pvMaybePartialTC ∷ pvAuthorToVote ∷ [])

  PendingVotes∙new : PendingVotes
  PendingVotes∙new = mkPendingVotes Map.empty nothing Map.empty

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

  record StateComputeResult : Set where
    constructor StateComputeResult∙new
    field
      _scrObmNumLeaves : Version
      _scrEpochState   : Maybe EpochState
  open StateComputeResult public
  unquoteDecl scrObmNumLeaves   scrEpochState = mkLens (quote StateComputeResult)
             (scrObmNumLeaves ∷ scrEpochState ∷ [])

  postulate -- TODO: eliminate after fully implementing executeBlockE
    stateComputeResult : StateComputeResult

  record ExecutedBlock : Set where
    constructor ExecutedBlock∙new
    field
      _ebBlock              : Block
      _ebStateComputeResult : StateComputeResult
  open ExecutedBlock public
  unquoteDecl ebBlock   ebStateComputeResult = mkLens (quote ExecutedBlock)
             (ebBlock ∷ ebStateComputeResult ∷ [])

  -- getter only in Haskell
  ebId : Lens ExecutedBlock HashValue
  ebId = ebBlock ∙ bId

  -- getter only in Haskell
  ebQuorumCert : Lens ExecutedBlock QuorumCert
  ebQuorumCert = ebBlock ∙ bQuorumCert

  -- getter only in Haskell
  ebParentId : Lens ExecutedBlock HashValue
  ebParentId = ebQuorumCert ∙ qcCertifiedBlock ∙ biId

  -- getter only in Haskell
  ebRound : Lens ExecutedBlock Round
  ebRound = ebBlock ∙ bRound

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

  record LinkableBlock : Set where
    constructor LinkableBlock∙new
    field
      _lbExecutedBlock : ExecutedBlock
      -- _lbChildren      : Set HashValue
  open LinkableBlock public
  unquoteDecl lbExecutedBlock = mkLens (quote LinkableBlock)
             (lbExecutedBlock ∷ [])

  -- getter only in Haskell
  lbId : Lens LinkableBlock HashValue
  lbId = lbExecutedBlock ∙ ebId

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

  -- A block tree depends on a epoch config but works regardlesss of which
  -- EpochConfig we have.
  record BlockTree : Set where
    constructor mkBlockTree
    field
      _btIdToBlock               : KVMap HashValue LinkableBlock
      _btRootId                  : HashValue
      _btHighestCertifiedBlockId : HashValue
      _btHighestQuorumCert       : QuorumCert
      _btHighestTimeoutCert      : Maybe TimeoutCertificate
      _btHighestCommitCert       : QuorumCert
      _btIdToQuorumCert          : KVMap HashValue QuorumCert
      _btPrunedBlockIds          : VecDeque
      _btMaxPrunedBlocksInMem    : ℕ
  open BlockTree public
  unquoteDecl btIdToBlock   btRootId  btHighestCertifiedBlockId   btHighestQuorumCert
              btHighestTimeoutCert   btHighestCommitCert
              btIdToQuorumCert   btPrunedBlockIds
              btMaxPrunedBlocksInMem = mkLens (quote BlockTree)
             (btIdToBlock ∷ btRootId ∷ btHighestCertifiedBlockId ∷ btHighestQuorumCert ∷
              btHighestTimeoutCert ∷ btHighestCommitCert ∷
              btIdToQuorumCert ∷ btPrunedBlockIds ∷
              btMaxPrunedBlocksInMem ∷ [])

  btGetLinkableBlock : HashValue → BlockTree → Maybe LinkableBlock
  btGetLinkableBlock hv bt = Map.lookup hv (bt ^∙ btIdToBlock)

  btGetBlock : HashValue → BlockTree → Maybe ExecutedBlock
  btGetBlock hv bt = (_^∙ lbExecutedBlock) <$> btGetLinkableBlock hv bt

  -- getter only in Haskell
  btRoot : Lens BlockTree (Maybe ExecutedBlock)
  btRoot = mkLens' g s
    where
    g : BlockTree → Maybe ExecutedBlock
    g bt = btGetBlock (bt ^∙ btRootId) bt

    -- TODO-1 : the setter is not needed/defined in Haskell
    -- Defining it just to make progress, but it can't be defined
    -- correctly in terms of type correctness (let alone setting a new root!)
    s : BlockTree → Maybe ExecutedBlock → BlockTree
    s bt _ = bt -- TODO-1 : cannot be done: need a way to defined only getters

  -- getter only in haskell
  btHighestCertifiedBlock : Lens BlockTree (Maybe ExecutedBlock)
  btHighestCertifiedBlock = mkLens' g s
    where
    g : BlockTree → (Maybe ExecutedBlock)
    g bt = btGetBlock (bt ^∙ btHighestCertifiedBlockId) bt

    s : BlockTree → (Maybe ExecutedBlock) → BlockTree
    s bt _ = bt -- TODO-1 : cannot be done: need a way to defined only getters

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

  record LedgerStore : Set where
    constructor mkLedgerStore
    field
      _lsObmVersionToEpoch : Map.KVMap Version Epoch
      _lsObmEpochToLIWS    : Map.KVMap Epoch   LedgerInfoWithSignatures
      _lsLatestLedgerInfo  : Maybe LedgerInfoWithSignatures
  open LedgerStore public
  unquoteDecl lsObmVersionToEpoch   lsObmEpochToLIWS   lsLatestLedgerInfo = mkLens (quote LedgerStore)
             (lsObmVersionToEpoch ∷ lsObmEpochToLIWS ∷ lsLatestLedgerInfo ∷ [])

  record DiemDB : Set where
    constructor DiemDB∙new
    field
      _ddbLedgerStore : LedgerStore
  open DiemDB public
  unquoteDecl ddbLedgerStore = mkLens (quote DiemDB)
             (ddbLedgerStore ∷ [])

  record LedgerRecoveryData : Set where
    constructor LedgerRecoveryData∙new
    field
      _lrdStorageLedger : LedgerInfo

  record MockSharedStorage : Set where
    constructor mkMockSharedStorage
    field
      -- Safety state
      _mssBlock                     : Map.KVMap HashValue Block
      _mssQc                        : Map.KVMap HashValue QuorumCert
      _mssLis                       : Map.KVMap Version   LedgerInfoWithSignatures
      _mssLastVote                  : Maybe Vote
      -- Liveness state
      _mssHighestTimeoutCertificate : Maybe TimeoutCertificate
      _mssValidatorSet              : ValidatorSet
  open MockSharedStorage public
  unquoteDecl mssBlock    mssQc   mssLis    mssLastVote
              mssHighestTimeoutCertificate  mssValidatorSet = mkLens (quote MockSharedStorage)
             (mssBlock ∷  mssQc ∷ mssLis ∷ mssLastVote ∷
              mssHighestTimeoutCertificate ∷ mssValidatorSet ∷ [])

  record MockStorage : Set where
    constructor MockStorage∙new
    field
      _msSharedStorage : MockSharedStorage
      _msStorageLedger : LedgerInfo
      _msObmDiemDB     : DiemDB
  open MockStorage public
  unquoteDecl msSharedStorage   msStorageLedger   msObmDiemDB = mkLens (quote MockStorage)
             (msSharedStorage ∷ msStorageLedger ∷ msObmDiemDB ∷ [])

  PersistentLivenessStorage = MockStorage

  -- IMPL-DIFF : This is defined without record fields in Haskell.
  -- The record fields below are never used.  But RootInfo must be a record for pattern matching.
  record RootInfo : Set where
    constructor RootInfo∙new
    field
      _riBlock : Block
      _riQC1   : QuorumCert
      _riQC2   : QuorumCert

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

  record SafetyData : Set where
    constructor SafetyData∙new
    field
      _sdEpoch          : Epoch
      _sdLastVotedRound : Round
      _sdPreferredRound : Round
      _sdLastVote       : Maybe Vote
  open SafetyData public
  unquoteDecl sdEpoch sdLastVotedRound sdPreferredRound sdLastVote =
    mkLens (quote SafetyData)
    (sdEpoch ∷ sdLastVotedRound ∷ sdPreferredRound ∷ sdLastVote ∷  [])

  record Waypoint : Set where
    constructor Waypoint∙new
    field
      _wVersion : Version
      _wValue   : HashValue
  open Waypoint public
  unquoteDecl wVersion   wValue = mkLens (quote Waypoint)
             (wVersion ∷ wValue ∷ [])
  postulate instance enc-Waypoint : Encoder Waypoint

  record PersistentSafetyStorage : Set where
    constructor mkPersistentSafetyStorage
    field
      _pssSafetyData : SafetyData
      _pssAuthor     : Author
      _pssWaypoint   : Waypoint
      _pssObmSK      : Maybe SK
  open PersistentSafetyStorage public
  unquoteDecl pssSafetyData   pssAuthor   pssWaypoint   pssObmSK = mkLens (quote PersistentSafetyStorage)
             (pssSafetyData ∷ pssAuthor ∷ pssWaypoint ∷ pssObmSK ∷ [])

  record OnChainConfigPayload : Set where
    constructor OnChainConfigPayload∙new
    field
      _occpEpoch           : Epoch
      _occpObmValidatorSet : ValidatorSet
  open OnChainConfigPayload public
  unquoteDecl occpEpoch   occpObmValidatorSet = mkLens (quote OnChainConfigPayload)
             (occpEpoch ∷ occpObmValidatorSet ∷ [])
  -- instance S.Serialize OnChainConfigPayload

  record ReconfigEventEpochChange : Set where
    constructor ReconfigEventEpochChange∙new
    field
      _reecOnChainConfigPayload : OnChainConfigPayload
  -- instance S.Serialize ReconfigEventEpochChange

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

  -- IMPL-DIFF : Haskell StateComputer has pluggable functions.
  -- The Agda version just calls them directly
  record StateComputer : Set where
    constructor StateComputer∙new
    field
      _scObmVersion : Version
  open StateComputer public
  unquoteDecl scObmVersion = mkLens (quote StateComputer)
             (scObmVersion ∷ [])

  StateComputerComputeType
    = StateComputer → Block → HashValue
    → Either (List String) StateComputeResult

  StateComputerCommitType
    = StateComputer → DiemDB → ExecutedBlock → LedgerInfoWithSignatures
    → Either (List String) (StateComputer × DiemDB × Maybe ReconfigEventEpochChange)

  StateComputerSyncToType
    = LedgerInfoWithSignatures
    → Either (List String) ReconfigEventEpochChange

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

  record BlockStore : Set where
    constructor BlockStore∙new
    field
      _bsInner         : BlockTree
      _bsStateComputer : StateComputer
      _bsStorage       : PersistentLivenessStorage
  open BlockStore public
  unquoteDecl bsInner   bsStateComputer   bsStorage = mkLens (quote BlockStore)
             (bsInner ∷ bsStateComputer ∷ bsStorage ∷ [])

  postulate  -- TODO: stateComputer
    stateComputer : StateComputer

  -- getter only in Haskell
  bsRoot : Lens BlockStore (Maybe ExecutedBlock)
  bsRoot = bsInner ∙ btRoot

  -- getter only in Haskell
  bsHighestQuorumCert : Lens BlockStore QuorumCert
  bsHighestQuorumCert = bsInner ∙ btHighestQuorumCert

  -- getter only in Haskell
  bsHighestCommitCert : Lens BlockStore QuorumCert
  bsHighestCommitCert = bsInner ∙ btHighestCommitCert

  -- getter only in Haskell
  bsHighestTimeoutCert : Lens BlockStore (Maybe TimeoutCertificate)
  bsHighestTimeoutCert = bsInner ∙ btHighestTimeoutCert

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

  data NewRoundReason : Set where
    QCReady : NewRoundReason
    TOReady : NewRoundReason

  record NewRoundEvent : Set where
    constructor NewRoundEvent∙new
    field
      _nreRound   : Round
      _nreReason  : NewRoundReason
      _nreTimeout : Duration
  unquoteDecl nreRound   nreReason   nreTimeout = mkLens (quote NewRoundEvent)
             (nreRound ∷ nreReason ∷ nreTimeout ∷ [])

-- LibraBFT.ImplShared.Consensus.Types contains
-- ExponentialTimeInterval, RoundState

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

  record ProposalGenerator : Set where
    constructor ProposalGenerator∙new
    field
      _pgLastRoundGenerated : Round
  open ProposalGenerator
  unquoteDecl pgLastRoundGenerated = mkLens (quote ProposalGenerator)
             (pgLastRoundGenerated ∷ [])

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

  data ObmNotValidProposerReason : Set where
    ProposalDoesNotHaveAnAuthor ProposerForBlockIsNotValidForThisRound NotValidProposer : ObmNotValidProposerReason

  record ProposerElection : Set where
    constructor ProposerElection∙new
    field
      _peProposers : List Author -- TODO-1 : this should be 'Set Author'
      -- _peObmLeaderOfRound : LeaderOfRoundFn
      -- _peObmNodesInOrder  : NodesInOrder
  open ProposerElection

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

  record SafetyRules : Set where
    constructor mkSafetyRules
    field
      _srPersistentStorage  : PersistentSafetyStorage
      _srExportConsensusKey : Bool
      _srValidatorSigner    : Maybe ValidatorSigner
      _srEpochState         : Maybe EpochState
  open SafetyRules public
  unquoteDecl srPersistentStorage   srExportConsensusKey   srValidatorSigner   srEpochState = mkLens (quote SafetyRules)
             (srPersistentStorage ∷ srExportConsensusKey ∷ srValidatorSigner ∷ srEpochState ∷ [])

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

  record BlockRetrievalRequest : Set where
    constructor BlockRetrievalRequest∙new
    field
      _brqObmFrom   : Author
      _brqBlockId   : HashValue
      _brqNumBlocks : U64
  open BlockRetrievalRequest public
  unquoteDecl brqObmFrom   brqBlockId   brqNumBlocks = mkLens (quote BlockRetrievalRequest)
             (brqObmFrom ∷ brqBlockId ∷ brqNumBlocks ∷ [])
  postulate instance enc-BlockRetrievalRequest : Encoder BlockRetrievalRequest

  data BlockRetrievalStatus : Set where
    BRSSucceeded BRSIdNotFound BRSNotEnoughBlocks : BlockRetrievalStatus
  open BlockRetrievalStatus public
  postulate instance enc-BlockRetrievalState : Encoder BlockRetrievalStatus

  brs-eq : (brs₁ brs₂ : BlockRetrievalStatus) → Dec (brs₁ ≡ brs₂)
  brs-eq BRSSucceeded       BRSSucceeded       = yes refl
  brs-eq BRSSucceeded       BRSIdNotFound      = no λ ()
  brs-eq BRSSucceeded       BRSNotEnoughBlocks = no λ ()
  brs-eq BRSIdNotFound      BRSSucceeded       = no λ ()
  brs-eq BRSIdNotFound      BRSIdNotFound      = yes refl
  brs-eq BRSIdNotFound      BRSNotEnoughBlocks = no λ ()
  brs-eq BRSNotEnoughBlocks BRSSucceeded       = no λ ()
  brs-eq BRSNotEnoughBlocks BRSIdNotFound      = no λ ()
  brs-eq BRSNotEnoughBlocks BRSNotEnoughBlocks = yes refl

  instance
    Eq-BlockRetrievalStatus : Eq BlockRetrievalStatus
    Eq._≟_ Eq-BlockRetrievalStatus = brs-eq

  record BlockRetrievalResponse : Set where
    constructor BlockRetrievalResponse∙new
    field
      _brpObmFrom : (Author × Epoch × Round) -- for logging
      _brpStatus  : BlockRetrievalStatus
      _brpBlocks  : List Block
  unquoteDecl brpObmFrom   brpStatus   brpBlocks   = mkLens (quote BlockRetrievalResponse)
             (brpObmFrom ∷ brpStatus ∷ brpBlocks ∷ [])
  postulate instance enc-BlockRetrievalResponse : Encoder BlockRetrievalResponse

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

-- LibraBFT.ImplShared.Consensus.Types contains
-- ObmNeedFetch, RoundManager

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

  record BlockRetriever : Set where
    constructor BlockRetriever∙new
    field
      _brDeadline      : Instant
      _brPreferredPeer : Author
  open BlockRetriever public
  unquoteDecl brDeadline   brPreferredPeer = mkLens (quote BlockRetriever)
             (brDeadline ∷ brPreferredPeer ∷ [])

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

  record SyncInfo : Set where
    constructor mkSyncInfo -- Bare constructor to enable pattern matching against SyncInfo; "smart"
                           -- constructor SyncInfo∙new is below
    field
      _siHighestQuorumCert  : QuorumCert
      _sixxxHighestCommitCert  : Maybe QuorumCert
      _siHighestTimeoutCert : Maybe TimeoutCertificate
  open SyncInfo public
  -- Note that we do not automatically derive a lens for siHighestCommitCert;
  -- it is defined manually below.
  unquoteDecl siHighestQuorumCert   sixxxHighestCommitCert   siHighestTimeoutCert = mkLens (quote SyncInfo)
             (siHighestQuorumCert ∷ sixxxHighestCommitCert ∷ siHighestTimeoutCert ∷ [])
  postulate instance enc-SyncInfo : Encoder SyncInfo

  SyncInfo∙new : QuorumCert → QuorumCert → Maybe TimeoutCertificate → SyncInfo
  SyncInfo∙new highestQuorumCert highestCommitCert highestTimeoutCert =
    record { _siHighestQuorumCert    = highestQuorumCert
           ; _sixxxHighestCommitCert = if highestQuorumCert QCBoolEq highestCommitCert
                                       then nothing else (just highestCommitCert)
           ; _siHighestTimeoutCert   = highestTimeoutCert }

  -- getter only in Haskell
  siHighestCommitCert : Lens SyncInfo QuorumCert
  siHighestCommitCert =
    mkLens' (λ x → fromMaybe (x ^∙ siHighestQuorumCert) (x ^∙ sixxxHighestCommitCert))
            (λ x qc → record x { _sixxxHighestCommitCert = just qc })

  -- getter only in Haskell
  siHighestCertifiedRound : Lens SyncInfo Round
  siHighestCertifiedRound = siHighestQuorumCert ∙ qcCertifiedBlock ∙ biRound

  -- getter only in Haskell
  siHighestTimeoutRound : Lens SyncInfo Round
  siHighestTimeoutRound =
    mkLens' (maybe 0 (_^∙ tcRound) ∘ (_^∙ siHighestTimeoutCert))
            (λ x _r → x) -- TODO-1

  -- getter only in Haskell
  siHighestCommitRound : Lens SyncInfo Round
  siHighestCommitRound = siHighestCommitCert ∙ qcCommitInfo ∙ biRound

  -- getter only in Haskell
  siHighestRound : Lens SyncInfo Round
  siHighestRound =
    mkLens' (λ x → (x ^∙ siHighestCertifiedRound) ⊔ (x ^∙ siHighestTimeoutRound))
            (λ x _r → x) -- TODO-1

  -- getter only in Haskell
  siEpoch : Lens SyncInfo Epoch
  siEpoch  = siHighestQuorumCert ∙ qcCertifiedBlock ∙ biEpoch

  -- getter only in Haskell
  siObmRound : Lens SyncInfo Round
  siObmRound = siHighestQuorumCert ∙ qcCertifiedBlock ∙ biRound

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

  record ProposalMsg : Set where
    constructor ProposalMsg∙new
    field
      _pmProposal : Block
      _pmSyncInfo : SyncInfo
  open ProposalMsg public
  unquoteDecl pmProposal   pmSyncInfo = mkLens (quote ProposalMsg)
             (pmProposal ∷ pmSyncInfo ∷ [])
  postulate instance enc-ProposalMsg : Encoder ProposalMsg

  -- getter only in Haskell
  pmEpoch : Lens ProposalMsg Epoch
  pmEpoch = pmProposal ∙ bEpoch

  -- getter only in Haskell
  pmRound : Lens ProposalMsg Round
  pmRound = pmProposal ∙ bRound

  -- getter only in Haskell
  pmProposer : Lens ProposalMsg (Maybe Author)
  pmProposer = pmProposal ∙ bAuthor

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

  record VoteMsg : Set where
    constructor  VoteMsg∙new
    field
      _vmVote     : Vote
      _vmSyncInfo : SyncInfo
  open VoteMsg public
  unquoteDecl vmVote   vmSyncInfo = mkLens (quote VoteMsg)
             (vmVote ∷ vmSyncInfo ∷ [])
  postulate instance enc-VoteMsg : Encoder VoteMsg

  -- not defined in Haskell
  vmProposed : Lens VoteMsg BlockInfo
  vmProposed = vmVote ∙ vVoteData ∙ vdProposed

  -- not defined in Haskell
  vmParent : Lens VoteMsg BlockInfo
  vmParent = vmVote ∙ vVoteData ∙ vdParent

  -- getter-only in Haskell
  vmEpoch : Lens VoteMsg Epoch
  vmEpoch = vmVote ∙ vEpoch

  -- getter-only in Haskell
  vmRound : Lens VoteMsg Round
  vmRound = vmVote ∙ vRound

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

  -- This is a notification of a commit.  It may not be explicitly included in an implementation,
  -- but we need something to be able to express correctness conditions.  It will
  -- probably have something different in it, but will serve the purpose for now.
  record CommitMsg : Set where
    constructor CommitMsg∙new
    field
      _cmEpoch   : Epoch
      _cmAuthor  : NodeId
      _cmRound   : Round
      _cmCert    : QuorumCert  -- We assume for now that a CommitMsg contains the QuorumCert of the head of the 3-chain
      _cmSigMB   : Maybe Signature
  open CommitMsg public
  unquoteDecl cmEpoch   cmAuthor   cmRound   cmCert   cmSigMB = mkLens (quote CommitMsg)
             (cmEpoch ∷ cmAuthor ∷ cmRound ∷ cmCert ∷ cmSigMB ∷ [])
  postulate instance enc-CommitMsg : Encoder CommitMsg

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

  data RootMetadata : Set where RootMetadata∙new : RootMetadata

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

  record RecoveryData : Set where
    constructor mkRecoveryData
    field
      _rdLastVote                  : Maybe Vote
      _rdRoot                      : RootInfo
      _rdRootMetadata              : RootMetadata
      _rdBlocks                    : List Block
      _rdQuorumCerts               : List QuorumCert
      _rdBlocksToPrune             : Maybe (List HashValue)
      _rdHighestTimeoutCertificate : Maybe TimeoutCertificate
  open RecoveryData public
  unquoteDecl rdLastVote      rdRoot            rdRootMetadata                rdBlocks
              rdQuorumCerts   rdBlocksToPrune   rdHighestTimeoutCertificate = mkLens (quote RecoveryData)
             (rdLastVote    ∷ rdRoot          ∷ rdRootMetadata              ∷ rdBlocks ∷
              rdQuorumCerts ∷ rdBlocksToPrune ∷ rdHighestTimeoutCertificate ∷ [])

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

  record EpochChangeProof : Set where
    constructor EpochChangeProof∙new
    field
      _ecpLedgerInfoWithSigs : List LedgerInfoWithSignatures
      _ecpMore               : Bool
  open EpochChangeProof public
  unquoteDecl ecpLedgerInfoWithSigs   ecpMore = mkLens (quote EpochChangeProof)
             (ecpLedgerInfoWithSigs ∷ ecpMore ∷ [])
  -- instance S.Serialize EpochChangeProof

  record Ledger2WaypointConverter : Set where
    constructor mkLedger2WaypointConverter
    field
      _l2wcEpoch          : Epoch
      _l2wcRootHash       : HashValue
      _l2wcVersion        : Version
    --_l2wcTimestamp      : Instant
      _l2wcNextEpochState : Maybe EpochState
  open Ledger2WaypointConverter public
  unquoteDecl l2wcEpoch   2wcRootHash   2wcVersion
              {-l2wcTimestamp-} l2wcNextEpochState = mkLens (quote Ledger2WaypointConverter)
             (l2wcEpoch ∷ 2wcRootHash ∷ 2wcVersion ∷
              {-l2wcTimestamp-} l2wcNextEpochState ∷ [])

  record EpochRetrievalRequest : Set where
    constructor EpochRetrievalRequest∙new
    field
      _eprrqStartEpoch : Epoch
      _eprrqEndEpoch   : Epoch
  unquoteDecl eprrqStartEpoch   eprrqEndEpoch   = mkLens (quote EpochRetrievalRequest)
             (eprrqStartEpoch ∷ eprrqEndEpoch ∷ [])
  -- instance S.Serialize EpochRetrievalRequest

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

  record ConsensusState : Set where
    constructor ConsensusState∙new
    field
      _csSafetyData     : SafetyData
      _csWaypoint       : Waypoint
    --_csInValidatorSet : Bool -- LBFT-OBM-DIFF: only used in tests in Rust
  open ConsensusState public
  unquoteDecl csSafetyData   csWaypoint   {-csInValidatorSet-} = mkLens (quote ConsensusState)
             (csSafetyData ∷ csWaypoint {-∷ csInValidatorSet-} ∷ [])

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

  data SafetyRulesWrapper : Set where
    SRWLocal : SafetyRules → SafetyRulesWrapper

  record SafetyRulesManager : Set where
    constructor mkSafetyRulesManager
    field
      _srmInternalSafetyRules : SafetyRulesWrapper
  open SafetyRulesWrapper public
  unquoteDecl srmInternalSafetyRules = mkLens  (quote SafetyRulesManager)
             (srmInternalSafetyRules ∷ [])

  data SafetyRulesService : Set where
    SRSLocal : SafetyRulesService

  record SafetyRulesConfig : Set where
    constructor SafetyRulesConfig∙new
    field
      _srcService                     : SafetyRulesService
      _srcExportConsensusKey          : Bool
      _srcObmGenesisWaypoint          : Waypoint
  open SafetyRulesConfig public
  unquoteDecl srcService   srcExportConsensusKey   srcObmGenesisWaypoint = mkLens  (quote SafetyRulesConfig)
             (srcService ∷ srcExportConsensusKey ∷ srcObmGenesisWaypoint ∷ [])

  record ConsensusConfig : Set where
    constructor ConsensusConfig∙new
    field
      _ccMaxPrunedBlocksInMem  : Usize
      _ccRoundInitialTimeoutMS : U64
      _ccSafetyRules           : SafetyRulesConfig
      _ccSyncOnly              : Bool
  open ConsensusConfig public
  unquoteDecl ccMaxPrunedBlocksInMem   ccRoundInitialTimeoutMS   ccSafetyRules   ccSyncOnly = mkLens (quote ConsensusConfig)
             (ccMaxPrunedBlocksInMem ∷ ccRoundInitialTimeoutMS ∷ ccSafetyRules ∷ ccSyncOnly ∷ [])

  record NodeConfig : Set where
    constructor NodeConfig∙new
    field
      _ncObmMe     : AuthorName
      _ncConsensus : ConsensusConfig
  open NodeConfig public
  unquoteDecl ncObmMe    ncConsensus = mkLens  (quote NodeConfig)
             (ncObmMe ∷  ncConsensus ∷ [])

  record RecoveryManager : Set where
    constructor RecoveryManager∙new
    field
      _rcmEpochState         : EpochState
      _rcmStorage            : PersistentLivenessStorage
    --_rcmStateComputer      : StateComputer
      _rcmLastCommittedRound : Round
  open RecoveryManager public
  unquoteDecl rcmEpochState   rcmStorage {-  rcmStateComputer-}  rcmLastCommittedRound = mkLens (quote RecoveryManager)
             (rcmEpochState ∷ rcmStorage {-∷ rcmStateComputer-} ∷ rcmLastCommittedRound ∷ [])

  -- RoundProcessor  in EpochManagerTypes (because it depends on RoundManager)
  -- EpochManager    in EpochManagerTypes (because it depends on RoundProcessor)

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

  data VoteReceptionResult : Set where
    QCVoteAdded           : U64 →                VoteReceptionResult
    TCVoteAdded           : U64 →                VoteReceptionResult
    DuplicateVote         :                      VoteReceptionResult
    EquivocateVote        :                      VoteReceptionResult
    NewQuorumCertificate  : QuorumCert →         VoteReceptionResult
    NewTimeoutCertificate : TimeoutCertificate → VoteReceptionResult
    UnexpectedRound       : Round → Round →      VoteReceptionResult
    VRR_TODO              :                      VoteReceptionResult

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

-- LibraBFT.ImplShared.Interface.Output contains
-- Output

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

  data VerifyError : Set where
    UnknownAuthor        : AuthorName →    VerifyError
    TooLittleVotingPower : U64 → U64 →     VerifyError
    TooManySignatures    : Usize → Usize → VerifyError
    InvalidSignature     :                 VerifyError


text:
-- Actually, we're cheating (for expediency); this is
-- Symmetric Rig, not just Rig.
module Categories.RigCategory where

open import Level
open import Data.Fin renaming (zero to 0F; suc to sucF)
open import Data.Product using (_,_)

open import Categories.Category
open import Categories.Functor
open import Categories.Monoidal
open import Categories.Monoidal.Braided
open import Categories.Monoidal.Braided.Helpers
open import Categories.Monoidal.Symmetric
open import Categories.Monoidal.Helpers
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (_∘₀_; _∘₁_; _∘ˡ_; _∘ʳ_; NaturalTransformation) renaming (_≡_ to _≡ⁿ_; id to idⁿ)

-- first round of setting up, just for defining the NaturalIsomorphisms
-- of Rig.  Next one will be for the equalities.
module BimonoidalHelperFunctors {o ℓ e} {C : Category o ℓ e}
  {M⊎ M× : Monoidal C} (B⊎ : Braided M⊎) (B× : Braided M×) where

  private
    module C = Category C
    module M⊎ = Monoidal M⊎
    module M× = Monoidal M×
    module B⊎ = Braided B⊎
    module B× = Braided B×

  module h⊎ = MonoidalHelperFunctors C M⊎.⊗ M⊎.id
  module h× = MonoidalHelperFunctors C M×.⊗ M×.id
  module b⊎ = BraidedHelperFunctors C M⊎.⊗ M⊎.id
  module b× = BraidedHelperFunctors C M×.⊗ M×.id

  module br⊎ = b⊎.Braiding M⊎.identityˡ M⊎.identityʳ M⊎.assoc B⊎.braid
  module br× = b×.Braiding M×.identityˡ M×.identityʳ M×.assoc B×.braid

  import Categories.Power.NaturalTransformation
  private module PowNat = Categories.Power.NaturalTransformation C
  open PowNat hiding (module C)

  -- for convenience of multiple of the larger equations, define
  -- shorthands for 3 and 4 variables
  x⊗z : Powerendo 3
  x⊗z = select 0 h×.⊗₂ select 2

  z⊗x : Powerendo 3
  z⊗x = (select 2) h×.⊗₂ (select 0)

  z⊗y : Powerendo 3
  z⊗y = select 2 h×.⊗₂ select 1

  y⊗z : Powerendo 3
  y⊗z = select 1 h×.⊗₂ select 2

  x : Powerendo 4
  x = select 0

  y : Powerendo 4
  y = select 1

  z : Powerendo 4
  z = select 2

  w : Powerendo 4
  w = select 3

  -- combinations of 3 variables
  x⊗[y⊕z] : Powerendo 3
  x⊗[y⊕z] = h×.x h×.⊗ (h⊎.x⊗y)

  x⊗[z⊕y] : Powerendo 3
  x⊗[z⊕y] = h×.x h×.⊗ h⊎.y⊗x

  [x⊕y]⊗z : Powerendo 3
  [x⊕y]⊗z = (h⊎.x⊗y) h×.⊗ h×.x

  z⊗[x⊕y] : Powerendo 3
  z⊗[x⊕y] = (select 2) h×.⊗₂ ((select 0) h⊎.⊗₂ (select 1))

  [x⊗y]⊕[x⊗z] : Powerendo 3
  [x⊗y]⊕[x⊗z] = (select 0 h×.⊗₂ select 1) h⊎.⊗₂ (select 0 h×.⊗₂ select 2)

  [x⊗z]⊕[y⊗z] : Powerendo 3
  [x⊗z]⊕[y⊗z] = (select 0 h×.⊗₂ select 2) h⊎.⊗₂ (select 1 h×.⊗₂ select 2)

  [z⊗x]⊕[z⊗y] : Powerendo 3
  [z⊗x]⊕[z⊗y] = z⊗x h⊎.⊗₂ z⊗y

  [x⊗z]⊕[x⊗y] : Powerendo 3
  [x⊗z]⊕[x⊗y] = x⊗z h⊎.⊗₂ (select 0 h×.⊗₂ select 1)

  x⊗0 : Powerendo 1
  x⊗0 = h⊎.x h×.⊗ h⊎.id↑

  0⊗x : Powerendo 1
  0⊗x = h⊎.id↑ h×.⊗ h⊎.x

  0↑ : Powerendo 1
  0↑ = widenˡ 1 h⊎.id↑

  xy : Powerendo 4
  xy = widenʳ 2 h×.x⊗y

  yz : Powerendo 4
  yz = select 1 h×.⊗₂ select 2

  xw : Powerendo 4
  xw = select 0 h×.⊗₂ select 3

  yw : Powerendo 4
  yw = select 1 h×.⊗₂ select 3

  zw : Powerendo 4
  zw = select 2 h×.⊗₂ select 3

  xz : Powerendo 4
  xz = select 0 h×.⊗₂ select 2

  z⊕w : Powerendo 4
  z⊕w = widenˡ 2 h⊎.x⊗y

  -- for 2 variables
  x₂ : Powerendo 2
  x₂ = widenʳ 1 h×.x

  y₂ : Powerendo 2
  y₂ = widenˡ 1 h×.x

  -- 0 variables!
  0₀ : Powerendo 0
  0₀ = h⊎.id↑

  0⊗0 : Powerendo 0
  0⊗0 = 0₀ h×.⊗ 0₀

  0⊕0 : Powerendo 0
  0⊕0 = 0₀ h⊎.⊗ 0₀

  1₀ : Powerendo 0
  1₀ = h×.id↑

  -- 1 variable + 0
  A0 : Powerendo 1
  A0 = h×.x h×.⊗ 0₀

  0A : Powerendo 1
  0A = 0₀ h×.⊗ h×.x

  -- 2 variables + 0
  0₂ : Powerendo 2
  0₂ = widenʳ 2 0₀

  0[A⊕B] : Powerendo 2
  0[A⊕B] = 0₂ h×.⊗₂ h⊎.x⊗y

  0[AB] : Powerendo 2
  0[AB] = 0₀ h×.⊗ (h×.x⊗y)

  [0A]B : Powerendo 2
  [0A]B = 0A h×.⊗ h×.x

  0A₂ : Powerendo 2
  0A₂ = 0₂ h×.⊗₂ select 0

  0B : Powerendo 2
  0B = 0₂ h×.⊗₂ (select 1)

  A0₂ : Powerendo 2
  A0₂ = select 0 h×.⊗₂ 0₂

  AB : Powerendo 2
  AB = h×.x⊗y

  0A⊕0B : Powerendo 2
  0A⊕0B = 0A₂ h⊎.⊗₂ 0B

  A[0B] : Powerendo 2
  A[0B] = (widenʳ 1 h×.x) h×.⊗₂ 0B

  [A0]B : Powerendo 2
  [A0]B = A0 h×.⊗ h×.x

  A[0⊕B] : Powerendo 2
  A[0⊕B] = h×.x h×.⊗ h⊎.id⊗x

  A0⊕AB : Powerendo 2
  A0⊕AB = A0₂ h⊎.⊗₂ AB

  0⊕AB : Powerendo 2
  0⊕AB = 0₂ h⊎.⊗₂ AB

  -- 2 variables + 1
  1₂ : Powerendo 2
  1₂ = widenʳ 2 1₀

  A⊕B : Powerendo 2
  A⊕B = h⊎.x⊗y

  1[A⊕B] : Powerendo 2
  1[A⊕B] = 1₀ h×.⊗ A⊕B

  1A⊕1B : Powerendo 2
  1A⊕1B = h×.id⊗x h⊎.⊗ h×.id⊗x

  -- like Laplaza, use concatenation for ⊗ to make things easier to read
  -- also ⊗ binds more tightly, so skip those parens

  -- combinations of 4 variables
  [x⊕[y⊕z]]w : Powerendo 4
  [x⊕[y⊕z]]w = h⊎.x⊗[y⊗z] h×.⊗ h⊎.x

  xw⊕[y⊕z]w : Powerendo 4
  xw⊕[y⊕z]w = (x h×.⊗₂ w) h⊎.⊗₂ ((y h⊎.⊗₂ z) h×.⊗₂ w)

  xw⊕[yw⊕zw] : Powerendo 4
  xw⊕[yw⊕zw] = (x h×.⊗₂ w) h⊎.⊗₂ ((y h×.⊗₂ w) h⊎.⊗₂ (z h×.⊗₂ w))

  [xw⊕yw]⊕zw : Powerendo 4
  [xw⊕yw]⊕zw = ((x h×.⊗₂ w) h⊎.⊗₂ (y h×.⊗₂ w)) h⊎.⊗₂ (z h×.⊗₂ w)

  [[x⊕y]⊕z]w : Powerendo 4
  [[x⊕y]⊕z]w = h⊎.[x⊗y]⊗z h×.⊗ h⊎.x

  [x⊕y]w⊕zw : Powerendo 4
  [x⊕y]w⊕zw = ((x h⊎.⊗₂ y) h×.⊗₂ w) h⊎.⊗₂ (z h×.⊗₂ w)

  x[y[z⊕w]] : Powerendo 4
  x[y[z⊕w]] = x h×.⊗₂ (y h×.⊗₂ (z h⊎.⊗₂ w))

  x[yz⊕yw] : Powerendo 4
  x[yz⊕yw] = x h×.⊗₂ ((y h×.⊗₂ z) h⊎.⊗₂ (y h×.⊗₂ w))

  x[yz]⊕x[yw] : Powerendo 4
  x[yz]⊕x[yw] = (x h×.⊗₂ (y h×.⊗₂ z)) h⊎.⊗₂ (x h×.⊗₂ (y h×.⊗₂ w))

  [xy][z⊕w] : Powerendo 4
  [xy][z⊕w] = (x h×.⊗₂ y) h×.⊗₂ (z h⊎.⊗₂ w)

  [xy]z⊕[xy]w : Powerendo 4
  [xy]z⊕[xy]w = let xy = (x h×.⊗₂ y) in (xy h×.⊗₂ z) h⊎.⊗₂ (xy h×.⊗₂ w)

  x⊕y : Powerendo 4
  x⊕y = widenʳ 2 h⊎.x⊗y

  x[z⊕w] : Powerendo 4
  x[z⊕w] = x h×.⊗₂ z⊕w

  y[z⊕w] : Powerendo 4
  y[z⊕w] = y h×.⊗₂ z⊕w

  xz⊕xw : Powerendo 4
  xz⊕xw = xz h⊎.⊗₂ xw

  yz⊕yw : Powerendo 4
  yz⊕yw = yz h⊎.⊗₂ yw

  xz⊕yz : Powerendo 4
  xz⊕yz = xz h⊎.⊗₂ yz

  xw⊕yw : Powerendo 4
  xw⊕yw = xw h⊎.⊗₂ yw

  [x⊕y]z : Powerendo 4
  [x⊕y]z = x⊕y h×.⊗₂ z

  [x⊕y]w : Powerendo 4
  [x⊕y]w = x⊕y h×.⊗₂ w

  [x⊕y][z⊕w] : Powerendo 4
  [x⊕y][z⊕w] = x⊕y h×.⊗₂ z⊕w

  [x⊕y]z⊕[x⊕y]w : Powerendo 4
  [x⊕y]z⊕[x⊕y]w = [x⊕y]z h⊎.⊗₂ [x⊕y]w

  [xz⊕yz]⊕[xw⊕yw] : Powerendo 4
  [xz⊕yz]⊕[xw⊕yw] = xz⊕yz h⊎.⊗₂ xw⊕yw

  [[xz⊕yz]⊕xw]⊕yw : Powerendo 4
  [[xz⊕yz]⊕xw]⊕yw = (xz⊕yz h⊎.⊗₂ xw) h⊎.⊗₂ yw

  x[z⊕w]⊕y[z⊕w] : Powerendo 4
  x[z⊕w]⊕y[z⊕w] = x[z⊕w] h⊎.⊗₂ y[z⊕w]

  [xz⊕xw]⊕[yz⊕yw] : Powerendo 4
  [xz⊕xw]⊕[yz⊕yw] = xz⊕xw h⊎.⊗₂ yz⊕yw

  [[xz⊕xw]⊕yz]⊕yw : Powerendo 4
  [[xz⊕xw]⊕yz]⊕yw = (xz⊕xw h⊎.⊗₂ yz) h⊎.⊗₂ yw

  [xz⊕[xw⊕yz]]⊕yw : Powerendo 4
  [xz⊕[xw⊕yz]]⊕yw = (xz h⊎.⊗₂ (xw h⊎.⊗₂ yz)) h⊎.⊗₂ yw

  [xz⊕[yz⊕xw]]⊕yw : Powerendo 4
  [xz⊕[yz⊕xw]]⊕yw = (xz h⊎.⊗₂ (yz h⊎.⊗₂ xw)) h⊎.⊗₂ yw

  module SRig (S⊎ : Symmetric B⊎) (S× : Symmetric B×)
    (distribₗ : NaturalIsomorphism x⊗[y⊕z] [x⊗y]⊕[x⊗z])
    (distribᵣ : NaturalIsomorphism [x⊕y]⊗z [x⊗z]⊕[y⊗z])
    (annₗ : NaturalIsomorphism 0⊗x 0↑)
    (annᵣ : NaturalIsomorphism x⊗0 0↑) where

    open NaturalIsomorphism distribₗ using () renaming (F⇒G to dₗ)
    open NaturalIsomorphism distribᵣ using () renaming (F⇒G to dᵣ)
    open NaturalIsomorphism annₗ using () renaming (F⇒G to aₗ)
    open NaturalIsomorphism annᵣ using () renaming (F⇒G to aᵣ)

    dₗ-over : ∀ {n} (F₁ F₂ F₃ : Powerendo n) → NaturalTransformation (F₁ h×.⊗₂ (F₂ h⊎.⊗₂ F₃)) ((F₁ h×.⊗₂ F₂) h⊎.⊗₂ (F₁ h×.⊗₂ F₃))
    dₗ-over F₁ F₂ F₃ = dₗ ∘ʳ plex {3} F₁ F₂ F₃

    dᵣ-over : ∀ {n} (F₁ F₂ F₃ : Powerendo n) → NaturalTransformation ((F₁ h⊎.⊗₂ F₂) h×.⊗₂ F₃) ((F₁ h×.⊗₂ F₃) h⊎.⊗₂ (F₂ h×.⊗₂ F₃))
    dᵣ-over F₁ F₂ F₃ = dᵣ ∘ʳ plex {3} F₁ F₂ F₃

    aₗ-over : ∀ {n} (F₁ : Powerendo n) → NaturalTransformation ((widenʳ n 0₀) h×.⊗₂ F₁) (widenʳ n 0₀)
    aₗ-over F₁ = aₗ ∘ʳ plex {1} F₁

    aᵣ-over : ∀ {n} (F₁ : Powerendo n) → NaturalTransformation (F₁ h×.⊗₂ (widenʳ n 0₀)) (widenʳ n 0₀)
    aᵣ-over F₁ = aᵣ ∘ʳ plex {1} F₁

    uₗ⊕-over : ∀ {n} (F₁ : Powerendo n) → NaturalTransformation ((widenʳ n 0₀) h⊎.⊗₂ F₁) F₁
    uₗ⊕-over F₁ = (NaturalIsomorphism.F⇒G M⊎.identityˡ) ∘ʳ plex {1} F₁

    uₗ⊗-over : ∀ {n} (F₁ : Powerendo n) → NaturalTransformation ((widenʳ n 1₀) h×.⊗₂ F₁) F₁
    uₗ⊗-over F₁ = (NaturalIsomorphism.F⇒G M×.identityˡ) ∘ʳ plex {1} F₁

    uᵣ⊗-over : ∀ {n} (F₁ : Powerendo n) → NaturalTransformation (F₁ h×.⊗₂ (widenʳ n 1₀)) F₁
    uᵣ⊗-over F₁ = (NaturalIsomorphism.F⇒G M×.identityʳ) ∘ʳ plex {1} F₁

    s⊕-over : ∀ {n} (F₁ F₂ : Powerendo n) → NaturalTransformation (F₁ h⊎.⊗₂ F₂) (F₂ h⊎.⊗₂ F₁)
    s⊕-over F₁ F₂ = (NaturalIsomorphism.F⇒G B⊎.braid) ∘ʳ plex {2} F₁ F₂

    s⊗-over : ∀ {n} (F₁ F₂ : Powerendo n) → NaturalTransformation (F₁ h×.⊗₂ F₂) (F₂ h×.⊗₂ F₁)
    s⊗-over F₁ F₂ = (NaturalIsomorphism.F⇒G B×.braid) ∘ʳ plex {2} F₁ F₂

    -- for 2 variables
    idx₂ : NaturalTransformation x₂ x₂
    idx₂ = idⁿ

    idy₂ : NaturalTransformation y₂ y₂
    idy₂ = idⁿ

    idxy : NaturalTransformation AB AB
    idxy = idⁿ

    -- these are all for 3 variables
    Bxz : NaturalTransformation x⊗z z⊗x
    Bxz = br×.B-over (select 0) (select 2)

    Byz : NaturalTransformation y⊗z z⊗y
    Byz = br×.B-over (select 1) (select 2)

    Bxz⊕Byz : NaturalTransformation [x⊗z]⊕[y⊗z] [z⊗x]⊕[z⊗y]
    Bxz⊕Byz = Bxz h⊎.⊗ⁿ′ Byz

    B[x⊕y]z : NaturalTransformation [x⊕y]⊗z z⊗[x⊕y]
    B[x⊕y]z = br×.B-over (widenʳ 1 h⊎.x⊗y) (select 2)

    dᵣABC : NaturalTransformation [x⊕y]⊗z [x⊗z]⊕[y⊗z]
    dᵣABC = dᵣ-over (select 0) (select 1) (select 2)

    dₗABC : NaturalTransformation x⊗[y⊕z] [x⊗y]⊕[x⊗z]
    dₗABC = dₗ-over (select 0) (select 1) (select 2)

    dₗACB : NaturalTransformation x⊗[z⊕y] [x⊗z]⊕[x⊗y]
    dₗACB = dₗ-over (select 0) (select 2) (select 1)

    dₗCAB : NaturalTransformation z⊗[x⊕y] [z⊗x]⊕[z⊗y]
    dₗCAB = dₗ-over (select 2) (select 0) (select 1)

    1⊗Byz : NaturalTransformation x⊗[y⊕z] x⊗[z⊕y]
    1⊗Byz = reduceN M×.⊗ h×.id₂ (br⊎.B-over (select 0) (select 1))

    B[x⊗y][x⊗z] : NaturalTransformation [x⊗y]⊕[x⊗z] [x⊗z]⊕[x⊗y]
    B[x⊗y][x⊗z] = br⊎.B-over (widenʳ 1 h×.x⊗y) x⊗z

    -- these are all for 4 variables
    dᵣA[B⊕C]D : NaturalTransformation [x⊕[y⊕z]]w xw⊕[y⊕z]w
    dᵣA[B⊕C]D = dᵣ-over (select 0) (widenʳ 1 (widenˡ 1 h⊎.x⊗y)) (select 3)

    dᵣBCD : NaturalTransformation (widenˡ 1 [x⊕y]⊗z) (widenˡ 1 [x⊗z]⊕[y⊗z])
    dᵣBCD = dᵣ-over (select 1) (select 2) (select 3)

    id03 : NaturalTransformation xw xw
    id03 = idⁿ

    id23 : NaturalTransformation zw zw
    id23 = idⁿ

    idx : NaturalTransformation x x
    idx = idⁿ

    idw : NaturalTransformation w w
    idw = idⁿ

    idyw : NaturalTransformation yw yw
    idyw = idⁿ

    idxz : NaturalTransformation xz xz
    idxz = idⁿ

    1⊗dᵣBCD : NaturalTransformation xw⊕[y⊕z]w xw⊕[yw⊕zw]
    1⊗dᵣBCD = overlapN M⊎.⊗ id03 dᵣBCD

    assocˡAD-BD-CD : NaturalTransformation xw⊕[yw⊕zw] [xw⊕yw]⊕zw
    assocˡAD-BD-CD = br⊎.α₂-over xw yw zw

    αˡABC⊗1 : NaturalTransformation [x⊕[y⊕z]]w [[x⊕y]⊕z]w
    αˡABC⊗1 = overlapN M×.⊗ (br⊎.α₂-over (select 0) (select 1) (select 2)) idw

    dᵣ[A⊕B]CD : NaturalTransformation [[x⊕y]⊕z]w [x⊕y]w⊕zw
    dᵣ[A⊕B]CD = dᵣ-over (widenʳ 2 h⊎.x⊗y) (select 2) (select 3)

    dᵣABD⊗1 : NaturalTransformation [x⊕y]w⊕zw [xw⊕yw]⊕zw
    dᵣABD⊗1 = overlapN M⊎.⊗ (dᵣ-over (select 0) (select 1) (select 3)) id23

    1A⊗dₗBCD : NaturalTransformation x[y[z⊕w]] x[yz⊕yw]
    1A⊗dₗBCD = overlapN M×.⊗ idx (dₗ-over y z w)

    dₗA[BC][BD] : NaturalTransformation x[yz⊕yw] x[yz]⊕x[yw]
    dₗA[BC][BD] = dₗ-over x yz yw

    αABC⊕αABD : NaturalTransformation x[yz]⊕x[yw] [xy]z⊕[xy]w
    αABC⊕αABD = overlapN M⊎.⊗ (br×.α₂-over x y z) (br×.α₂-over x y w)

    αAB[C⊕D] : NaturalTransformation x[y[z⊕w]] [xy][z⊕w]
    αAB[C⊕D] = br×.α₂-over x y z⊕w

    dₗ[AB]CD : NaturalTransformation [xy][z⊕w] [xy]z⊕[xy]w
    dₗ[AB]CD = dₗ-over xy z w

    dₗ0AB : NaturalTransformation 0[A⊕B] 0A⊕0B
    dₗ0AB = dₗ-over (widenʳ 2 0₀) (select 0) (select 1)

    aₗA⊕aₗB : NaturalTransformation 0A⊕0B (widenʳ 2 0⊕0)
    aₗA⊕aₗB = overlapN M⊎.⊗ (aₗ-over (select 0)) (aₗ-over (select 1))

    -- a bit weird, but the widening is needed
    uˡ0 : NaturalTransformation (widenʳ 2 0⊕0) (widenʳ 2 0₀)
    uˡ0 = uₗ⊕-over (widenʳ 2 0₀)

    aᵣA : NaturalTransformation A0 0↑
    aᵣA = aᵣ-over (select 0)

    aₗA : NaturalTransformation 0A (widenʳ 1 0₀)
    aₗA = aₗ-over (select 0)

    s⊗A0 : NaturalTransformation A0 0A
    s⊗A0 = s⊗-over (select 0) 0↑

    α0AB : NaturalTransformation 0[AB] [0A]B
    α0AB = br×.α₂-over 0₂ (select 0) (select 1)

    aₗA⊗1B : NaturalTransformation [0A]B 0B
    aₗA⊗1B = overlapN M×.⊗ (aₗ-over (select 0)) idy₂

    aₗAB : NaturalTransformation 0[AB] 0₂
    aₗAB = aₗ-over h×.x⊗y

    aₗB : NaturalTransformation 0B 0₂
    aₗB = aₗ-over y₂

    αA0B : NaturalTransformation A[0B] [A0]B
    αA0B = br×.α₂-over (select 0) 0₂ (select 1)

    aᵣA⊗1B : NaturalTransformation [A0]B 0B
    aᵣA⊗1B = overlapN M×.⊗ (aᵣ-over (select 0)) idy₂

    1A⊗aₗB : NaturalTransformation A[0B] (widenʳ 1 A0)
    1A⊗aₗB = overlapN M×.⊗ idx₂ aₗB

    aᵣA₂ : NaturalTransformation (widenʳ 1 A0) 0₂
    aᵣA₂ = aᵣ-over (select 0)

    1A⊗uₗB : NaturalTransformation A[0⊕B] AB
    1A⊗uₗB = overlapN M×.⊗ idx₂ (uₗ⊕-over y₂)

    dₗA0B : NaturalTransformation A[0⊕B] A0⊕AB
    dₗA0B = dₗ-over x₂ 0₂ y₂

    aᵣA⊕1AB : NaturalTransformation A0⊕AB 0⊕AB
    aᵣA⊕1AB = overlapN M⊎.⊗ (aᵣ-over x₂) idxy

    uₗAB : NaturalTransformation 0⊕AB AB
    uₗAB = uₗ⊕-over AB

    dₗ1AB : NaturalTransformation 1[A⊕B] 1A⊕1B
    dₗ1AB = dₗ-over 1₂ x₂ y₂

    uₗA⊕B : NaturalTransformation 1[A⊕B] A⊕B
    uₗA⊕B = uₗ⊗-over h⊎.x⊗y

    uₗA⊕uₗB : NaturalTransformation 1A⊕1B A⊕B
    uₗA⊕uₗB = overlapN M⊎.⊗ (uₗ⊗-over x₂) (uₗ⊗-over y₂)

    -- the monster, aka diagram IX
    dₗ[A⊕B]CD : NaturalTransformation [x⊕y][z⊕w] [x⊕y]z⊕[x⊕y]w
    dₗ[A⊕B]CD = dₗ-over x⊕y z w

    dᵣABC⊕dᵣABD : NaturalTransformation [x⊕y]z⊕[x⊕y]w [xz⊕yz]⊕[xw⊕yw]
    dᵣABC⊕dᵣABD = overlapN M⊎.⊗ ( dᵣ-over x y z ) (dᵣ-over x y w)

    α[AC⊕BC][AD][BD] : NaturalTransformation [xz⊕yz]⊕[xw⊕yw] [[xz⊕yz]⊕xw]⊕yw
    α[AC⊕BC][AD][BD] = br⊎.α₂-over xz⊕yz xw yw

    dᵣAB[C⊕D] : NaturalTransformation [x⊕y][z⊕w] x[z⊕w]⊕y[z⊕w]
    dᵣAB[C⊕D] = dᵣ-over x y z⊕w

    dₗACD⊕dₗBCD : NaturalTransformation x[z⊕w]⊕y[z⊕w] [xz⊕xw]⊕[yz⊕yw]
    dₗACD⊕dₗBCD = overlapN M⊎.⊗ (dₗ-over x z w) (dₗ-over y z w)

    α[AC⊕AD][BC][BD] : NaturalTransformation [xz⊕xw]⊕[yz⊕yw] [[xz⊕xw]⊕yz]⊕yw
    α[AC⊕AD][BC][BD] = br⊎.α₂-over xz⊕xw yz yw

    α′[AC][AD][BC]⊕1BD : NaturalTransformation [[xz⊕xw]⊕yz]⊕yw [xz⊕[xw⊕yz]]⊕yw
    α′[AC][AD][BC]⊕1BD = overlapN M⊎.⊗ (br⊎.α-over xz xw yz) idyw

    [1AC⊕s[AD][BC]]⊕1BD : NaturalTransformation [xz⊕[xw⊕yz]]⊕yw [xz⊕[yz⊕xw]]⊕yw
    [1AC⊕s[AD][BC]]⊕1BD = overlapN M⊎.⊗ (overlapN M⊎.⊗ idxz (s⊕-over xw yz)) idyw

    α[AC][BC][AD]⊕1BD : NaturalTransformation [xz⊕[yz⊕xw]]⊕yw [[xz⊕yz]⊕xw]⊕yw
    α[AC][BC][AD]⊕1BD = overlapN M⊎.⊗ (br⊎.α₂-over xz yz xw) idyw

record RigCategory {o ℓ e} {C : Category o ℓ e}
  {M⊎ M× : Monoidal C} {B⊎ : Braided M⊎} (S⊎ : Symmetric B⊎)
   {B× : Braided M×} (S× : Symmetric B×) : Set (o ⊔ ℓ ⊔ e) where

  open BimonoidalHelperFunctors B⊎ B×

  field
    distribₗ : NaturalIsomorphism x⊗[y⊕z] [x⊗y]⊕[x⊗z]
    distribᵣ : NaturalIsomorphism [x⊕y]⊗z [x⊗z]⊕[y⊗z]
    annₗ : NaturalIsomorphism 0⊗x 0↑
    annᵣ : NaturalIsomorphism x⊗0 0↑

  open SRig S⊎ S× distribₗ distribᵣ annₗ annᵣ

  -- need II, IX, X, XV
  -- choose I, IV, VI, XI, XIII, XIX, XXIII and (XVI, XVII)
  field
    .laplazaI : dₗACB ∘₁ 1⊗Byz ≡ⁿ B[x⊗y][x⊗z] ∘₁ dₗABC
    .laplazaII : Bxz⊕Byz ∘₁ dᵣABC ≡ⁿ dₗCAB ∘₁ B[x⊕y]z
    .laplazaIV : dᵣABD⊗1 ∘₁ (dᵣ[A⊕B]CD ∘₁ αˡABC⊗1) ≡ⁿ assocˡAD-BD-CD ∘₁ (1⊗dᵣBCD ∘₁ dᵣA[B⊕C]D)
    .laplazaVI : dₗ[AB]CD ∘₁ αAB[C⊕D] ≡ⁿ αABC⊕αABD ∘₁ (dₗA[BC][BD] ∘₁ 1A⊗dₗBCD)
    .laplazaIX : α[AC⊕BC][AD][BD] ∘₁ (dᵣABC⊕dᵣABD ∘₁ dₗ[A⊕B]CD) ≡ⁿ
        α[AC][BC][AD]⊕1BD ∘₁ ([1AC⊕s[AD][BC]]⊕1BD ∘₁ (α′[AC][AD][BC]⊕1BD ∘₁
           (α[AC⊕AD][BC][BD] ∘₁ (dₗACD⊕dₗBCD ∘₁ dᵣAB[C⊕D]))))
    .laplazaX : aₗ-over 0₀ ≡ⁿ aᵣ-over 0₀
    .laplazaXI : aₗ-over (h⊎.x⊗y) ≡ⁿ uˡ0 ∘₁ (aₗA⊕aₗB ∘₁ dₗ0AB)
    .laplazaXIII : uᵣ⊗-over 0₀ ≡ⁿ aₗ-over 1₀
    .laplazaXV : aᵣA ≡ⁿ aₗA ∘₁ s⊗A0
    .laplazaXVI : aₗAB ≡ⁿ aₗB ∘₁ (aₗA⊗1B ∘₁ α0AB)
    .laplazaXVII : aᵣA₂ ∘₁ 1A⊗aₗB ≡ⁿ aₗB ∘₁ (aᵣA⊗1B ∘₁ αA0B)
    .laplazaXIX : 1A⊗uₗB ≡ⁿ uₗAB ∘₁ (aᵣA⊕1AB ∘₁ dₗA0B)
    .laplazaXXIII : uₗA⊕B ≡ⁿ uₗA⊕uₗB ∘₁ dₗ1AB

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
module Properties.Step where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Heap using (Heap; lookup; alloc; ok; function_⟨_⟩_end)
open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Value using (nil; addr; val)
open import Properties.Remember using (remember; _,_)

data StepResultᴮ (H : Heap) (B : Block) : Set
data StepResultᴱ (H : Heap) (M : Expr) : Set

data StepResultᴮ H B where
  step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
  return : ∀ V {B′} → (B ≡ (return (val V) ∙ B′)) → StepResultᴮ H B
  done : (B ≡ done) → StepResultᴮ H B
  error : (RuntimeErrorᴮ H B) → StepResultᴮ H B

data StepResultᴱ H M where
  step : ∀ H′ M′ → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → StepResultᴱ H M
  value : ∀ V → (M ≡ val V) → StepResultᴱ H M
  error : (RuntimeErrorᴱ H M) → StepResultᴱ H M

stepᴱ : ∀ H M → StepResultᴱ H M
stepᴮ : ∀ H B → StepResultᴮ H B

stepᴱ H nil = value nil refl
stepᴱ H (var x) = error (UnboundVariable x)
stepᴱ H (addr a) = value (addr a) refl
stepᴱ H (M $ N) with stepᴱ H M
stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app D)
stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
stepᴱ H (addr a $ N) | value (addr a) refl with remember (lookup H a)
stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
stepᴱ H (addr a $ N) | value (addr a) refl | (just(function f ⟨ x ⟩ B end) , p) = step H (block f is local x ← N ∙ B end) (beta p)
stepᴱ H (M $ N) | error E = error (app E)
stepᴱ H (function⟨ x ⟩ B end) with alloc H (function "anon" ⟨ x ⟩ B end)
stepᴱ H (function⟨ x ⟩ B end) | ok a H′ p = step H′ (addr a) (function p)
stepᴱ H (block b is B end) with stepᴮ H B
stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return
stepᴱ H (block b is done end) | done refl = step H nil done
stepᴱ H (block b is B end) | error E = error (block b E)

stepᴮ H (function f ⟨ x ⟩ C end ∙ B) with alloc H (function f ⟨ x ⟩ C end)
stepᴮ H (function f ⟨ x ⟩ C end ∙ B) | ok a H′ p = step H′ (B [ addr a / f ]ᴮ) (function p)
stepᴮ H (local x ← M ∙ B) with stepᴱ H M
stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / x ]ᴮ) subst
stepᴮ H (local x ← M ∙ B) | error E = error (local x E)
stepᴮ H (return M ∙ B) with stepᴱ H M
stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
stepᴮ H (return _ ∙ B) | value V refl = return V refl
stepᴮ H (return M ∙ B) | error E = error (return E)
stepᴮ H done = done refl

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
-- The --no-coverage-check option has been removed.

{-# OPTIONS --no-coverage-check #-}

module Issue1918 where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module AllTests where

import Issue14
import Issue65
import Issue73
import Fixities
import LanguageConstructs
import Numbers
import Pragmas
import Sections
import Test
import Tuples
import Where
import TypeSynonyms
import Datatypes
import Records
import DefaultMethods
import Vector

{-# FOREIGN AGDA2HS
import Issue14
import Issue65
import Issue73
import Fixities
import LanguageConstructs
import Numbers
import Pragmas
import Sections
import Test
import Tuples
import Where
import TypeSynonyms
import Datatypes
import Records
import DefaultMethods
import Vector
#-}


text:
module _ where

postulate
  T U V : Set
  F G : Set → Set
  Sea : {A : Set} → (A → A → Set) → Set
  Seas : {I : Set} (As : I → Set) → ({i j : I} → As i → As j → Set) → Set
  _eq_ _to_ : T → T → Set

record K : Set₁ where
  field
    A : Set
    B : A → A → Set
    C : Sea B

record IK (I : Set) : Set₁ where
  field
    As : I → Set
    Bs : {i j : I} → As i → As j → Set
    Cs : Seas As Bs

open K
open IK

record L (f t : K) : Set where
  field
    D : A f → A t
    E : ∀ {x y} → (B f x y) → B t (D x) (D y)

record IL (f : K) (t : IK (A f)): Set where
  field
    Ds : (x : A f) → As t x
    Es : ∀ {x y} → (B f x y) → Bs t (Ds x) (Ds y)

-- make Cs or E irrelevant and the last line turns yellow
postulate blah : ∀ {a b c : K} → L a b → L b c → L a c

foop : ∀ {a b c d : K} → L a b → L b c → L c d → L a d
foop f g h = blah f (blah g h)

postulate Equiv : Sea _eq_

Cat : K
Cat = record
  { A = T
  ; B = _eq_
  ; C = Equiv
  }

record T2 : Set where
  constructor _,_
  field fst snd : T

open T2

record _eq2_ (a b : T2) : Set where
  constructor _∧_
  field
    feq : (fst a) eq (fst b)
    seq : (snd a) eq (snd b)

postulate Equiv2 : Sea _eq2_

Cat2 : K
Cat2 = record { A = T2; B = _eq2_; C = Equiv2 }

postulate
  Hm : T2 → Set
  _heq_ : {t t' : T2} → Hm t → Hm t' → Set
  HEquiv : Seas Hm _heq_

Hom : IK T2
Hom = record
  { As = Hm
  ; Bs = _heq_
  ; Cs = HEquiv
  }

_×_ : ∀ {U} → L U Cat → L U Cat → L U Cat2
X × Y = record { D = λ x → L.D X x , L.D Y x
               ; E = λ x' → L.E X x' ∧ L.E Y x' }

postulate
  _∘_ : ∀ {a b c} → Hm (b , c) → Hm (a , b) → Hm (a , c)
  ∘cong : ∀ {a b c} {f f' : Hm (b , c)} {g g' : Hm (a , b)} → f heq f' → g heq g' → (f ∘ g) heq (f' ∘ g')
  _∘H_ : ∀ {a b c} → Hm (b , c) → Hm (a , b) → Hm (a , c)

module Fool (Base : K) where
  Dust = L Base Cat

  promote : L Base Cat2 → IK (A Base)
  promote f = record
    { As = λ x → Hm (L.D f x)
    ; Bs = λ x y → x heq y
    ; Cs = my-Cs
    }
    where
    postulate my-Cs : Seas (λ x → Hm (L.D f x)) (λ {i} {j} x y → x heq y)

  Dance : Dust → Dust → Set
  Dance f t = IL Base (promote (f × t))

  _⊚_ : ∀ {as bs cs} → Dance bs cs → Dance as bs → Dance as cs
  _⊚_ {as} {bs} {cs} fs gs = record
    { Ds = λ x → IL.Ds fs x ∘ IL.Ds gs x
    ; Es = my-Es
    }
    where
    postulate my-Es : ∀ {x y} → B Base x y → _

  comp3 : ∀ {as bs cs ds} → Dance cs ds → Dance bs cs → Dance as bs → Dance as ds
  comp3 f g h = f ⊚ (g ⊚ h)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Categories.Diagram.End.Properties where

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

open import Categories.Category
open import Categories.Category.Product
open import Categories.Category.Construction.Functors
open import Categories.Functor
open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.Dinatural
open import Categories.Diagram.End as ∫

import Categories.Morphism.Reasoning as MR

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

module _ {C : Category o ℓ e}
         (F : Functor E (Functors (Product (Category.op C) C) D)) where
  private
    module C = Category C
    module D = Category D
    module E = Category E
    module NT = NaturalTransformation
  open D
  open HomReasoning

  open MR D
  open Functor F
  open End hiding (E)
  open NT using (η)

  EndF : (∀ X → End (F₀ X)) → Functor E D
  EndF end = record
    { F₀           = λ X → End.E (end X)
    ; F₁           = F₁′
    ; identity     = λ {A} → unique (end A) (id-comm ○ ∘-resp-≈ˡ (⟺ identity))
    ; homomorphism = λ {A B C} {f g} → unique (end C) $ λ {Z} → begin
      dinatural.α (end C) Z ∘ F₁′ g ∘ F₁′ f                       ≈⟨ pullˡ (universal (end C)) ⟩
      (η (F₁ g) (Z , Z) ∘ dinatural.α (end B) Z) ∘ F₁′ f          ≈⟨ pullʳ (universal (end B)) ⟩
      η (F₁ g) (Z , Z) ∘ η (F₁ f) (Z , Z) ∘ dinatural.α (end A) Z ≈˘⟨ pushˡ homomorphism ⟩
      η (F₁ (g E.∘ f)) (Z , Z) ∘ dinatural.α (end A) Z            ∎
    ; F-resp-≈     = λ {A B f g} eq → unique (end B) $ λ {Z} → begin
      dinatural.α (end B) Z ∘ F₁′ g                               ≈⟨ universal (end B) ⟩
      η (F₁ g) (Z , Z) ∘ dinatural.α (end A) Z                    ≈˘⟨ F-resp-≈ eq ⟩∘⟨refl ⟩
      η (F₁ f) (Z , Z) ∘ dinatural.α (end A) Z                    ∎
    }
    where F₁′ : ∀ {X Y} → X E.⇒ Y → End.E (end X) ⇒ End.E (end Y)
          F₁′ {X} {Y} f = factor (end Y) $ record
            { E         = End.E (end X)
            ; dinatural = F₁ f <∘ dinatural (end X)
            }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

module Strict where

open import Agda.Builtin.Strict
open import Level

infixr 0 _$!_
_$!_ : {A : Type a} {B : A → Type b} → (∀ x → B x) → ∀ x → B x
f $! x = primForce x f
{-# INLINE _$!_ #-}

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper