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

Conceptual Service Interface: 
A Conceptual Service Interface is a communication behavior that describes a typical course of interactions intended to produce Conceptual Outcome Events, through the involvement of Conceptual Agents.
 - ============================== -}

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

module 219162176786411d where -- ========== Conceptual Service Interface

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 24ae31b55ed1c66d public -- Service Interface
open import f97e3119632b25f8 public -- Conceptual Behavior
open import 21916383678642d1 public -- Conceptual Outcome Event

postulate
  ConceptualServiceInterface : ClassOfClassOfIndividual

postulate --  ConceptualServiceInterface is subTypeOf ServiceInterface
  st-2191622767864183 : ConceptualServiceInterface ⊏⋆ₑ ServiceInterface

postulate --  ConceptualServiceInterface is subTypeOf ConceptualBehavior
  st-cb94f21f68185f4c : ConceptualServiceInterface ⊏⋆ₑ ConceptualBehavior

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

{- Conceptual Flow: 
A Conceptual Flow is an Conceptual Outcome Event event that occurs between the consumer and the provider participant of a Conceptual Service Interface.
 -}
-- Aggregate Member : Conceptual Flow
postulate
  ConceptualFlow : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Conceptual Flow-
  membershipOfConceptualFlow-nestingbinding : ConceptualServiceInterface ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfConceptualFlow : classOfNestingRelation {ct = ConceptualFlow}  membershipOfConceptualFlow-nestingbinding

postulate -- Relation: Aggregation of -Conceptual Outcome Event (Conceptual Flow) -
  aggregationOfConceptualOutcomeEventConceptualFlow : classOfOrderedRelation  ConceptualFlow ConceptualOutcomeEvent

-- Relation derived from the composability of Conceptual Flow, by mathematical composition
conceptualFlow : classOfOrderedRelation  ConceptualServiceInterface ConceptualOutcomeEvent
conceptualFlow = membershipOfConceptualFlow ∘ aggregationOfConceptualOutcomeEventConceptualFlow