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

Capability Map: 
Top level assembly of Capabilitys and their dependencies which, together, provide a scope of added value (Outcome Events) pursued by Operational Transformations.
 - ============================== -}

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

module 01f12127689b6de2 where -- ========== Capability Map

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 06710aeb68ed2d29 public -- Meta Family of Class
open import 8cfa942f68527849 public -- Unbounded Aggregate
open import 515c13db68953887 public -- Capability

postulate
  CapabilityMap : PropertyType

postulate --  CapabilityMap is subTypeOf MetaFamilyOfClass
  st-299e33c5684864b3 : CapabilityMap ⊏ₐₑ MetaFamilyOfClass {lsuc(lzero)}

postulate --  CapabilityMap is subTypeOf UnboundedAggregate
  st-299e556b6848808c : CapabilityMap ⊏ₐₑ UnboundedAggregate {lsuc(lzero)}

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

{- Capability Member: 
Aggregate Composition of a Capability.
 -}
-- Aggregate Member : Capability Member
postulate
  CapabilityMember : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Capability Member-
  membershipOfCapabilityMember-nestingbinding : CapabilityMap ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfCapabilityMember : classOfNestingRelation {ct = CapabilityMember}  membershipOfCapabilityMember-nestingbinding

postulate -- Relation: Aggregation of -Capability (Capability Member) -
  aggregationOfCapabilityCapabilityMember : classOfOrderedRelation  CapabilityMember Capability

-- Relation derived from the composability of Capability Member, by mathematical composition
capabilityMember : classOfOrderedRelation  CapabilityMap Capability
capabilityMember = membershipOfCapabilityMember ∘ aggregationOfCapabilityCapabilityMember