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

Logical Data View: 
A Logical Data View a collection of filtered Logical Data Entitys.
 - ============================== -}

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

module 7eaa886156121e80 where -- ========== Logical Data View

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 2b5858b85eec51d9 public -- Logical Data Element
open import 325c32fc5eb02d02 public -- Data Entity
open import 4619527e560d45eb public -- Logical Data Entity

postulate
  LogicalDataView : ClassOfClassOfBoundedIndividual

postulate --  LogicalDataView is subTypeOf LogicalDataElement
  st-2b58597c5eec556d : LogicalDataView ⊏⋆ₑ LogicalDataElement

postulate --  LogicalDataView is subTypeOf DataEntity
  st-4478c335603c1b8c : LogicalDataView ⊏⋆ₑ DataEntity

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

{- Root Data Entity:  -}
-- Aggregate Member : Root Data Entity
postulate
  RootDataEntity : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Root Data Entity-
  membershipOfRootDataEntity-nestingbinding : LogicalDataView ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfRootDataEntity : classOfNestingRelation {ct = RootDataEntity}  membershipOfRootDataEntity-nestingbinding

postulate -- Relation: Aggregation of -Logical Data Entity (Root Data Entity) -
  aggregationOfLogicalDataEntityRootDataEntity : classOfOrderedRelation  RootDataEntity LogicalDataEntity

-- Relation derived from the composability of Root Data Entity, by mathematical composition
rootDataEntity : classOfOrderedRelation  LogicalDataView LogicalDataEntity
rootDataEntity = membershipOfRootDataEntity ∘ aggregationOfLogicalDataEntityRootDataEntity


{- Embedded Data Object:  -}
-- Aggregate Member : Embedded Data Object
postulate
  EmbeddedDataObject : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Embedded Data Object-
  membershipOfEmbeddedDataObject-nestingbinding : LogicalDataView ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfEmbeddedDataObject : classOfNestingRelation {ct = EmbeddedDataObject}  membershipOfEmbeddedDataObject-nestingbinding

postulate -- Relation: Aggregation of -Logical Data Element (Embedded Data Object) -
  aggregationOfLogicalDataElementEmbeddedDataObject : classOfOrderedRelation  EmbeddedDataObject LogicalDataElement

-- Relation derived from the composability of Embedded Data Object, by mathematical composition
embeddedDataObject : classOfOrderedRelation  LogicalDataView LogicalDataElement
embeddedDataObject = membershipOfEmbeddedDataObject ∘ aggregationOfLogicalDataElementEmbeddedDataObject


{- Referenced Entity:  -}
-- Aggregate Member : Referenced Entity
postulate
  ReferencedEntity : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Referenced Entity-
  membershipOfReferencedEntity-nestingbinding : LogicalDataView ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfReferencedEntity : classOfNestingRelation {ct = ReferencedEntity}  membershipOfReferencedEntity-nestingbinding

postulate -- Relation: Aggregation of -Logical Data Entity (Referenced Entity) -
  aggregationOfLogicalDataEntityReferencedEntity : classOfOrderedRelation  ReferencedEntity LogicalDataEntity

-- Relation derived from the composability of Referenced Entity, by mathematical composition
referencedEntity : classOfOrderedRelation  LogicalDataView LogicalDataEntity
referencedEntity = membershipOfReferencedEntity ∘ aggregationOfLogicalDataEntityReferencedEntity