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

Audit: 
An Audit is a mission assigned to a team of internal auditors in the context of an audit plan.
 - ============================== -}

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

module f4be37465ee1cba6 where -- ========== Audit

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (_×_ to _⊗_)
open import 1737b76a5fe28204 public -- Governance Activity
open import ebcfaeac5ad76ed7 public -- Individual Asset

postulate
  Audit : ClassOfBoundedIndividual

postulate --  Audit is subTypeOf GovernanceActivity
  st-f4be375d5ee1ccbf : Audit ⊏⋆ₑ GovernanceActivity

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

{- Audit Activity:  -}
-- Aggregate Member : Audit Activity
postulate
  AuditActivity : ClassOfIndividual

postulate -- NestingRelation: Membership of -Audit Activity-
  membershipOfAuditActivity-nestingbinding : Audit ⊏ₑ  LexicalScope {lzero}
  membershipOfAuditActivity : classOfNestingRelation {ct = AuditActivity}  membershipOfAuditActivity-nestingbinding

postulate -- Relation: Aggregation of -Audit (Audit Activity) -
  aggregationOfAuditAuditActivity : classOfOrderedRelation  AuditActivity Audit

-- Relation derived from the composability of Audit Activity, by mathematical composition
auditActivity : classOfOrderedRelation  Audit Audit
auditActivity = membershipOfAuditActivity ∘ aggregationOfAuditAuditActivity


{- Finding:  -}
-- Aggregate Member : Finding
postulate
  Finding : ClassOfIndividual

postulate -- NestingRelation: Membership of -Finding-
  membershipOfFinding-nestingbinding : Audit ⊏ₑ  LexicalScope {lzero}
  membershipOfFinding : classOfNestingRelation {ct = Finding}  membershipOfFinding-nestingbinding

postulate -- Relation: Aggregation of -Individual Asset (Finding) -
  aggregationOfIndividualAssetFinding : classOfOrderedRelation  Finding IndividualAsset

-- Relation derived from the composability of Finding, by mathematical composition
finding : classOfOrderedRelation  Audit IndividualAsset
finding = membershipOfFinding ∘ aggregationOfIndividualAssetFinding