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

Category Partition: 

 - ============================== -}

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

module f696240c6a0f9ea4 where -- ========== Category Partition

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 8d1ceeab68f755a5 public -- Class Partition
open import 0eb97aff6855cd23 public -- Model Property Block
open import f69619236a0f8dcd public -- Category
open import 24f72ea26a0f5029 public -- Family of Category

postulate
  CategoryPartition : ∀ {u} → Category u

postulate --  CategoryPartition is subTypeOf ClassPartition
  st-24f72e4d6a0f4fa3 : ∀ {u} → (CategoryPartition {u}) ⊏⋆ₑ (ClassPartition u)

postulate --  CategoryPartition is subTypeOf ModelPropertyBlock
  st-c2f2a60166ea394c : ∀ {u} → (CategoryPartition {u}) ⊏⋆ₑ (ModelPropertyBlock {u})

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

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

{- Classifying Schema:  -}
postulate -- Relation: Classifying Schema
  classifyingSchema : ∀ {u} → classOfMixedOrderRelation  (CategoryPartition {u}) (FamilyOfCategory {u})