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

Operating Asset: 
An Operating Asset is a kind of Asset Block which is architectured accross Systemic Levels.
 - ============================== -}

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

module 0c4559c86a033792 where -- ========== Operating Asset

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 0eb95f356855bf94 public -- Asset Block
open import 52b05a616a104fab public -- Conceptualization Level
open import 0c450e776a031ff0 public -- Systemic Level

postulate
  OperatingAsset : ∀ {u} → ClassOfMixedOrderEntity u

postulate --  OperatingAsset is subTypeOf AssetBlock
  st-0c455d016a033cf0 : ∀ {u} → (OperatingAsset {u}) ⊏⋆ₑ (AssetBlock {u})

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

{- Dependent Conceptual Level:  -}
postulate -- Relation: Dependent Conceptual Level
  dependentConceptualLevel : ∀ {u} → classOfMixedOrderRelation  (OperatingAsset {u}) (ConceptualizationLevel {u})

{- Dependent Level Type: 
The Systemic Level that an Operating Asset is parametred by. 
 -}
postulate -- Relation: Dependent Level Type
  dependentLevelType : ∀ {u} → classOfMixedOrderRelation  (OperatingAsset {u}) (SystemicLevel {u})