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

Resource Behavior: 
An Resource Behavior is an Resource Operating Asset that describes any action or reaction of a Resource Agent Type to external or internal circumstances. This includes Resource Action Processes (actions), Resource Interaction Processs (stories) or service interactions (Business Service Interface).
 - ============================== -}

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

module 0185cd936221bd72 where -- ========== Resource Behavior

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import f8e61da0621db6fa public -- Resource Operating Asset
open import 986cd4ec5ffca3ac public -- Behavior Type
open import e2ef091962147ad7 public -- Resource Agent Type

postulate
  ResourceBehavior : ClassOfClassOfBoundedIndividual

postulate --  ResourceBehavior is subTypeOf ResourceOperatingAsset
  st-01850bb66222c5ff : ResourceBehavior ⊏⋆ₑ ResourceOperatingAsset

postulate --  ResourceBehavior is subTypeOf BehaviorType
  st-f08ff44566580d72 : ResourceBehavior ⊏⋆ₑ BehaviorType

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

{- Specialized Resource Behavior:  -}
postulate -- Relation: Specialized Resource Behavior
  specializedResourceBehavior : classOfOrderedRelation  ResourceBehavior ResourceBehavior

{- Resource Behavior Participant: 
A Resource Behavior Participant is the participation of a Resource Agent Type in a Resource Behavior.
 -}
-- Aggregate Member : Resource Behavior Participant
postulate
  ResourceBehaviorParticipant : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Resource Behavior Participant-
  membershipOfResourceBehaviorParticipant-nestingbinding : ResourceBehavior ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfResourceBehaviorParticipant : classOfNestingRelation {ct = ResourceBehaviorParticipant}  membershipOfResourceBehaviorParticipant-nestingbinding

postulate -- Relation: Aggregation of -Resource Agent Type (Resource Behavior Participant) -
  aggregationOfResourceAgentTypeResourceBehaviorParticipant : classOfOrderedRelation  ResourceBehaviorParticipant ResourceAgentType

-- Relation derived from the composability of Resource Behavior Participant, by mathematical composition
resourceBehaviorParticipant : classOfOrderedRelation  ResourceBehavior ResourceAgentType
resourceBehaviorParticipant = membershipOfResourceBehaviorParticipant ∘ aggregationOfResourceAgentTypeResourceBehaviorParticipant