{- ============================== Copyright (c) 2026 SysFEAT - Systemic Framework for Enterprise Architecture & Transformation This work is released under the MIT License. framework.sysfeat.com Class of Bounded Individual: A Class of Bounded Individual is a Class of Individual which denotes Bounded Individuals that have a proper life cycle, bounded by Temporal Bounding Types.Class of Bounded Individual is the powertype of Bounded Individual. It means that all sub-types of Bounded Individual are instances of Class of Bounded Individual.Examples:- Car, - Application,- A Process Type (Action Process Type) such as the registration process used at the Oackland digital hospital during the COVID-19 pandemic.Counterexamples:- Project is not a Class of Bounded Individual because its instances have a spatio-temporal extent. Project is a subtype of Bounded Individual.- Capability is not a Class of Bounded Individual. It is a Property. Documentation : https://framework.sysfeat.com/pages/3492c53e619642ed.htm External references: OMG - KerML - Class: https://www.omg.org/spec/KerML/1.0/PDF#page=67 ISO 15926 - ClassOfArrangedIndividual: https://15926.blog/topics/data-model/index.htm#ClassOfArrangedIndividual - ============================== -} {-# OPTIONS --cubical --guardedness #-} module SysFEAT.UpperOntology.3492c53e619642ed where -- ========== Class of Bounded Individual open import Agda.Primitive open import SysFEAT.UpperOntology.6aa8cbcb65b32971 public -- Class of Individual open import SysFEAT.UpperOntology.8cfa941b6852781f public -- Bounded Aggregate open import SysFEAT.UpperOntology.60876d5c68de82f2 public -- Class of Class of Bounded Individual open import SysFEAT.UpperOntology.746ac18368905aa2 public -- Property open import SysFEAT.UpperOntology.9429979a66823f90 public -- Temporal Bounding Type ClassOfBoundedIndividual : ClassOfClassOfBoundedIndividual ClassOfBoundedIndividual = ClassOfIndividual -- ClassOfBoundedIndividual is subTypeOf ClassOfIndividual st-3492c53e619642ed-6aa8cbcb65b32971 : ClassOfBoundedIndividual ⊏ₑ ClassOfIndividual st-3492c53e619642ed-6aa8cbcb65b32971 = polySubTypeOf-identity -- ClassOfBoundedIndividual withAspect BoundedAggregate st-3492c53e619642ed-8cfa941b6852781f : ClassOfBoundedIndividual ⊏ₐₑ (BoundedAggregate (lsuc(lzero))) st-3492c53e619642ed-8cfa941b6852781f = polySubTypeOf-identity postulate -- ClassOfBoundedIndividual is PowerInstanceOf Class of Class of Bounded Individual 328b393a66e32434 : ClassOfBoundedIndividual ∷ₚₑ ClassOfClassOfBoundedIndividual postulate -- ClassOfClassOfBoundedIndividual is ReflexivePowerType 9ba3baef6aaa6223 : ClassOfClassOfBoundedIndividual ⊏ₘₑ ClassOfBoundedIndividual -- == Relations ======================= -- -------------------------------------------------------------------------------------------- {- Specialized Class of Bounded Individual: -} specializedClassOfBoundedIndividual : Linkage ClassOfBoundedIndividual ClassOfBoundedIndividual specializedClassOfBoundedIndividual = make_subTypeOf "Class of Bounded Individual Specialization" "Specialized Class of Bounded Individual" postulate -- specializedClassOfBoundedIndividual is subTypeOf specializedClassOfIndividual st-e53a627766e4b4cd-e429632e66ec72ab : specializedClassOfBoundedIndividual ⊏⋆ᵣ specializedClassOfIndividual -- -------------------------------------------------------------------------------------------- {- Qualifying Property: A SubTypeOfEntity from a Class of Bounded Individual to a Property that asserts all members of the Class of Bounded Individual have the Property. -} qualifyingProperty : Linkage ClassOfBoundedIndividual Property qualifyingProperty = make_subTypeOf "Qualification" "Qualifying Property" postulate -- qualifyingProperty is subTypeOf specializedClassOfIndividual st-16621f9a689131e0-e429632e66ec72ab : qualifyingProperty ⊏⋆ᵣ specializedClassOfIndividual -- -------------------------------------------------------------------------------------------- {- Temporal Ordering Type: -} -- Aggregate Member : Temporal Ordering Type TemporalOrderingType : ClassOfClassOfIndividual TemporalOrderingType = ClassOfIndividual -- TemporalOrderingType withAspect OrderingConnector st-2557481f6758a91a-478a4a4468565425 : TemporalOrderingType ⊏ₐₑ (OrderingConnector (lsuc(lzero))) st-2557481f6758a91a-478a4a4468565425 = polySubTypeOf-identity -- Membership relation membershipOfTemporalOrderingType : Linkage ClassOfBoundedIndividual TemporalOrderingType membershipOfTemporalOrderingType = make_upwardNestingRelation "temporalOrderingType membership" "nested temporalOrderingType" -- Aggregation relation aggregationOfTemporalBoundingTypeTemporalOrderingType : Linkage TemporalOrderingType TemporalBoundingType aggregationOfTemporalBoundingTypeTemporalOrderingType = make_Relation "TemporalBoundingType aggregation" "aggregated TemporalBoundingType" {- temporalOrderingType : derived relation obtained by composing membershipOfTemporalOrderingType and aggregationOfTemporalBoundingTypeTemporalOrderingType It directly links an Class of Bounded Individual to the final aggregated TemporalBoundingType hiding the reifying TemporalOrderingType -} temporalOrderingType : Linkage ClassOfBoundedIndividual TemporalBoundingType temporalOrderingType = membershipOfTemporalOrderingType ∘ aggregationOfTemporalBoundingTypeTemporalOrderingType -- -------------------------------------------------------------------------------------------- {- Aggregate Qualification: An Aggregate Qualification is a Qualifying Property that is refied as an Unbounded Member of a Class of Bounded Individual.Example:. The enforcement of a rule in a process (Rule Enforcement) is a refied Qualifying Property. -} -- Aggregate Member : Aggregate Qualification AggregateQualification : ClassOfClassOfAbstractEntity AggregateQualification = ClassOfAbstractEntity -- AggregateQualification is subTypeOf ClassOfAbstractEntity st-b83e30bc696f51e5-3aca55ee6aa645c2 : AggregateQualification ⊏ₑ ClassOfAbstractEntity st-b83e30bc696f51e5-3aca55ee6aa645c2 = polySubTypeOf-identity -- AggregateQualification withAspect UnboundedMember st-b83e30bc696f51e5-8cfaf71a6852b042 : AggregateQualification ⊏ₐₑ (UnboundedMember (lsuc(lzero))) st-b83e30bc696f51e5-8cfaf71a6852b042 = polySubTypeOf-identity -- Membership relation membershipOfAggregateQualification : Linkage ClassOfBoundedIndividual AggregateQualification membershipOfAggregateQualification = make_upwardNestingRelation "aggregateQualification membership" "nested aggregateQualification" -- Aggregation relation aggregationOfPropertyAggregateQualification : Linkage AggregateQualification Property aggregationOfPropertyAggregateQualification = make_Relation "Property aggregation" "aggregated Property" {- aggregateQualification : derived relation obtained by composing membershipOfAggregateQualification and aggregationOfPropertyAggregateQualification It directly links an Class of Bounded Individual to the final aggregated Property hiding the reifying AggregateQualification -} aggregateQualification : Linkage ClassOfBoundedIndividual Property aggregateQualification = membershipOfAggregateQualification ∘ aggregationOfPropertyAggregateQualification postulate -- aggregateQualification is subTypeOf specializedClassOfIndividual st-b83e30bc696f51e5-e429632e66ec72ab : aggregateQualification ⊏⋆ᵣ specializedClassOfIndividual -- -------------------------------------------------------------------------------------------- {- Aggregate Holonymy Type: An Aggregate Holonymy Type is a reified flavor of Poly Class of Holonymy whereby the referenced Class of Individual is aggregated in its parent (whole) Class of Bounded Individual.Example:1) A Process Step is the reification of the composition of a child process in a parent process.2) -} -- Aggregate Member : Aggregate Holonymy Type AggregateHolonymyType : ClassOfClassOfIndividual AggregateHolonymyType = ClassOfIndividual -- AggregateHolonymyType is subTypeOf ClassOfBoundedIndividual st-c2f2c83b66ea4d78-3492c53e619642ed : AggregateHolonymyType ⊏ₑ ClassOfBoundedIndividual st-c2f2c83b66ea4d78-3492c53e619642ed = polySubTypeOf-identity -- AggregateHolonymyType withAspect BoundedMember st-c2f2c83b66ea4d78-0eb999956855e070 : AggregateHolonymyType ⊏ₐₑ (BoundedMember (lsuc(lzero))) st-c2f2c83b66ea4d78-0eb999956855e070 = polySubTypeOf-identity -- Membership relation membershipOfAggregateHolonymyType : Linkage ClassOfBoundedIndividual AggregateHolonymyType membershipOfAggregateHolonymyType = make_upwardNestingRelation "aggregateHolonymyType membership" "nested aggregateHolonymyType" -- Aggregation relation aggregationOfClassOfBoundedIndividualAggregateHolonymyType : Linkage AggregateHolonymyType ClassOfBoundedIndividual aggregationOfClassOfBoundedIndividualAggregateHolonymyType = make_Relation "ClassOfBoundedIndividual aggregation" "aggregated ClassOfBoundedIndividual" {- aggregateHolonymyType : derived relation obtained by composing membershipOfAggregateHolonymyType and aggregationOfClassOfBoundedIndividualAggregateHolonymyType It directly links an Class of Bounded Individual to the final aggregated ClassOfBoundedIndividual hiding the reifying AggregateHolonymyType -} aggregateHolonymyType : Linkage ClassOfBoundedIndividual ClassOfBoundedIndividual aggregateHolonymyType = membershipOfAggregateHolonymyType ∘ aggregationOfClassOfBoundedIndividualAggregateHolonymyType postulate -- aggregateHolonymyType is subTypeOf classOfHolonymy st-c2f2c83b66ea4d78-d91704746a62320c : aggregateHolonymyType ⊏⋆ᵣ classOfHolonymy