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

Enterprise Initiative: 
An Enterprise Initiative is a past, current or future state of the enterprise. Each stage represents an initiative comprising a purposeful set of activities whose primary purpose is focused on achieving a set of clearly defined objectives that may transcend organisational boundaries and consequently require integrated team working under the direction of an Architecture Governance Committee.
 - ============================== -}

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

module 036a3de3548f229e where -- ========== Enterprise Initiative

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 0ffeec41600be08a public -- Initiative
open import 203b8fdb5a5f43dd public -- Concept Domain Map
open import 25c0a25061e2fd5a public -- Software System Environment
open import 7c4097c855271c8e public -- Conceptual Environment
open import c189f8c868ae5b73 public -- Business Capability Map
open import fe1c250d678803b6 public -- Individual Resource Behavior
open import 21ed240a689c08df public -- Value Proposition
open import 56ea5ff966047632 public -- Product

postulate
  EnterpriseInitiative : ClassOfBoundedIndividual

postulate --  EnterpriseInitiative is subTypeOf Initiative
  st-18a827fa5eeb6ed2 : EnterpriseInitiative ⊏⋆ₑ Initiative

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

{- Enterprise Concept Map: 
Top level concept map of the enterprise or of one its transformation stages.
 -}
postulate -- Relation: Enterprise Concept Map
  enterpriseConceptMap : classOfMixedOrderRelation  EnterpriseInitiative ConceptDomainMap

{- Enterprise IT Ecosystem: 
Software System Environment of the enterprise or of one of its transformation stage.
 -}
postulate -- Relation: Enterprise IT Ecosystem
  enterpriseITEcosystem : classOfMixedOrderRelation  EnterpriseInitiative SOftwareSystemEnvironment

{- Enterprise Conceptual Environment: 
Conceptual Environment of the enterprise or of one of its transformation stages.This Conceptual Environment defines the enterprise Conceptual Environments ()
 -}
postulate -- Relation: Enterprise Conceptual Environment
  enterpriseConceptualEnvironment : classOfMixedOrderRelation  EnterpriseInitiative ConceptualEnvironment

{- Enterprise Capability Map:  -}
postulate -- Relation: Enterprise Capability Map
  enterpriseCapabilityMap : classOfMixedOrderRelation  EnterpriseInitiative BusinessCapabilityMap

{- Enterprise Course of Action: 
A plan recognized by an enterprise as being essential to achieving its goals - i.e. a strategic specification of what the enterprise does. In other words, a Course of Action channels efforts towards Desired Results.Business Capabilities might be required by an Enterprise to conduct its Courses of Action.
 -}
-- Aggregate Member : Enterprise Course of Action
postulate
  EnterpriseCourseOfAction : ClassOfIndividual

postulate -- NestingRelation: Membership of -Enterprise Course of Action-
  membershipOfEnterpriseCourseOfAction-nestingbinding : EnterpriseInitiative ⊏ₑ  LexicalScope {lzero}
  membershipOfEnterpriseCourseOfAction : classOfNestingRelation {ct = EnterpriseCourseOfAction}  membershipOfEnterpriseCourseOfAction-nestingbinding

postulate -- Relation: Aggregation of -Individual Resource Behavior (Enterprise Course of Action) -
  aggregationOfIndividualResourceBehaviorEnterpriseCourseOfAction : classOfOrderedRelation  EnterpriseCourseOfAction IndividualResourceBehavior

-- Relation derived from the composability of Enterprise Course of Action, by mathematical composition
enterpriseCourseOfAction : classOfOrderedRelation  EnterpriseInitiative IndividualResourceBehavior
enterpriseCourseOfAction = membershipOfEnterpriseCourseOfAction ∘ aggregationOfIndividualResourceBehaviorEnterpriseCourseOfAction


{- Enterprise Desired Result:  -}
-- Aggregate Member : Enterprise Desired Result
postulate
  EnterpriseDesiredResult : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Enterprise Desired Result-
  membershipOfEnterpriseDesiredResult-nestingbinding : EnterpriseInitiative ⊏ₑ  LexicalScope {lzero}
  membershipOfEnterpriseDesiredResult : classOfNestingRelation {ct = EnterpriseDesiredResult}  membershipOfEnterpriseDesiredResult-nestingbinding

postulate -- Relation: Aggregation of -Value Proposition (Enterprise Desired Result) -
  aggregationOfValuePropositionEnterpriseDesiredResult : classOfOrderedRelation  EnterpriseDesiredResult ValueProposition

-- Relation derived from the composability of Enterprise Desired Result, by mathematical composition
enterpriseDesiredResult : classOfMixedOrderRelation  EnterpriseInitiative ValueProposition
enterpriseDesiredResult = membershipOfEnterpriseDesiredResult ∘ aggregationOfValuePropositionEnterpriseDesiredResult


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

postulate -- NestingRelation: Membership of -Product-
  membershipOfProduct-nestingbinding : EnterpriseInitiative ⊏ₑ  LexicalScope {lzero}
  membershipOfProduct : classOfNestingRelation {ct = Product}  membershipOfProduct-nestingbinding

postulate -- Relation: Aggregation of -Product (Product) -
  aggregationOfProductProduct : classOfOrderedRelation  Product Product

-- Relation derived from the composability of Product, by mathematical composition
product : classOfMixedOrderRelation  EnterpriseInitiative Product
product = membershipOfProduct ∘ aggregationOfProductProduct