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

Conceptual Behavior: 
A Conceptual Behavior is a Conceptual Operating Asset that describes any action or reaction of a Conceptual Agent to external or internal circumstances. This includes Value Streams (actions), Conceptual Interaction Scenarios (stories) or Conceptual Service Interfaces.
 - ============================== -}

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

module f97e3119632b25f8 where -- ========== Conceptual Behavior

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import c8b2238961e5385a public -- Conceptual Operating Asset
open import 986cd4ec5ffca3ac public -- Behavior Type
open import 7c40987055271d04 public -- Conceptual Agent

postulate
  ConceptualBehavior : ClassOfClassOfBoundedIndividual

postulate --  ConceptualBehavior is subTypeOf ConceptualOperatingAsset
  st-f97e3ae9632b2f8f : ConceptualBehavior ⊏⋆ₑ ConceptualOperatingAsset

postulate --  ConceptualBehavior is subTypeOf BehaviorType
  st-6a70996267875a47 : ConceptualBehavior ⊏⋆ₑ BehaviorType

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

{- Conceptual Participant:  -}
-- Aggregate Member : Conceptual Participant
postulate
  ConceptualParticipant : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Conceptual Participant-
  membershipOfConceptualParticipant-nestingbinding : ConceptualBehavior ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfConceptualParticipant : classOfNestingRelation {ct = ConceptualParticipant}  membershipOfConceptualParticipant-nestingbinding

postulate -- Relation: Aggregation of -Conceptual Agent (Conceptual Participant) -
  aggregationOfConceptualAgentConceptualParticipant : classOfOrderedRelation  ConceptualParticipant ConceptualAgent

-- Relation derived from the composability of Conceptual Participant, by mathematical composition
conceptualParticipant : classOfOrderedRelation  ConceptualBehavior ConceptualAgent
conceptualParticipant = membershipOfConceptualParticipant ∘ aggregationOfConceptualAgentConceptualParticipant