{- ============================== Copyright (c) 2026 SysFEAT - Systemic Framework for Enterprise Architecture & Transformation This work is released under the MIT License. framework.sysfeat.com Unbounded Aggregate: An Unbounded Aggregate is an Aggregate Entity Block that does not have boundaries and, thereby, that cannot participate to Ordering Connections.Examples:- Operating Eco-System;- Directive. Documentation : https://framework.sysfeat.com/pages/8cfa942f68527849.htm - ============================== -} {-# OPTIONS --cubical --guardedness #-} module SysFEAT.UpperOntology.8cfa942f68527849 where -- ========== Unbounded Aggregate open import Agda.Primitive open import SysFEAT.UpperOntology.23d56d9868525869 public -- Aggregate Entity Block UnboundedAggregate : ∀ (u : Level) → ClassOfMixedOrderEntity u UnboundedAggregate u = MixedOrderEntity u -- UnboundedAggregate is subTypeOf AggregateEntityBlock st-8cfa942f68527849-23d56d9868525869 : ∀ {u v} → (UnboundedAggregate u) ⊏⋆ₑ (AggregateEntityBlock v) st-8cfa942f68527849-23d56d9868525869 = trivialPolySubTypeOfEntity -- == Relations =======================