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

Data Quality Indicator: 

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

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

module 003f595c64775717 where -- ========== Data Quality Indicator

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 8f46e8eb64b7719a public -- Key Indicator
open import b90aeac8600e619f public -- Data Assurance Case

postulate
  DataQualityIndicator : ClassOfBoundedIndividual

postulate --  DataQualityIndicator is subTypeOf KeyIndicator
  st-003f596b64775773 : DataQualityIndicator ⊏⋆ₑ KeyIndicator

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

{- Monitored Data Assurance Case:  -}
-- Aggregate Member : Monitored Data Assurance Case
postulate
  MonitoredDataAssuranceCase : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Monitored Data Assurance Case-
  membershipOfMonitoredDataAssuranceCase-nestingbinding : DataQualityIndicator ⊏ₑ  LexicalScope {lzero}
  membershipOfMonitoredDataAssuranceCase : classOfNestingRelation {ct = MonitoredDataAssuranceCase}  membershipOfMonitoredDataAssuranceCase-nestingbinding

postulate -- Relation: Aggregation of -Data Assurance Case (Monitored Data Assurance Case) -
  aggregationOfDataAssuranceCaseMonitoredDataAssuranceCase : classOfOrderedRelation  MonitoredDataAssuranceCase DataAssuranceCase

-- Relation derived from the composability of Monitored Data Assurance Case, by mathematical composition
monitoredDataAssuranceCase : classOfMixedOrderRelation  DataQualityIndicator DataAssuranceCase
monitoredDataAssuranceCase = membershipOfMonitoredDataAssuranceCase ∘ aggregationOfDataAssuranceCaseMonitoredDataAssuranceCase