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

Application Portfolio: 
Application Portfolios are Enduring Initiatives aimed at managing a set of Applications delivering functionalities required by enterprise operations.The purpose of Application Portfolios is efficiency: managed Applications must provide expected functionalities in the best cost / performance ratio.
 - ============================== -}

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

module 1ce3429d5c48982e where -- ========== Application Portfolio

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 26b8889c5eea8ab7 public -- Asset Portfolio
open import 052015c666474dfe public -- Application Portfolio Stage
open import bcebd8e9549144db public -- Application

postulate
  ApplicationPortfolio : ClassOfBoundedIndividual

postulate --  ApplicationPortfolio is subTypeOf AssetPortfolio
  st-6ce61b895ef3827b : ApplicationPortfolio ⊏⋆ₑ AssetPortfolio

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

{- Roadmap:  -}
postulate -- Relation: Roadmap
  roadmap : classOfOrderedRelation  ApplicationPortfolio ApplicationPortfolioStage

{- Managed Application: 
A Managed Application represents the status of an Application under the management of an Application Portfolio.
 -}
-- Aggregate Member : Managed Application
postulate
  ManagedApplication : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Managed Application-
  membershipOfManagedApplication-nestingbinding : ApplicationPortfolio ⊏ₑ  LexicalScope {lzero}
  membershipOfManagedApplication : classOfNestingRelation {ct = ManagedApplication}  membershipOfManagedApplication-nestingbinding

postulate -- Relation: Aggregation of -Application (Managed Application) -
  aggregationOfApplicationManagedApplication : classOfOrderedRelation  ManagedApplication Application

-- Relation derived from the composability of Managed Application, by mathematical composition
managedApplication : classOfMixedOrderRelation  ApplicationPortfolio Application
managedApplication = membershipOfManagedApplication ∘ aggregationOfApplicationManagedApplication