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

Container: 
A Container is a collection of Building Blocks whose existence and meaning are defined by the Container.A Container is both:1. A Lexical Scope: the meaning and usage of a Building Block is only applicable within the context of the Container to which it belongs.2. A universe of discourse: the complete range of Building Blocks that are expressed, assumed, or implied in an architecture domain.Examples: - Container Package- Library- Enterprise
 - ============================== -}

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

module 0eb93b4268549a66 where -- ========== Container

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 23d5c494685141b5 public -- Block Lexical Scope
open import 23d5a9ea68513ced public -- Building Block

postulate
  Container : ∀ {u} → ClassOfMixedOrderEntity u

postulate --  Container is subTypeOf BlockLexicalScope
  st-0eb9430568549edb : ∀ {u} → (Container {u}) ⊏⋆ₑ (BlockLexicalScope {u})

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

{- Packaged Building Block:  -}
postulate -- NestingRelation: Packaged Building Block
  packagedBuildingBlock-nestingbinding : ∀ {u} → (Container {u}) ⊏ₑ  LexicalScope {u}
  packagedBuildingBlock : ∀ {u} → classOfNestingRelation {ct = BuildingBlock {u}}  (packagedBuildingBlock-nestingbinding {u})

{- Imported Container: 
The Imported Container relationship extends the Block Lexical Scope of a Containerr to Building Blocksof the imported Container.
 -}
postulate -- Relation: Imported Container
  importedContainer : ∀ {u} → classOfMixedOrderRelation  (Container {u}) (Container {u})