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

Category: 
A Category is a used to classify Class of Individual.
 - ============================== -}

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

module f69619236a0f8dcd where -- ========== Category

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 23d5c5fc685142de public -- Elementary Block

Category : (u : Level) → Set (lsuc (lsuc (lsuc u)))
Category u = MetaClass u

postulate --  Category is subTypeOf MetaFamilyOfClass
  st-f69619306a0f8e3e : ∀ {u} → (Category u) ⊏⋆ₑ (MetaFamilyOfClass u)

postulate --  Category is subTypeOf ElementaryBlock
  st-afe2c475681b7b09 : ∀ {u} → (Category u) ⊏⋆ₑ (ElementaryBlock {u})

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

{- Category Specialization:  -}
postulate -- Relation: Category Specialization
  categorySpecialization : ∀ {u} → classOfMixedOrderRelation  (Category u) (Category u)