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

Business Scenario: 
A Business Scenario is a story describing how Business-Entity (Department Type) interact wtiht its partners (Partner Department) to achieve Business Outcome Events in a specific Eco-System (Business Environment).This includes:1) A course of events represented by Resource Object Flows depicting the story towards the delivery of expected Business Outcome Events.2) Interacting  Business Entities (Department Types)  who participate to the story in the considered Eco-System.
 - ============================== -}

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

module c334dfca5ecb83dd where -- ========== Business Scenario

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 2b705f2661ba04de public -- Business Ecosystem
open import 2b6f337e61bae6d6 public -- Business Environment Scenario
open import 6f4b92d65fd3b49b public -- Business Environment
open import 08d181af678a2d51 public -- Customer
open import 7c408aa155270eea public -- Department Type

postulate
  BusinessScenario : ClassOfClassOfBoundedIndividual

postulate --  BusinessScenario is subTypeOf BusinessEcosystem
  st-2b70687a61ba1394 : BusinessScenario ⊏⋆ₑ BusinessEcosystem

postulate --  BusinessScenario is subTypeOf BusinessEnvironmentScenario
  st-0e0cf99a5f1f3c64 : BusinessScenario ⊏⋆ₑ BusinessEnvironmentScenario

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

{- Scenarized Business Environment:  -}
postulate -- Relation: Scenarized Business Environment
  scenarizedBusinessEnvironment : classOfOrderedRelation  BusinessScenario BusinessEnvironment

{- Served customer:  -}
-- Aggregate Member : Served customer
postulate
  Servedcustomer : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Served customer-
  membershipOfServedcustomer-nestingbinding : BusinessScenario ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfServedcustomer : classOfNestingRelation {ct = Servedcustomer}  membershipOfServedcustomer-nestingbinding

postulate -- Relation: Aggregation of -Customer (Served customer) -
  aggregationOfCustomerServedcustomer : classOfOrderedRelation  Servedcustomer Customer

-- Relation derived from the composability of Served customer, by mathematical composition
servedcustomer : classOfOrderedRelation  BusinessScenario Customer
servedcustomer = membershipOfServedcustomer ∘ aggregationOfCustomerServedcustomer


{- Subject-Department:  -}
-- Aggregate Member : Subject-Department
postulate
  SubjectDepartment : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Subject-Department-
  membershipOfSubjectDepartment-nestingbinding : BusinessScenario ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfSubjectDepartment : classOfNestingRelation {ct = SubjectDepartment}  membershipOfSubjectDepartment-nestingbinding

postulate -- Relation: Aggregation of -Department Type (Subject-Department) -
  aggregationOfDepartmentTypeSubjectDepartment : classOfOrderedRelation  SubjectDepartment DepartmentType

-- Relation derived from the composability of Subject-Department, by mathematical composition
subjectDepartment : classOfOrderedRelation  BusinessScenario DepartmentType
subjectDepartment = membershipOfSubjectDepartment ∘ aggregationOfDepartmentTypeSubjectDepartment


{- Partner Department:  -}
-- Aggregate Member : Partner Department
postulate
  PartnerDepartment : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Partner Department-
  membershipOfPartnerDepartment-nestingbinding : BusinessScenario ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfPartnerDepartment : classOfNestingRelation {ct = PartnerDepartment}  membershipOfPartnerDepartment-nestingbinding

postulate -- Relation: Aggregation of -Department Type (Partner Department) -
  aggregationOfDepartmentTypePartnerDepartment : classOfOrderedRelation  PartnerDepartment DepartmentType

-- Relation derived from the composability of Partner Department, by mathematical composition
partnerDepartment : classOfOrderedRelation  BusinessScenario DepartmentType
partnerDepartment = membershipOfPartnerDepartment ∘ aggregationOfDepartmentTypePartnerDepartment