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

Concept Type: 
A Concept Type is a class of concepts which have Concepts as instances: Concept Types classify Concepts.
 - ============================== -}

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

module c39701c75747a173 where -- ========== Concept Type

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import d6cd2cea5ab98e5f public -- Information Entity
open import 267b28fc66757618 public -- Class of Conceptual Entity
open import 362fc4365b3c39b8 public -- Concept

postulate
  ConceptType : ClassOfClassOfBoundedIndividual

postulate --  ConceptType is subTypeOf InformationEntity
  st-3a0e3bed63ce3320 : ConceptType ⊏⋆ₑ InformationEntity

postulate --  ConceptType is subTypeOf ClassOfConceptualEntity
  st-5e4060eb5b528622 : ConceptType ⊏⋆ₑ ClassOfConceptualEntity

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

{- Power Component:  -}
postulate -- Relation: Power Component
  powerComponent : classOfOrderedRelation  ConceptType Concept

{- Concept Type Relationship:  -}
-- Aggregate Member : Concept Type Relationship
postulate
  ConceptTypeRelationship : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Concept Type Relationship-
  membershipOfConceptTypeRelationship-nestingbinding : ConceptType ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfConceptTypeRelationship : classOfNestingRelation {ct = ConceptTypeRelationship}  membershipOfConceptTypeRelationship-nestingbinding

postulate -- Relation: Aggregation of -Concept Type (Concept Type Relationship) -
  aggregationOfConceptTypeConceptTypeRelationship : classOfOrderedRelation  ConceptTypeRelationship ConceptType

-- Relation derived from the composability of Concept Type Relationship, by mathematical composition
conceptTypeRelationship : classOfOrderedRelation  ConceptType ConceptType
conceptTypeRelationship = membershipOfConceptTypeRelationship ∘ aggregationOfConceptTypeConceptTypeRelationship