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

Logical Operating Environment: 
A Logical Operating Environment presents a logical application system use context. It describes the interactions between the Logical Application System and its external partners, which allows it to fulfill its mission and ensure the expected functionalities.
 - ============================== -}

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

module 25582c685c6d1c93 where -- ========== Logical Operating Environment

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 25c0a25061e2fd5a public -- Software System Environment
open import 255833cb5c6d1d64 public -- Logical Application System

postulate
  LogicalOperatingEnvironment : ClassOfClassOfBoundedIndividual

postulate --  LogicalOperatingEnvironment is subTypeOf SOftwareSystemEnvironment
  st-2b585f5d5ef0fe20 : LogicalOperatingEnvironment ⊏⋆ₑ SOftwareSystemEnvironment

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

{- Partner Logical Part:  -}
-- Aggregate Member : Partner Logical Part
postulate
  PartnerLogicalPart : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Partner Logical Part-
  membershipOfPartnerLogicalPart-nestingbinding : LogicalOperatingEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfPartnerLogicalPart : classOfNestingRelation {ct = PartnerLogicalPart}  membershipOfPartnerLogicalPart-nestingbinding

postulate -- Relation: Aggregation of -Logical Application System (Partner Logical Part) -
  aggregationOfLogicalApplicationSystemPartnerLogicalPart : classOfOrderedRelation  PartnerLogicalPart LogicalApplicationSystem

-- Relation derived from the composability of Partner Logical Part, by mathematical composition
partnerLogicalPart : classOfOrderedRelation  LogicalOperatingEnvironment LogicalApplicationSystem
partnerLogicalPart = membershipOfPartnerLogicalPart ∘ aggregationOfLogicalApplicationSystemPartnerLogicalPart


{- Subject Logical Member:  -}
-- Aggregate Member : Subject Logical Member
postulate
  SubjectLogicalMember : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Subject Logical Member-
  membershipOfSubjectLogicalMember-nestingbinding : LogicalOperatingEnvironment ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfSubjectLogicalMember : classOfNestingRelation {ct = SubjectLogicalMember}  membershipOfSubjectLogicalMember-nestingbinding

postulate -- Relation: Aggregation of -Logical Application System (Subject Logical Member) -
  aggregationOfLogicalApplicationSystemSubjectLogicalMember : classOfOrderedRelation  SubjectLogicalMember LogicalApplicationSystem

-- Relation derived from the composability of Subject Logical Member, by mathematical composition
subjectLogicalMember : classOfOrderedRelation  LogicalOperatingEnvironment LogicalApplicationSystem
subjectLogicalMember = membershipOfSubjectLogicalMember ∘ aggregationOfLogicalApplicationSystemSubjectLogicalMember