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

Conceptual Environment: 
A Conceptual Environment  is an operating context which defines the interactions (Business Interaction) of an Operating Domain with its partners (Customers).
 - ============================== -}

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

module 7c4097c855271c8e where -- ========== Conceptual Environment

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import f97e3e30632b31c1 public -- Conceptual Ecosystem
open import d6cd0fd95ab9744b public -- Agent Type Environment
open import 9dcea2655ec768ee public -- Business Service Interface
open import 08d180d4678a2c8f public -- Supplier
open import 9810b060551137d0 public -- Operating Domain
open import 08d181af678a2d51 public -- Customer

postulate
  ConceptualEnvironment : ClassOfClassOfBoundedIndividual

postulate --  ConceptualEnvironment is subTypeOf ConceptualEcosystem
  st-6a70b9af67876384 : ConceptualEnvironment ⊏⋆ₑ ConceptualEcosystem

postulate --  ConceptualEnvironment is subTypeOf AgentTypeEnvironment
  st-ebcff5365ad8b891 : ConceptualEnvironment ⊏⋆ₑ AgentTypeEnvironment

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

{- Specialized Operating Model Environment:  -}
postulate -- Relation: Specialized Operating Model Environment
  specializedOperatingModelEnvironment : classOfOrderedRelation  ConceptualEnvironment ConceptualEnvironment

{- Business Interaction:  -}
-- Aggregate Member : Business Interaction
postulate
  BusinessInteraction : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Business Interaction-
  membershipOfBusinessInteraction-nestingbinding : ConceptualEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfBusinessInteraction : classOfNestingRelation {ct = BusinessInteraction}  membershipOfBusinessInteraction-nestingbinding

postulate -- Relation: Aggregation of -Business Service Interface (Business Interaction) -
  aggregationOfBusinessServiceInterfaceBusinessInteraction : classOfOrderedRelation  BusinessInteraction BusinessServiceInterface

-- Relation derived from the composability of Business Interaction, by mathematical composition
businessInteraction : classOfOrderedRelation  ConceptualEnvironment BusinessServiceInterface
businessInteraction = membershipOfBusinessInteraction ∘ aggregationOfBusinessServiceInterfaceBusinessInteraction


{- Partner Supplier:  -}
-- Aggregate Member : Partner Supplier
postulate
  PartnerSupplier : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Partner Supplier-
  membershipOfPartnerSupplier-nestingbinding : ConceptualEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfPartnerSupplier : classOfNestingRelation {ct = PartnerSupplier}  membershipOfPartnerSupplier-nestingbinding

postulate -- Relation: Aggregation of -Supplier (Partner Supplier) -
  aggregationOfSupplierPartnerSupplier : classOfOrderedRelation  PartnerSupplier Supplier

-- Relation derived from the composability of Partner Supplier, by mathematical composition
partnerSupplier : classOfOrderedRelation  ConceptualEnvironment Supplier
partnerSupplier = membershipOfPartnerSupplier ∘ aggregationOfSupplierPartnerSupplier


{- Subject Activity Domain:  -}
-- Aggregate Member : Subject Activity Domain
postulate
  SubjectActivityDomain : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Subject Activity Domain-
  membershipOfSubjectActivityDomain-nestingbinding : ConceptualEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfSubjectActivityDomain : classOfNestingRelation {ct = SubjectActivityDomain}  membershipOfSubjectActivityDomain-nestingbinding

postulate -- Relation: Aggregation of -Operating Domain (Subject Activity Domain) -
  aggregationOfOperatingDomainSubjectActivityDomain : classOfOrderedRelation  SubjectActivityDomain OperatingDomain

-- Relation derived from the composability of Subject Activity Domain, by mathematical composition
subjectActivityDomain : classOfOrderedRelation  ConceptualEnvironment OperatingDomain
subjectActivityDomain = membershipOfSubjectActivityDomain ∘ aggregationOfOperatingDomainSubjectActivityDomain


{- Customer:  -}
-- Aggregate Member : Customer
postulate
  Customer : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Customer-
  membershipOfCustomer-nestingbinding : ConceptualEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfCustomer : classOfNestingRelation {ct = Customer}  membershipOfCustomer-nestingbinding

postulate -- Relation: Aggregation of -Customer (Customer) -
  aggregationOfCustomerCustomer : classOfOrderedRelation  Customer Customer

-- Relation derived from the composability of Customer, by mathematical composition
customer : classOfOrderedRelation  ConceptualEnvironment Customer
customer = membershipOfCustomer ∘ aggregationOfCustomerCustomer