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

Computing Device: 
A Computing Device is a physical or virtual computer that can host and run software code. Together with their Deployable Application Packages, they provide Information Outcomes.Examples: Computer Device, Computer Server.
 - ============================== -}

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

module 02f51209641c7ea4 where -- ========== Computing Device

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 26b8384f5eeae33c public -- Networking System
open import f4be0eda5ee1d6c0 public -- Computing System
open import d5e6d7eb5c464b21 public -- Deployable Application Package
open import d6a956495a395d28 public -- MicroService
open import 028f03ff5b4f55ee public -- Physical Data Domain
open import d5e6ddd05c46547c public -- Software Technology

postulate
  ComputingDevice : ClassOfClassOfBoundedIndividual

postulate --  ComputingDevice is subTypeOf NetworkingSystem
  st-02f5121d641c7ef7 : ComputingDevice ⊏⋆ₑ NetworkingSystem

postulate --  ComputingDevice is subTypeOf ComputingSystem
  st-02f5155c641c8262 : ComputingDevice ⊏⋆ₑ ComputingSystem

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

{- Hosted Application Package: 
Hosting of a Deployable Application Package in a Computing System.
 -}
-- Aggregate Member : Hosted Application Package
postulate
  HostedApplicationPackage : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Hosted Application Package-
  membershipOfHostedApplicationPackage-nestingbinding : ComputingDevice ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfHostedApplicationPackage : classOfNestingRelation {ct = HostedApplicationPackage}  membershipOfHostedApplicationPackage-nestingbinding

postulate -- Relation: Aggregation of -Deployable Application Package (Hosted Application Package) -
  aggregationOfDeployableApplicationPackageHostedApplicationPackage : classOfOrderedRelation  HostedApplicationPackage DeployableApplicationPackage

-- Relation derived from the composability of Hosted Application Package, by mathematical composition
hostedApplicationPackage : classOfOrderedRelation  ComputingDevice DeployableApplicationPackage
hostedApplicationPackage = membershipOfHostedApplicationPackage ∘ aggregationOfDeployableApplicationPackageHostedApplicationPackage


{- Hosted Micro-Service: 
Hosting of a MicroService in a Computing System.
 -}
-- Aggregate Member : Hosted Micro-Service
postulate
  HostedMicroService : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Hosted Micro-Service-
  membershipOfHostedMicroService-nestingbinding : ComputingDevice ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfHostedMicroService : classOfNestingRelation {ct = HostedMicroService}  membershipOfHostedMicroService-nestingbinding

postulate -- Relation: Aggregation of -MicroService (Hosted Micro-Service) -
  aggregationOfMicroServiceHostedMicroService : classOfOrderedRelation  HostedMicroService MicroService

-- Relation derived from the composability of Hosted Micro-Service, by mathematical composition
hostedMicroService : classOfOrderedRelation  ComputingDevice MicroService
hostedMicroService = membershipOfHostedMicroService ∘ aggregationOfMicroServiceHostedMicroService


{- Hosted Data: 
Hosting a set of Physical Data Assets in a data store of a Computing System.
 -}
-- Aggregate Member : Hosted Data
postulate
  HostedData : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Hosted Data-
  membershipOfHostedData-nestingbinding : ComputingDevice ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfHostedData : classOfNestingRelation {ct = HostedData}  membershipOfHostedData-nestingbinding

postulate -- Relation: Aggregation of -Physical Data Domain (Hosted Data) -
  aggregationOfPhysicalDataDomainHostedData : classOfOrderedRelation  HostedData PhysicalDataDomain

-- Relation derived from the composability of Hosted Data, by mathematical composition
hostedData : classOfOrderedRelation  ComputingDevice PhysicalDataDomain
hostedData = membershipOfHostedData ∘ aggregationOfPhysicalDataDomainHostedData


{- Hosted Software Technology: 
Hosting of a Software Technology in a Computing Device.
 -}
-- Aggregate Member : Hosted Software Technology
postulate
  HostedSOftwareTechnology : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Hosted Software Technology-
  membershipOfHostedSOftwareTechnology-nestingbinding : ComputingDevice ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfHostedSOftwareTechnology : classOfNestingRelation {ct = HostedSOftwareTechnology}  membershipOfHostedSOftwareTechnology-nestingbinding

postulate -- Relation: Aggregation of -Software Technology (Hosted Software Technology) -
  aggregationOfSOftwareTechnologyHostedSOftwareTechnology : classOfOrderedRelation  HostedSOftwareTechnology SOftwareTechnology

-- Relation derived from the composability of Hosted Software Technology, by mathematical composition
hostedSOftwareTechnology : classOfOrderedRelation  ComputingDevice SOftwareTechnology
hostedSOftwareTechnology = membershipOfHostedSOftwareTechnology ∘ aggregationOfSOftwareTechnologyHostedSOftwareTechnology