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

Library: 
A Library is a kind of Architecture Container used to group Asset Blocks into several independent modules (aka package).They allow virtual partitions of model repositories used for model management. In particular, Asset Blocks owned by different Library(ies) can have the same name (namespacing).
 - ============================== -}

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

module 0eb9601c6855c11e where -- ========== Library

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 0eb96bc36855ca44 public -- Model Package
open import 0eb95f1b6855bf64 public -- Architecture Container

postulate
  Library : FirstOrderClass

postulate --  Library is subTypeOf ModelPackage
  st-0f6418c268598b03 : Library ⊏⋆ₑ ModelPackage

postulate --  Library is subTypeOf ArchitectureContainer
  st-0eb960326855c14a : Library ⊏ₐₑ ArchitectureContainer {lzero}

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

{- Sub-Library:  -}
postulate -- NestingRelation: Sub-Library
  subLibrary-nestingbinding : Library ⊏ₑ  LexicalScope {lzero}
  subLibrary : classOfNestingRelation {ct = Library}  subLibrary-nestingbinding