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

Individual Behavior: 
An Individual Behavior is an actual instance of Behavior Type that is bounded in time.

Documentation : https://framework.sysfeat.com/pages/e9af119866e86785.htm

External references:
  OpenGroup - ArchiMate - Behavior-Elements: https://pubs.opengroup.org/architecture/archimate32-doc/ch-Generic-Metamodel.html#sec-Behavior-Elements
  ISO 15926 - Activity: https://15926.blog/topics/data-model/index.htm#Activity
 - ============================== -}

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

module SysFEAT.SOF.e9af119866e86785 where -- ========== Individual Behavior

open import Agda.Primitive
open import SysFEAT.SOF.9f61cf9166833fb7 public -- Individual Operating Asset
open import SysFEAT.SOF.986cd4ec5ffca3ac public -- Behavior Type
open import SysFEAT.SOF.9e3837e46192fcad public -- Individual Agent

IndividualBehavior : ClassOfBoundedIndividual
IndividualBehavior = BoundedIndividual


--  IndividualBehavior is subTypeOf IndividualOperatingAsset
st-e9af119866e86785-9f61cf9166833fb7 : IndividualBehavior ⊏ₑ IndividualOperatingAsset
st-e9af119866e86785-9f61cf9166833fb7 = polySubTypeOf-identity


-- == Relations =======================

-- -------------------------------------------------------------------------------------------- 
{- Individual Behavior Part: 
An Individual Behavior Part is the Aggregate Holonymy of an Individual Behavior in a parent Individual Behavior.
-}
-- Aggregate Member : Individual Behavior Part
IndividualBehaviorPart : AggregateHolonymyType
IndividualBehaviorPart = AggregateHolonymy



--  IndividualBehaviorPart is subTypeOf IndividualOperatingPart
st-ffb9011b68d36c96-d8ee780d68d224c2 : IndividualBehaviorPart ⊏ₑ IndividualOperatingPart
st-ffb9011b68d36c96-d8ee780d68d224c2 = polySubTypeOf-identity

--  IndividualBehaviorPart is subTypeOf IndividualBehavior
st-ffb9011b68d36c96-e9af119866e86785 : IndividualBehaviorPart ⊏ₑ IndividualBehavior
st-ffb9011b68d36c96-e9af119866e86785 = polySubTypeOf-identity

-- Membership relation
membershipOfIndividualBehaviorPart :  Linkage IndividualBehavior IndividualBehaviorPart
membershipOfIndividualBehaviorPart = make_upwardNestingRelation "individualBehaviorPart membership" "nested individualBehaviorPart"

-- Aggregation relation
aggregationOfIndividualBehaviorIndividualBehaviorPart :  Linkage IndividualBehaviorPart IndividualBehavior
aggregationOfIndividualBehaviorIndividualBehaviorPart = make_Relation "IndividualBehavior aggregation" "aggregated IndividualBehavior"

{- individualBehaviorPart : derived relation obtained by composing
   membershipOfIndividualBehaviorPart and aggregationOfIndividualBehaviorIndividualBehaviorPart
   It directly links an Individual Behavior to the final aggregated IndividualBehavior
   hiding the reifying IndividualBehaviorPart
-}
individualBehaviorPart : Linkage IndividualBehavior IndividualBehavior
individualBehaviorPart = membershipOfIndividualBehaviorPart  ∘  aggregationOfIndividualBehaviorIndividualBehaviorPart



-- -------------------------------------------------------------------------------------------- 
{- Individual Participant: 
An  Individual Participant is
-}
-- Aggregate Member : Individual Participant
IndividualParticipant : AgentType
IndividualParticipant = IndividualAgent



--  IndividualParticipant is subTypeOf IndividualOperatingPart
st-ffb9014568d36d76-d8ee780d68d224c2 : IndividualParticipant ⊏ₑ IndividualOperatingPart
st-ffb9014568d36d76-d8ee780d68d224c2 = polySubTypeOf-identity

--  IndividualParticipant is subTypeOf IndividualAgent
st-ffb9014568d36d76-9e3837e46192fcad : IndividualParticipant ⊏ₑ IndividualAgent
st-ffb9014568d36d76-9e3837e46192fcad = polySubTypeOf-identity

-- Membership relation
membershipOfIndividualParticipant :  Linkage IndividualBehavior IndividualParticipant
membershipOfIndividualParticipant = make_upwardNestingRelation "individualParticipant membership" "nested individualParticipant"

-- Aggregation relation
aggregationOfIndividualAgentIndividualParticipant :  Linkage IndividualParticipant IndividualAgent
aggregationOfIndividualAgentIndividualParticipant = make_Relation "IndividualAgent aggregation" "aggregated IndividualAgent"

{- individualParticipant : derived relation obtained by composing
   membershipOfIndividualParticipant and aggregationOfIndividualAgentIndividualParticipant
   It directly links an Individual Behavior to the final aggregated IndividualAgent
   hiding the reifying IndividualParticipant
-}
individualParticipant : Linkage IndividualBehavior IndividualAgent
individualParticipant = membershipOfIndividualParticipant  ∘  aggregationOfIndividualAgentIndividualParticipant