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

Organization: 
An Organization is a group of people who share a common purpose and establish a functional division of labor in pursuit of their common purpose.It is the relationships between its members in the pursuit of their common purpose that give unity and identity to an organization.
 - ============================== -}

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

module 910196ca550a2ec2 where -- ========== Organization

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import c7dad03f5ae92ae9 public -- Responsible Human Entity
open import 66f8685a620b1440 public -- Individual Business Agent
open import 076d15425a5e158c public -- Org-Unit Type
open import c7dad43c5ae92d25 public -- Person

postulate
  Organization : ClassOfBoundedIndividual

postulate --  Organization is subTypeOf ResponsibleHumanEntity
  st-c334e7635ecb9fea : Organization ⊏⋆ₑ ResponsibleHumanEntity

postulate --  Organization is subTypeOf IndividualBusinessAgent
  st-c80a3e6567858e70 : Organization ⊏⋆ₑ IndividualBusinessAgent

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

{- Sub Contractor:  -}
-- Aggregate Member : Sub Contractor
postulate
  SubContractor : ClassOfIndividual

postulate -- NestingRelation: Membership of -Sub Contractor-
  membershipOfSubContractor-nestingbinding : Organization ⊏ₑ  LexicalScope {lzero}
  membershipOfSubContractor : classOfNestingRelation {ct = SubContractor}  membershipOfSubContractor-nestingbinding

postulate -- Relation: Aggregation of -Organization (Sub Contractor) -
  aggregationOfOrganizationSubContractor : classOfOrderedRelation  SubContractor Organization

-- Relation derived from the composability of Sub Contractor, by mathematical composition
subContractor : classOfOrderedRelation  Organization Organization
subContractor = membershipOfSubContractor ∘ aggregationOfOrganizationSubContractor


{- Organizational Position:  -}
-- Aggregate Member : Organizational Position
postulate
  OrganizationalPosition : ClassOfIndividual

postulate -- NestingRelation: Membership of -Organizational Position-
  membershipOfOrganizationalPosition-nestingbinding : Organization ⊏ₑ  LexicalScope {lzero}
  membershipOfOrganizationalPosition : classOfNestingRelation {ct = OrganizationalPosition}  membershipOfOrganizationalPosition-nestingbinding

postulate -- Relation: Aggregation of -Person (Organizational Position) -
  aggregationOfPersonOrganizationalPosition : classOfOrderedRelation  OrganizationalPosition Person

-- Relation derived from the composability of Organizational Position, by mathematical composition
organizationalPosition : classOfOrderedRelation  Organization Person
organizationalPosition = membershipOfOrganizationalPosition ∘ aggregationOfPersonOrganizationalPosition


{- Organizational Reponsibility:  -}
-- Aggregate Member : Organizational Reponsibility
postulate
  OrganizationalReponsibility : ClassOfIndividual

postulate -- NestingRelation: Membership of -Organizational Reponsibility-
  membershipOfOrganizationalReponsibility-nestingbinding : Organization ⊏ₑ  LexicalScope {lzero}
  membershipOfOrganizationalReponsibility : classOfNestingRelation {ct = OrganizationalReponsibility}  membershipOfOrganizationalReponsibility-nestingbinding

postulate -- Relation: Aggregation of -Person (Organizational Reponsibility) -
  aggregationOfPersonOrganizationalReponsibility : classOfOrderedRelation  OrganizationalReponsibility Person

-- Relation derived from the composability of Organizational Reponsibility, by mathematical composition
organizationalReponsibility : classOfOrderedRelation  Organization Person
organizationalReponsibility = membershipOfOrganizationalReponsibility ∘ aggregationOfPersonOrganizationalReponsibility


{- Sub-Unit:  -}
-- Aggregate Member : Sub-Unit
postulate
  SubUnit : ClassOfIndividual

postulate -- NestingRelation: Membership of -Sub-Unit-
  membershipOfSubUnit-nestingbinding : Organization ⊏ₑ  LexicalScope {lzero}
  membershipOfSubUnit : classOfNestingRelation {ct = SubUnit}  membershipOfSubUnit-nestingbinding

postulate -- Relation: Aggregation of -Organization (Sub-Unit) -
  aggregationOfOrganizationSubUnit : classOfOrderedRelation  SubUnit Organization

-- Relation derived from the composability of Sub-Unit, by mathematical composition
subUnit : classOfOrderedRelation  Organization Organization
subUnit = membershipOfSubUnit ∘ aggregationOfOrganizationSubUnit