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

Skill Map: 
Family of Skills associated to an activity domain or to an Enterprise.
 - ============================== -}

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

module dd26f21668a0b0fd where -- ========== Skill Map

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import dd2638ba68a073a8 public -- Business Resource Capability Map
open import dd26f17a68a0b08b public -- Skill

postulate
  SkillMap : PropertyType

postulate --  SkillMap is subTypeOf BusinessResourceCapabilityMap
  st-d98b27bf632368c6 : SkillMap ⊏⋆ₑ BusinessResourceCapabilityMap

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

{- Skill Member:  -}
-- Aggregate Member : Skill Member
postulate
  SkillMember : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Skill Member-
  membershipOfSkillMember-nestingbinding : SkillMap ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfSkillMember : classOfNestingRelation {ct = SkillMember}  membershipOfSkillMember-nestingbinding

postulate -- Relation: Aggregation of -Skill (Skill Member) -
  aggregationOfSkillSkillMember : classOfOrderedRelation  SkillMember Skill

-- Relation derived from the composability of Skill Member, by mathematical composition
skillMember : classOfOrderedRelation  SkillMap Skill
skillMember = membershipOfSkillMember ∘ aggregationOfSkillSkillMember