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

Agent Type Environment: 
An Agent Type Environment is an Operating Eco-System which defines the interactions (Service Channel) of an Agent Type with its partners (Partner Agent).
 - ============================== -}

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

module d6cd0fd95ab9744b where -- ========== Agent Type Environment

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import ca35f48a5fc48686 public -- Operating Eco-System
open import 24ae31b55ed1c66d public -- Service Interface
open import 79368381561716a6 public -- Agent Type
open import ca3513af5fc59413 public -- Environment Interaction Process Type

postulate
  AgentTypeEnvironment : ClassOfClassOfBoundedIndividual

postulate --  AgentTypeEnvironment is subTypeOf OperatingEcoSystem
  st-d6cd10f85ab974f9 : AgentTypeEnvironment ⊏⋆ₑ OperatingEcoSystem

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

{- Specialized Operating Environment:  -}
postulate -- Relation: Specialized Operating Environment
  specializedOperatingEnvironment : classOfOrderedRelation  AgentTypeEnvironment AgentTypeEnvironment

{- Realized Operating Environment:  -}
postulate -- Relation: Realized Operating Environment
  realizedOperatingEnvironment : classOfOrderedRelation  AgentTypeEnvironment AgentTypeEnvironment

{- Service Channel:  -}
-- Aggregate Member : Service Channel
postulate
  ServiceChannel : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Service Channel-
  membershipOfServiceChannel-nestingbinding : AgentTypeEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfServiceChannel : classOfNestingRelation {ct = ServiceChannel}  membershipOfServiceChannel-nestingbinding

postulate -- Relation: Aggregation of -Service Interface (Service Channel) -
  aggregationOfServiceInterfaceServiceChannel : classOfOrderedRelation  ServiceChannel ServiceInterface

-- Relation derived from the composability of Service Channel, by mathematical composition
serviceChannel : classOfOrderedRelation  AgentTypeEnvironment ServiceInterface
serviceChannel = membershipOfServiceChannel ∘ aggregationOfServiceInterfaceServiceChannel


{- Participant Agent:  -}
-- Aggregate Member : Participant Agent
postulate
  ParticipantAgent : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Participant Agent-
  membershipOfParticipantAgent-nestingbinding : AgentTypeEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfParticipantAgent : classOfNestingRelation {ct = ParticipantAgent}  membershipOfParticipantAgent-nestingbinding

postulate -- Relation: Aggregation of -Agent Type (Participant Agent) -
  aggregationOfAgentTypeParticipantAgent : classOfOrderedRelation  ParticipantAgent AgentType

-- Relation derived from the composability of Participant Agent, by mathematical composition
participantAgent : classOfOrderedRelation  AgentTypeEnvironment AgentType
participantAgent = membershipOfParticipantAgent ∘ aggregationOfAgentTypeParticipantAgent


{- Performed Interaction: 
set of interactions processes performed in the context of an Operating Eco-System.
 -}
-- Aggregate Member : Performed Interaction
postulate
  PerformedInteraction : ClassOfClassOfIndividual

postulate -- NestingRelation: 26CB2D596961099C
  26CB2D596961099C-nestingbinding : AgentTypeEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  26CB2D596961099C : classOfNestingRelation {ct = PerformedInteraction}  26CB2D596961099C-nestingbinding

postulate -- Relation: Aggregation of -Environment Interaction Process Type (Performed Interaction) -
  aggregationOfEnvironmentInteractionProcessTypePerformedInteraction : classOfOrderedRelation  PerformedInteraction EnvironmentInteractionProcessType

-- Relation derived from the composability of Performed Interaction, by mathematical composition
performedInteraction : classOfOrderedRelation  AgentTypeEnvironment EnvironmentInteractionProcessType
performedInteraction = 26CB2D596961099C ∘ aggregationOfEnvironmentInteractionProcessTypePerformedInteraction


{- Subject Agent:  -}
-- Aggregate Member : Subject Agent
postulate
  SubjectAgent : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Subject Agent-
  membershipOfSubjectAgent-nestingbinding : AgentTypeEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfSubjectAgent : classOfNestingRelation {ct = SubjectAgent}  membershipOfSubjectAgent-nestingbinding

postulate -- Relation: Aggregation of -Agent Type (Subject Agent) -
  aggregationOfAgentTypeSubjectAgent : classOfOrderedRelation  SubjectAgent AgentType

-- Relation derived from the composability of Subject Agent, by mathematical composition
subjectAgent : classOfOrderedRelation  AgentTypeEnvironment AgentType
subjectAgent = membershipOfSubjectAgent ∘ aggregationOfAgentTypeSubjectAgent


{- Partner Agent:  -}
-- Aggregate Member : Partner Agent
postulate
  PartnerAgent : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Partner Agent-
  membershipOfPartnerAgent-nestingbinding : AgentTypeEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfPartnerAgent : classOfNestingRelation {ct = PartnerAgent}  membershipOfPartnerAgent-nestingbinding

postulate -- Relation: Aggregation of -Agent Type (Partner Agent) -
  aggregationOfAgentTypePartnerAgent : classOfOrderedRelation  PartnerAgent AgentType

-- Relation derived from the composability of Partner Agent, by mathematical composition
partnerAgent : classOfOrderedRelation  AgentTypeEnvironment AgentType
partnerAgent = membershipOfPartnerAgent ∘ aggregationOfAgentTypePartnerAgent