{-# OPTIONS --safe --cubical #-}

module OWL2.DirectSemantics.AnnotationErasure where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.DirectSemantics

directAnnotationErasure :
  ∀ {ℓSig}
    {Sig : Signature ℓSig} →
  Ontology Sig → Ontology Sig
directAnnotationErasure ont =
  ont

directAnnotationErasureIdempotent :
  ∀ {ℓSig}
    {Sig : Signature ℓSig}
    (ont : Ontology Sig) →
  directAnnotationErasure (directAnnotationErasure ont) ≡
  directAnnotationErasure ont
directAnnotationErasureIdempotent ont =
  refl

directAnnotationErasurePreservesSatisfaction :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {ont : Ontology Sig} →
  SatisfiesOntology I ont →
  SatisfiesOntology I (directAnnotationErasure ont)
directAnnotationErasurePreservesSatisfaction satisfied =
  satisfied

directAnnotationErasureReflectsSatisfaction :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {ont : Ontology Sig} →
  SatisfiesOntology I (directAnnotationErasure ont) →
  SatisfiesOntology I ont
directAnnotationErasureReflectsSatisfaction satisfied =
  satisfied

directAnnotationErasureSatisfactionEquiv :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {ont : Ontology Sig} →
  (SatisfiesOntology I ont →
   SatisfiesOntology I (directAnnotationErasure ont))
  ×
  (SatisfiesOntology I (directAnnotationErasure ont) →
   SatisfiesOntology I ont)
directAnnotationErasureSatisfactionEquiv {I = I} {ont = ont} =
  (λ satisfied →
    directAnnotationErasurePreservesSatisfaction
      {I = I}
      {ont = ont}
      satisfied) ,
  (λ satisfied →
    directAnnotationErasureReflectsSatisfaction
      {I = I}
      {ont = ont}
      satisfied)