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

Set of Condition Properties: 
A Set of Condition Properties is a And combination of Condition Propertys.Example: . Delivery time of 30 minutes, at a cost ranging between $8.50 and $10, in stormy conditions.
 - ============================== -}

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

module 21ed5bf7689c1ca3 where -- ========== Set of Condition Properties

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 21ed231d689c0679 public -- Condition Property
open import 8cfa942f68527849 public -- Unbounded Aggregate
open import e53af87666e37fcd public -- Set of Environmental Condition Type

postulate
  SetOfConditionProperties : PropertyType

postulate --  SetOfConditionProperties is subTypeOf ConditionProperty
  st-dd26497d689f4774 : SetOfConditionProperties ⊏⋆ₑ ConditionProperty

postulate --  SetOfConditionProperties is subTypeOf UnboundedAggregate
  st-fee30ea2695d17bd : SetOfConditionProperties ⊏ₐₑ UnboundedAggregate {lsuc(lzero)}

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

{- Set of Environmental Condition Type:  -}
postulate -- Relation: Set of Environmental Condition Type
  setOfEnvironmentalConditionType : classOfMixedOrderRelation  SetOfConditionProperties SetOfEnvironmentalConditionType

{- Combined Property: 
And combination of a Condition Propertys.
 -}
-- Aggregate Member : Combined Property
postulate
  CombinedProperty : ClassOfClassOfIndividual

postulate -- NestingRelation: Membership of -Combined Property-
  membershipOfCombinedProperty-nestingbinding : SetOfConditionProperties ⊏ₑ  LexicalScope {lsuc(lzero)}
  membershipOfCombinedProperty : classOfNestingRelation {ct = CombinedProperty}  membershipOfCombinedProperty-nestingbinding

postulate -- Relation: Aggregation of -Condition Property (Combined Property) -
  aggregationOfConditionPropertyCombinedProperty : classOfOrderedRelation  CombinedProperty ConditionProperty

-- Relation derived from the composability of Combined Property, by mathematical composition
combinedProperty : classOfOrderedRelation  SetOfConditionProperties ConditionProperty
combinedProperty = membershipOfCombinedProperty ∘ aggregationOfConditionPropertyCombinedProperty