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

Service Interface: 
A Service Interface is an interaction Behavior Type that describes a typical course of Flow Connections, coordinated by Behavioral Events and Outcome Events, and intended to produce Outcomes through the involvement of Agent Types.
 - ============================== -}

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

module 24ae31b55ed1c66d where -- ========== Service Interface

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 986cd4ec5ffca3ac public -- Behavior Type
open import 21c5276e655759fb public -- Operating Connection
open import 30223b5c5ec90c01 public -- Outcome Event

postulate
  ServiceInterface : ClassOfClassOfIndividual

postulate --  ServiceInterface is subTypeOf BehaviorType
  st-56ea58726605a6c8 : ServiceInterface ⊏⋆ₑ BehaviorType

postulate --  ServiceInterface is subTypeOf OperatingConnection
  st-2b5b46d566ed59cd : ServiceInterface ⊏⋆ₑ OperatingConnection

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

{- Sub Service Interface:  -}
-- Aggregate Member : Sub Service Interface
postulate
  SubServiceInterface : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Sub Service Interface-
  membershipOfSubServiceInterface-nestingbinding : ServiceInterface ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfSubServiceInterface : classOfNestingRelation {ct = SubServiceInterface}  membershipOfSubServiceInterface-nestingbinding

postulate -- Relation: Aggregation of -Service Interface (Sub Service Interface) -
  aggregationOfServiceInterfaceSubServiceInterface : classOfOrderedRelation  SubServiceInterface ServiceInterface

-- Relation derived from the composability of Sub Service Interface, by mathematical composition
subServiceInterface : classOfOrderedRelation  ServiceInterface ServiceInterface
subServiceInterface = membershipOfSubServiceInterface ∘ aggregationOfServiceInterfaceSubServiceInterface


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

postulate -- NestingRelation: Membership of -Flow Connection-
  membershipOfFlowConnection-nestingbinding : ServiceInterface ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfFlowConnection : classOfNestingRelation {ct = FlowConnection}  membershipOfFlowConnection-nestingbinding

postulate -- Relation: Aggregation of -Outcome Event (Flow Connection) -
  aggregationOfOutcomeEventFlowConnection : classOfOrderedRelation  FlowConnection OutcomeEvent

-- Relation derived from the composability of Flow Connection, by mathematical composition
flowConnection : classOfOrderedRelation  ServiceInterface OutcomeEvent
flowConnection = membershipOfFlowConnection ∘ aggregationOfOutcomeEventFlowConnection