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

Computer Network: 
A Computer Network is an assembly of Network Devices (e.g. routers, switches, firewalls) that enables communications between Computing Systems (e.g. Computer Servers).A Computer Network may breakdown into sub-networks.
 - ============================== -}

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

module a41ab2d25b378b12 where -- ========== Computer Network

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import a41ab3105b378b66 public -- IT Infrastructure System
open import 070b0d5564011dbb public -- Networking System
open import f4be0fba5ee1d935 public -- Network Device

postulate
  ComputerNetwork : ClassOfClassOfBoundedIndividual

postulate --  ComputerNetwork is subTypeOf ITInfrastructureSystem
  st-a41ab3225b378bb7 : ComputerNetwork ⊏⋆ₑ ITInfrastructureSystem

postulate --  ComputerNetwork is subTypeOf NetworkingSystem
  st-070b1093640122ba : ComputerNetwork ⊏⋆ₑ NetworkingSystem

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

{- Network Node: 
Role of a Network Device in a Computer Network.
 -}
-- Aggregate Member : Network Node
postulate
  NetworkNode : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Network Node-
  membershipOfNetworkNode-nestingbinding : ComputerNetwork ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfNetworkNode : classOfNestingRelation {ct = NetworkNode}  membershipOfNetworkNode-nestingbinding

postulate -- Relation: Aggregation of -Network Device (Network Node) -
  aggregationOfNetworkDeviceNetworkNode : classOfOrderedRelation  NetworkNode NetworkDevice

-- Relation derived from the composability of Network Node, by mathematical composition
networkNode : classOfOrderedRelation  ComputerNetwork NetworkDevice
networkNode = membershipOfNetworkNode ∘ aggregationOfNetworkDeviceNetworkNode