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

Product Portfolio: 
A Product Portfolio is a Management System within an enterprise which purpose is to develop, maintain, transform and deliver a set of  Products of the Enterprise.
 - ============================== -}

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

module 215ccfab606c3a18 where -- ========== Product Portfolio

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 29df3f4060084c07 public -- Management System
open import 31257f5261dcdfca public -- Product Portfolio Stage
open import 56ea5ff966047632 public -- Product

postulate
  ProductPortfolio : ClassOfBoundedIndividual

postulate --  ProductPortfolio is subTypeOf ManagementSystem
  st-215c69dc606d58a4 : ProductPortfolio ⊏⋆ₑ ManagementSystem

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

{- Owned Portfolio Stage:  -}
postulate -- Relation: Owned Portfolio Stage
  ownedPortfolioStage : classOfOrderedRelation  ProductPortfolio ProductPortfolioStage

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

postulate -- NestingRelation: Membership of -Managed Product-
  membershipOfManagedProduct-nestingbinding : ProductPortfolio ⊏ₑ  LexicalScope {lzero}
  membershipOfManagedProduct : classOfNestingRelation {ct = ManagedProduct}  membershipOfManagedProduct-nestingbinding

postulate -- Relation: Aggregation of -Product (Managed Product) -
  aggregationOfProductManagedProduct : classOfOrderedRelation  ManagedProduct Product

-- Relation derived from the composability of Managed Product, by mathematical composition
managedProduct : classOfMixedOrderRelation  ProductPortfolio Product
managedProduct = membershipOfManagedProduct ∘ aggregationOfProductManagedProduct