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

Logical Software System: 
A Logical Software System is logical specification of a Business Software System, which is independant from the Business Software System physical implementation.For instance,  Human Resource ERP System  is a Logical Application System, while  SAP HR System ,  Sage HR System ,  Kronos HR System  are Application Systems.
 - ============================== -}

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

module 2558338d5c6d1d1b where -- ========== Logical Software System

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import d6cd02865ab966e8 public -- Business Software System
open import 9dce9f8d5ec76311 public -- Application Interface
open import 461950e9560d4461 public -- Logical Data Domain

postulate
  LogicalSOftwareSystem : ClassOfClassOfBoundedIndividual

postulate --  LogicalSOftwareSystem is subTypeOf BusinessSOftwareSystem
  st-6c0485af61f2e95e : LogicalSOftwareSystem ⊏⋆ₑ BusinessSOftwareSystem

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

{- Logical Software Channel:  -}
-- Aggregate Member : Logical Software Channel
postulate
  LogicalSOftwareChannel : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Logical Software Channel-
  membershipOfLogicalSOftwareChannel-nestingbinding : LogicalSOftwareSystem ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfLogicalSOftwareChannel : classOfNestingRelation {ct = LogicalSOftwareChannel}  membershipOfLogicalSOftwareChannel-nestingbinding

postulate -- Relation: Aggregation of -Application Interface (Logical Software Channel) -
  aggregationOfApplicationInterfaceLogicalSOftwareChannel : classOfOrderedRelation  LogicalSOftwareChannel ApplicationInterface

-- Relation derived from the composability of Logical Software Channel, by mathematical composition
logicalSOftwareChannel : classOfOrderedRelation  LogicalSOftwareSystem ApplicationInterface
logicalSOftwareChannel = membershipOfLogicalSOftwareChannel ∘ aggregationOfApplicationInterfaceLogicalSOftwareChannel


{- Logical Data Store:  -}
-- Aggregate Member : Logical Data Store
postulate
  LogicalDataStore : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Logical Data Store-
  membershipOfLogicalDataStore-nestingbinding : LogicalSOftwareSystem ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfLogicalDataStore : classOfNestingRelation {ct = LogicalDataStore}  membershipOfLogicalDataStore-nestingbinding

postulate -- Relation: Aggregation of -Logical Data Domain (Logical Data Store) -
  aggregationOfLogicalDataDomainLogicalDataStore : classOfOrderedRelation  LogicalDataStore LogicalDataDomain

-- Relation derived from the composability of Logical Data Store, by mathematical composition
logicalDataStore : classOfOrderedRelation  LogicalSOftwareSystem LogicalDataDomain
logicalDataStore = membershipOfLogicalDataStore ∘ aggregationOfLogicalDataDomainLogicalDataStore


{- Logical Software Member:  -}
-- Aggregate Member : Logical Software Member
postulate
  LogicalSOftwareMember : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Logical Software Member-
  membershipOfLogicalSOftwareMember-nestingbinding : LogicalSOftwareSystem ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfLogicalSOftwareMember : classOfNestingRelation {ct = LogicalSOftwareMember}  membershipOfLogicalSOftwareMember-nestingbinding

postulate -- Relation: Aggregation of -Logical Software System (Logical Software Member) -
  aggregationOfLogicalSOftwareSystemLogicalSOftwareMember : classOfOrderedRelation  LogicalSOftwareMember LogicalSOftwareSystem

-- Relation derived from the composability of Logical Software Member, by mathematical composition
logicalSOftwareMember : classOfOrderedRelation  LogicalSOftwareSystem LogicalSOftwareSystem
logicalSOftwareMember = membershipOfLogicalSOftwareMember ∘ aggregationOfLogicalSOftwareSystemLogicalSOftwareMember