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

Operational Assurance Case: 

 - ============================== -}

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

module f1606a8267d86149 where -- ========== Operational Assurance Case

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 07ca19e95dd854e9 public -- Assurance Case
open import f8e61da0621db6fa public -- Resource Operating Asset
open import f1606adf67d861a5 public -- Operating Risk Type

postulate
  OperationalAssuranceCase : ClassOfClassOfBoundedIndividual

postulate --  OperationalAssuranceCase is subTypeOf AssuranceCase
  st-f1606b7c67d862c3 : OperationalAssuranceCase ⊏⋆ₑ AssuranceCase

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

{- Resource Operating Asset:  -}
-- Aggregate Member : Resource Operating Asset
postulate
  ResourceOperatingAsset : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Resource Operating Asset-
  membershipOfResourceOperatingAsset-nestingbinding : OperationalAssuranceCase ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfResourceOperatingAsset : classOfNestingRelation {ct = ResourceOperatingAsset}  membershipOfResourceOperatingAsset-nestingbinding

postulate -- Relation: Aggregation of -Resource Operating Asset (Resource Operating Asset) -
  aggregationOfResourceOperatingAssetResourceOperatingAsset : classOfOrderedRelation  ResourceOperatingAsset ResourceOperatingAsset

-- Relation derived from the composability of Resource Operating Asset, by mathematical composition
resourceOperatingAsset : classOfOrderedRelation  OperationalAssuranceCase ResourceOperatingAsset
resourceOperatingAsset = membershipOfResourceOperatingAsset ∘ aggregationOfResourceOperatingAssetResourceOperatingAsset


{- Mitigated Operational Risk:  -}
-- Aggregate Member : Mitigated Operational Risk
postulate
  MitigatedOperationalRisk : ThirdOrderClass

postulate -- NestingRelation: Membership of -Mitigated Operational Risk-
  membershipOfMitigatedOperationalRisk-nestingbinding : OperationalAssuranceCase ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfMitigatedOperationalRisk : classOfNestingRelation {ct = MitigatedOperationalRisk}  membershipOfMitigatedOperationalRisk-nestingbinding

postulate -- Relation: Aggregation of -Operating Risk Type (Mitigated Operational Risk) -
  aggregationOfOperatingRiskTypeMitigatedOperationalRisk : classOfOrderedRelation  MitigatedOperationalRisk OperatingRiskType

-- Relation derived from the composability of Mitigated Operational Risk, by mathematical composition
mitigatedOperationalRisk : classOfMixedOrderRelation  OperationalAssuranceCase OperatingRiskType
mitigatedOperationalRisk = membershipOfMitigatedOperationalRisk ∘ aggregationOfOperatingRiskTypeMitigatedOperationalRisk