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

Asset Type: 
An Asset Type is a Class of Individual which is used in the description of the enterprise and its systems, such as Action Process Typees, Department Types, Applications, Location Types, Period Types.

Documentation : https://framework.sysfeat.com/pages/a4a5b3f855585ce1.htm

External references:
  OpenGroup - TOGAF - Architecture Building Blocks: https://pubs.opengroup.org/togaf-standard/architecture-content/chap04.html#tag_04_02_01
 - ============================== -}

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

module SysFEAT.SOF.a4a5b3f855585ce1 where -- ========== Asset Type

open import Agda.Primitive
open import SysFEAT.SOF.0eb95f356855bf94 public -- Asset Block
open import SysFEAT.UpperOntology.3492c53e619642ed public -- Class of Bounded Individual
open import SysFEAT.SOF.e53af71366e37de2 public -- Condition Property Type
open import SysFEAT.SOF.515c6a856893324e public -- Asset Property
open import SysFEAT.SOF.f69620466a0f9c2f public -- Asset Category

AssetType : ClassOfClassOfBoundedIndividual
AssetType = ClassOfBoundedIndividual


--  AssetType withAspect AssetBlock
st-a4a5b3f855585ce1-0eb95f356855bf94 : AssetType ⊏ₐₑ (AssetBlock (lsuc(lzero)))
st-a4a5b3f855585ce1-0eb95f356855bf94 = polySubTypeOf-identity

--  AssetType is subTypeOf ClassOfBoundedIndividual
st-a4a5b3f855585ce1-3492c53e619642ed : AssetType ⊏ₑ ClassOfBoundedIndividual
st-a4a5b3f855585ce1-3492c53e619642ed = polySubTypeOf-identity


-- == Relations =======================

-- -------------------------------------------------------------------------------------------- 
{- Specialized Asset: 
A specialization of Asset Types.
-}
specializedAsset :  Linkage AssetType AssetType
specializedAsset = make_subTypeOf "Specialized Asset" "Specialized Asset"

postulate -- specializedAsset is subTypeOf specializedClassOfBoundedIndividual
  st-12b0287266e936d5-e53a627766e4b4cd  : specializedAsset  ⊏⋆ᵣ  specializedClassOfBoundedIndividual

-- -------------------------------------------------------------------------------------------- 
{- Applicable Condition Type: 
Set of Condition Property Types that can be applied to an Asset Type.
-}
applicableConditionType :  Linkage AssetType ConditionPropertyType
applicableConditionType = make_instanceOf "Applicable Condition Type" "Applicable Condition Type"

postulate -- applicableConditionType is subTypeOf categorization
  st-c2f2709166ea21a0-f69619646a0f8e6c  : applicableConditionType  ⊏⋆ᵣ  categorization  {lsuc(lsuc(lzero))}

-- -------------------------------------------------------------------------------------------- 
{- Asset Type Qualification: 
Qualification of an Asset Type by an Asset Property.
-}
assetTypeQualification :  Linkage AssetType AssetProperty
assetTypeQualification = make_subTypeOf "Asset Type Qualification" "Asset Type Qualification"

postulate -- assetTypeQualification is subTypeOf qualifyingProperty
  st-190c1f3b68964a27-16621f9a689131e0  : assetTypeQualification  ⊏⋆ᵣ  qualifyingProperty

-- -------------------------------------------------------------------------------------------- 
{- Category of Architecture Block: -}
categoryOfArchitectureBlock : ∀ {u} →  Linkage AssetType (AssetCategory u)
categoryOfArchitectureBlock = make_instanceOf "Category of Architecture Block" "Category of Architecture Block"

postulate -- categoryOfArchitectureBlock is subTypeOf categorization
  st-f69620606a0f9c94-f69619646a0f8e6c  : categoryOfArchitectureBlock  {lsuc(lsuc(lzero))}  ⊏⋆ᵣ  categorization  {lsuc(lsuc(lzero))}