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

Legal Entity Type: 
A Legal Entity Type is a Macro Org-Unit Type that is a type of lawful or legally standing association, corporation, partnership, proprietorship, trust, or individual that has the legal capacity to: enter into agreements or contracts; assume obligations; incur and pay debts; sue and be sued in its own right; and to be accountable for illegal activities.
 - ============================== -}

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

module c0a3c7c666417665 where -- ========== Legal Entity Type

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 076d15425a5e158c public -- Org-Unit Type
open import 7c408aa155270eea public -- Department Type

postulate
  LegalEntityType : ClassOfClassOfBoundedIndividual

postulate --  LegalEntityType is subTypeOf OrgUnitType
  st-c0a3caa9664178c9 : LegalEntityType ⊏⋆ₑ OrgUnitType

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

{- Department Type:  -}
-- Aggregate Member : Department Type
postulate
  DepartmentType : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Department Type-
  membershipOfDepartmentType-nestingbinding : LegalEntityType ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfDepartmentType : classOfNestingRelation {ct = DepartmentType}  membershipOfDepartmentType-nestingbinding

postulate -- Relation: Aggregation of -Department Type (Department Type) -
  aggregationOfDepartmentTypeDepartmentType : classOfOrderedRelation  DepartmentType DepartmentType

-- Relation derived from the composability of Department Type, by mathematical composition
departmentType : classOfOrderedRelation  LegalEntityType DepartmentType
departmentType = membershipOfDepartmentType ∘ aggregationOfDepartmentTypeDepartmentType