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

Regulation Article: 
Compulsory Policy, define by law, that is not directly enforceable whose purpose is guide enterprise activities.Regulation Articles are classified by Regulation section in the context of a Regulatory Framework.
 - ============================== -}

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

module 190c57d568976e60 where -- ========== Regulation Article

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 190c7429689664b5 public -- Policy
open import 4b947d2068a49dbb public -- Regulatory Asset
open import 952eb284672864df public -- Regulation section

postulate
  RegulationArticle : PropertyType

postulate --  RegulationArticle is subTypeOf Policy
  st-af66197a6307d559 : RegulationArticle ⊏⋆ₑ Policy

postulate --  RegulationArticle is subTypeOf RegulatoryAsset
  st-4b947ee068a4a05d : RegulationArticle ⊏ₐₑ RegulatoryAsset {lsuc(lzero)}

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

{- Parent Section:  -}
postulate -- Relation: Parent Section
  parentSection : classOfMixedOrderRelation  RegulationArticle Regulationsection

{- Specialized Article:  -}
postulate -- Relation: Specialized Article
  specializedArticle : classOfOrderedRelation  RegulationArticle RegulationArticle