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

Business Asset: 
Business Assets are Resource Functional Assets that define how Business Outcome Events are specified, produced and consumed.
 - ============================== -}

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

module 6a70b9f6678763db where -- ========== Business Asset

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 9bec9fbf66fb0d6f public -- Resource Functional Asset
open import 0e55230266f12252 public -- Operational Risk Type

postulate
  BusinessAsset : ClassOfClassOfBoundedIndividual

postulate --  BusinessAsset is subTypeOf ResourceFunctionalAsset
  st-6a70bb636787650b : BusinessAsset ⊏⋆ₑ ResourceFunctionalAsset

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

{- Operational Risk: 
An Operational Risk is a kind of Risk that refers to the potential for loss resulting from inadequate structure or behavior of a Business Operating Asset.
 -}
-- Aggregate Member : Operational Risk
postulate
  OperationalRisk : ThirdOrderClass

postulate -- NestingRelation: Membership of -Operational Risk-
  membershipOfOperationalRisk-nestingbinding : BusinessAsset ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfOperationalRisk : classOfNestingRelation {ct = OperationalRisk}  membershipOfOperationalRisk-nestingbinding

postulate -- Relation: Aggregation of -Operational Risk Type (Operational Risk) -
  aggregationOfOperationalRiskTypeOperationalRisk : classOfOrderedRelation  OperationalRisk OperationalRiskType

-- Relation derived from the composability of Operational Risk, by mathematical composition
operationalRisk : classOfMixedOrderRelation  BusinessAsset OperationalRiskType
operationalRisk = membershipOfOperationalRisk ∘ aggregationOfOperationalRiskTypeOperationalRisk