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

Control Measure: 
A Control Measure is a Resource Operating Asset (agent or behavior) that is taken to prevent, eliminate or reduce the occurrence of a hazard that has been identified in the context of an Assurance Case.
 - ============================== -}

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

module f1600ddf67d8444b where -- ========== Control Measure

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import f8e61da0621db6fa public -- Resource Operating Asset
open import 4b9477ae68a4926d public -- Control Asset
open import 582e764f66f6a4cc public -- Control Measure Category
open import 01f1156d689b5ecc public -- Control Directive

postulate
  ControlMeasure : ClassOfClassOfBoundedIndividual

postulate --  ControlMeasure is subTypeOf ResourceOperatingAsset
  st-f1604eb267d85165 : ControlMeasure ⊏⋆ₑ ResourceOperatingAsset

postulate --  ControlMeasure is subTypeOf ControlAsset
  st-4b94798168a49542 : ControlMeasure ⊏ₐₑ ControlAsset {lsuc(lzero)}

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

{- Control Measure Category:  -}
postulate -- Relation: Control Measure Category
  controlMeasureCategory : classOfMixedOrderRelation  ControlMeasure ControlMeasureCategory

{- Enforced Control Directive:  -}
postulate -- Relation: Enforced Control Directive
  enforcedControlDirective : classOfOrderedRelation  ControlMeasure ControlDirective