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

Individual Resource Agent: 
An Individual Resource Agent is an Individual Operating Asset that exists in space/time and that is able to participate actively to Processes and/or to conduct Processes.
 - ============================== -}

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

module fe1c231267880201 where -- ========== Individual Resource Agent

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import fe1c24fa6788036e public -- Individual Resource Asset
open import 9e3837e46192fcad public -- Individual Agent
open import e2ef091962147ad7 public -- Resource Agent Type

postulate
  IndividualResourceAgent : ClassOfBoundedIndividual

postulate --  IndividualResourceAgent is subTypeOf IndividualResourceAsset
  st-fe1c27c1678807c6 : IndividualResourceAgent ⊏⋆ₑ IndividualResourceAsset

postulate --  IndividualResourceAgent is subTypeOf IndividualAgent
  st-fe1c25b167880564 : IndividualResourceAgent ⊏⋆ₑ IndividualAgent

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

{- Individual Resource Agent Part:  -}
-- Aggregate Member : Individual Resource Agent Part
postulate
  IndividualResourceAgentPart : ClassOfIndividual

postulate -- NestingRelation: Membership of -Individual Resource Agent Part-
  membershipOfIndividualResourceAgentPart-nestingbinding : IndividualResourceAgent ⊏ₑ  LexicalScope {lzero}
  membershipOfIndividualResourceAgentPart : classOfNestingRelation {ct = IndividualResourceAgentPart}  membershipOfIndividualResourceAgentPart-nestingbinding

postulate -- Relation: Aggregation of -Individual Resource Agent (Individual Resource Agent Part) -
  aggregationOfIndividualResourceAgentIndividualResourceAgentPart : classOfOrderedRelation  IndividualResourceAgentPart IndividualResourceAgent

-- Relation derived from the composability of Individual Resource Agent Part, by mathematical composition
individualResourceAgentPart : classOfOrderedRelation  IndividualResourceAgent IndividualResourceAgent
individualResourceAgentPart = membershipOfIndividualResourceAgentPart ∘ aggregationOfIndividualResourceAgentIndividualResourceAgentPart