{- ============================== 
   Copyright (c) 2024 SysFEAT - Systemic Framework for Enterprise Architecture & Transformation
   This work is released under the MIT License.
   framework.sysfeat.com

Individual Business Agent: 
An Individual Business Agent is an Individual Resource Agent which produces Business Outcome Events of the enterprise.
 - ============================== -}

{-# OPTIONS --cubical --guardedness #-}
{-# OPTIONS --cubical-compatible #-}

module 66f8685a620b1440 where -- ========== Individual Business Agent

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 62ff75f363765899 public -- Individual Business Asset
open import fe1c231267880201 public -- Individual Resource Agent
open import bcebd31f5491302c public -- Business Agent Type

postulate
  IndividualBusinessAgent : ClassOfBoundedIndividual

postulate --  IndividualBusinessAgent is subTypeOf IndividualBusinessAsset
  st-62ff764263765920 : IndividualBusinessAgent ⊏⋆ₑ IndividualBusinessAsset

postulate --  IndividualBusinessAgent is subTypeOf IndividualResourceAgent
  st-fe1c2cb167880dfe : IndividualBusinessAgent ⊏⋆ₑ IndividualResourceAgent

-- == Relationships =======================

{- Deployed Business Agent Part:  -}
-- Aggregate Member : Deployed Business Agent Part
postulate
  DeployedBusinessAgentPart : ClassOfIndividual

postulate -- NestingRelation: Membership of -Deployed Business Agent Part-
  membershipOfDeployedBusinessAgentPart-nestingbinding : IndividualBusinessAgent ⊏ₑ  LexicalScope {lzero}
  membershipOfDeployedBusinessAgentPart : classOfNestingRelation {ct = DeployedBusinessAgentPart}  membershipOfDeployedBusinessAgentPart-nestingbinding

postulate -- Relation: Aggregation of -Individual Business Agent (Deployed Business Agent Part) -
  aggregationOfIndividualBusinessAgentDeployedBusinessAgentPart : classOfOrderedRelation  DeployedBusinessAgentPart IndividualBusinessAgent

-- Relation derived from the composability of Deployed Business Agent Part, by mathematical composition
deployedBusinessAgentPart : classOfOrderedRelation  IndividualBusinessAgent IndividualBusinessAgent
deployedBusinessAgentPart = membershipOfDeployedBusinessAgentPart ∘ aggregationOfIndividualBusinessAgentDeployedBusinessAgentPart