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

Data Catalog: 
A Data Catalog is an Assurance System of Data Assets, ensuring understanding,  trust, compliance and confidence of enterprise data. This includes:1. Relationship with Enterprise Glossary to provide business context to metadata.2. Data policy definition and enforcement to ensure data quality.3. Data Lineage to master data provenance: where data comes from, how data is transformed, and where it is used.
 - ============================== -}

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

module 9152d8875ed741ef where -- ========== Data Catalog

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 07ca18d25dd85477 public -- Assurance System
open import 44226d6561819b50 public -- Data Assurance Instrument
open import affeb2255f6051e6 public -- Deployed Data Store
open import 203b8fdb5a5f43dd public -- Concept Domain Map
open import b90aeac8600e619f public -- Data Assurance Case
open import 190c7429689664b5 public -- Policy
open import 98159f6b5f682d1e public -- Data Quality Policy

postulate
  DataCatalog : ClassOfBoundedIndividual

postulate --  DataCatalog is subTypeOf AssuranceSystem
  st-c830d018617a4c38 : DataCatalog ⊏⋆ₑ AssuranceSystem

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

{- Owned Data Resource:  -}
postulate -- Relation: Owned Data Resource
  ownedDataResource : classOfOrderedRelation  DataCatalog DataAssuranceInstrument

{- Managed Data Store:  -}
postulate -- Relation: Managed Data Store
  managedDataStore : classOfOrderedRelation  DataCatalog DeployedDataStore

{- Business Concept Scope:  -}
postulate -- Relation: Business Concept Scope
  businessConceptScope : classOfMixedOrderRelation  DataCatalog ConceptDomainMap

{- Owned Data Assurance Case:  -}
postulate -- Relation: Owned Data Assurance Case
  ownedDataAssuranceCase : classOfMixedOrderRelation  DataCatalog DataAssuranceCase

{- Enforced Policy:  -}
-- Aggregate Member : Enforced Policy
postulate
  EnforcedPolicy : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Enforced Policy-
  membershipOfEnforcedPolicy-nestingbinding : DataCatalog ⊏ₑ  LexicalScope {lzero}
  membershipOfEnforcedPolicy : classOfNestingRelation {ct = EnforcedPolicy}  membershipOfEnforcedPolicy-nestingbinding

postulate -- Relation: Aggregation of -Policy (Enforced Policy) -
  aggregationOfPolicyEnforcedPolicy : classOfOrderedRelation  EnforcedPolicy Policy

-- Relation derived from the composability of Enforced Policy, by mathematical composition
enforcedPolicy : classOfMixedOrderRelation  DataCatalog Policy
enforcedPolicy = membershipOfEnforcedPolicy ∘ aggregationOfPolicyEnforcedPolicy


{- Controled Data Policy:  -}
-- Aggregate Member : Controled Data Policy
postulate
  ControledDataPolicy : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Controled Data Policy-
  membershipOfControledDataPolicy-nestingbinding : DataCatalog ⊏ₑ  LexicalScope {lzero}
  membershipOfControledDataPolicy : classOfNestingRelation {ct = ControledDataPolicy}  membershipOfControledDataPolicy-nestingbinding

postulate -- Relation: Aggregation of -Data Quality Policy (Controled Data Policy) -
  aggregationOfDataQualityPolicyControledDataPolicy : classOfOrderedRelation  ControledDataPolicy DataQualityPolicy

-- Relation derived from the composability of Controled Data Policy, by mathematical composition
controledDataPolicy : classOfMixedOrderRelation  DataCatalog DataQualityPolicy
controledDataPolicy = membershipOfControledDataPolicy ∘ aggregationOfDataQualityPolicyControledDataPolicy