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

module OWL2.DirectSemantics where

open import OWL2.Prelude
open import Cubical.Data.Nat.Base using (suc)
import Cubical.Data.Vec.Base as Vec
open import OWL2.Syntax

SemLevel : Level → Level → Level → Level → Level
SemLevel ℓSig ℓObj ℓData ℓSem =
  ℓ-max (ℓ-max (ℓ-max ℓSig ℓObj) ℓData) ℓSem

AllList :
  ∀ {ℓA ℓP} {A : Type ℓA} →
  List A → (A → Type ℓP) → Type (ℓ-max ℓA ℓP)
AllList xs P =
  RepListP P xs

AnyList :
  ∀ {ℓA ℓP} {A : Type ℓA} →
  List A → (A → Type ℓP) → Type (ℓ-max ℓA ℓP)
AnyList [] P =
  ⊥*
AnyList (x ∷ xs) P =
  P x ⊎ AnyList xs P

Pairwise :
  ∀ {ℓA ℓR} {A : Type ℓA} →
  (A → A → Type ℓR) → List A → Type (ℓ-max ℓA ℓR)
Pairwise R [] =
  Unit*
Pairwise R (x ∷ xs) =
  AllList xs (R x) × Pairwise R xs

VecAll :
  ∀ {ℓA ℓP n} {A : Type ℓA} →
  Vec.Vec A n → (A → Type ℓP) → Type (ℓ-max ℓA ℓP)
VecAll Vec.[] P =
  Unit*
VecAll (x Vec.∷ xs) P =
  P x × VecAll xs P

VecPairwise :
  ∀ {ℓA ℓR n} {A : Type ℓA} →
  (A → A → Type ℓR) → Vec.Vec A n → Type (ℓ-max ℓA ℓR)
VecPairwise R Vec.[] =
  Unit*
VecPairwise R (x Vec.∷ xs) =
  VecAll xs (R x) × VecPairwise R xs

_⊆_ :
  ∀ {ℓA ℓP ℓQ} {A : Type ℓA} →
  (A → Type ℓP) → (A → Type ℓQ) → Type (ℓ-max ℓA (ℓ-max ℓP ℓQ))
P ⊆ Q =
  ∀ x → P x → Q x

SameExtension :
  ∀ {ℓA ℓP ℓQ} {A : Type ℓA} →
  (A → Type ℓP) → (A → Type ℓQ) → Type (ℓ-max ℓA (ℓ-max ℓP ℓQ))
SameExtension P Q =
  (P ⊆ Q) × (Q ⊆ P)

Disjoint :
  ∀ {ℓA ℓP ℓQ} {A : Type ℓA} →
  (A → Type ℓP) → (A → Type ℓQ) → Type (ℓ-max ℓA (ℓ-max ℓP ℓQ))
Disjoint P Q =
  ∀ x → P x → Q x → ⊥

record Interpretation
  {ℓSig : Level}
  (Sig : Signature ℓSig)
  (ℓObj ℓData ℓSem : Level)
  : Type (ℓ-suc (SemLevel ℓSig ℓObj ℓData ℓSem)) where
  field
    ObjectDomain : Type ℓObj
    DataDomain   : Type ℓData

    classDenotation :
      ClassName Sig → ObjectDomain → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
    objectPropertyDenotation :
      ObjectPropertyName Sig → ObjectDomain → ObjectDomain → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
    dataPropertyDenotation :
      DataPropertyName Sig → ObjectDomain → DataDomain → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
    datatypeDenotation :
      DatatypeName Sig → DataDomain → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
    facetDenotation :
      DatatypeName Sig →
      FacetName Sig →
      Literal Sig →
      DataDomain →
      Type (SemLevel ℓSig ℓObj ℓData ℓSem)

    individualDenotation :
      IndividualName Sig → ObjectDomain
    literalDenotation :
      Literal Sig → DataDomain

open Interpretation public

ObjectEq :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  ObjectDomain I → ObjectDomain I →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
ObjectEq {ℓSig = ℓSig} {ℓData = ℓData} {ℓSem = ℓSem} I x y =
  Lift (ℓ-max (ℓ-max ℓSig ℓData) ℓSem) (x ≡ y)

DataEq :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  DataDomain I → DataDomain I →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
DataEq {ℓSig = ℓSig} {ℓObj = ℓObj} {ℓSem = ℓSem} I x y =
  Lift (ℓ-max (ℓ-max ℓSig ℓObj) ℓSem) (x ≡ y)

evalObjectProperty :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  ObjectPropertyExpression Sig →
  ObjectDomain I → ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
evalObjectProperty I (objectProperty p) x y =
  objectPropertyDenotation I p x y
evalObjectProperty I topObjectProperty x y =
  Unit*
evalObjectProperty I bottomObjectProperty x y =
  ⊥*
evalObjectProperty I (objectInverseOf p) x y =
  evalObjectProperty I p y x

evalObjectPropertyChain :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  ObjectPropertyExpression Sig →
  List (ObjectPropertyExpression Sig) →
  ObjectDomain I → ObjectDomain I →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
evalObjectPropertyChain I p [] x y =
  evalObjectProperty I p x y
evalObjectPropertyChain I p (q ∷ qs) x y =
  Σ (ObjectDomain I)
    (λ z →
      evalObjectProperty I p x z ×
      evalObjectPropertyChain I q qs z y)

evalSubObjectPropertyExpression :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  SubObjectPropertyExpression Sig →
  ObjectDomain I → ObjectDomain I →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
evalSubObjectPropertyExpression I (subObjectProperty p) =
  evalObjectProperty I p
evalSubObjectPropertyExpression I (subObjectPropertyChain p q ps) =
  evalObjectPropertyChain I p (q ∷ ps)

evalDataProperty :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  DataPropertyExpression Sig →
  ObjectDomain I → DataDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
evalDataProperty I (dataProperty p) x y =
  dataPropertyDenotation I p x y
evalDataProperty I topDataProperty x y =
  Unit*
evalDataProperty I bottomDataProperty x y =
  ⊥*

mutual
  evalDataRange :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    DataRange Sig →
    DataDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalDataRange I (datatype d) v =
    datatypeDenotation I d v
  evalDataRange I (datatypeRestriction d facets) v =
    datatypeDenotation I d v × evalFacetRestrictionsAll I d facets v
  evalDataRange I dataTop v =
    Unit*
  evalDataRange I dataBottom v =
    ⊥*
  evalDataRange I (dataComplementOf d) v =
    ¬ evalDataRange I d v
  evalDataRange I (dataIntersectionOf ds) v =
    evalDataRangesAll I ds v
  evalDataRange I (dataUnionOf ds) v =
    evalDataRangesAny I ds v
  evalDataRange I (dataOneOf xs) v =
    AnyList xs (λ lit → DataEq I (literalDenotation I lit) v)

  evalFacetRestriction :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    DatatypeName Sig →
    FacetRestriction Sig →
    DataDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalFacetRestriction I d restriction v =
    facetDenotation I d
      (facet restriction)
      (value restriction)
      v

  evalFacetRestrictionsAll :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    DatatypeName Sig →
    List (FacetRestriction Sig) →
    DataDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalFacetRestrictionsAll I d [] v =
    Unit*
  evalFacetRestrictionsAll I d (restriction ∷ restrictions) v =
    evalFacetRestriction I d restriction v
    ×
    evalFacetRestrictionsAll I d restrictions v

  evalDataRangesAll :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    List (DataRange Sig) →
    DataDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalDataRangesAll I [] v =
    Unit*
  evalDataRangesAll I (d ∷ ds) v =
    evalDataRange I d v × evalDataRangesAll I ds v

  evalDataRangesAny :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    List (DataRange Sig) →
    DataDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalDataRangesAny I [] v =
    ⊥*
  evalDataRangesAny I (d ∷ ds) v =
    evalDataRange I d v ⊎ evalDataRangesAny I ds v

mutual
  evalClass :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ClassExpression Sig →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalClass I (namedClass c) x =
    classDenotation I c x
  evalClass I owlThing x =
    Unit*
  evalClass I owlNothing x =
    ⊥*
  evalClass I (objectIntersectionOf cs) x =
    evalClassesAll I cs x
  evalClass I (objectUnionOf cs) x =
    evalClassesAny I cs x
  evalClass I (objectComplementOf c) x =
    ¬ evalClass I c x
  evalClass I (objectOneOf xs) x =
    AnyList xs (λ a → ObjectEq I (individualDenotation I a) x)
  evalClass I (objectSomeValuesFrom p c) x =
    Σ (ObjectDomain I) (λ y → evalObjectProperty I p x y × evalClass I c y)
  evalClass I (objectAllValuesFrom p c) x =
    ∀ y → evalObjectProperty I p x y → evalClass I c y
  evalClass I (objectHasValue p a) x =
    evalObjectProperty I p x (individualDenotation I a)
  evalClass I (objectHasSelf p) x =
    evalObjectProperty I p x x
  evalClass I (objectMinCardinality n p c) x =
    ObjectCardinalityAtLeast I n p c x
  evalClass I (objectMaxCardinality n p c) x =
    ObjectCardinalityAtMost I n p c x
  evalClass I (objectExactCardinality n p c) x =
    ObjectCardinalityExact I n p c x
  evalClass I (dataSomeValuesFrom p d) x =
    Σ (DataDomain I) (λ y → evalDataProperty I p x y × evalDataRange I d y)
  evalClass I (dataAllValuesFrom p d) x =
    ∀ y → evalDataProperty I p x y → evalDataRange I d y
  evalClass I (dataHasValue p lit) x =
    evalDataProperty I p x (literalDenotation I lit)
  evalClass I (dataMinCardinality n p d) x =
    DataCardinalityAtLeast I n p d x
  evalClass I (dataMaxCardinality n p d) x =
    DataCardinalityAtMost I n p d x
  evalClass I (dataExactCardinality n p d) x =
    DataCardinalityExact I n p d x

  evalClassesAll :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    List (ClassExpression Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalClassesAll I [] x =
    Unit*
  evalClassesAll I (c ∷ cs) x =
    evalClass I c x × evalClassesAll I cs x

  evalClassesAny :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    List (ClassExpression Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalClassesAny I [] x =
    ⊥*
  evalClassesAny I (c ∷ cs) x =
    evalClass I c x ⊎ evalClassesAny I cs x

  evalOptionalClass :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    Optional (ClassExpression Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalOptionalClass I absent y =
    Unit*
  evalOptionalClass I (present c) y =
    evalClass I c y

  ObjectCardinalityFiller :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ObjectPropertyExpression Sig →
    Optional (ClassExpression Sig) →
    ObjectDomain I → ObjectDomain I →
    Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  ObjectCardinalityFiller I p c x y =
    evalObjectProperty I p x y × evalOptionalClass I c y

  ObjectCardinalityAtLeast :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ℕ → ObjectPropertyExpression Sig →
    Optional (ClassExpression Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  ObjectCardinalityAtLeast I n p c x =
    Σ (Vec.Vec (ObjectDomain I) n)
      (λ ys →
        VecAll ys (ObjectCardinalityFiller I p c x)
        ×
        VecPairwise (λ y z → ¬ ObjectEq I y z) ys)

  ObjectCardinalityAtMost :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ℕ → ObjectPropertyExpression Sig →
    Optional (ClassExpression Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  ObjectCardinalityAtMost I n p c x =
    ¬ ObjectCardinalityAtLeast I (suc n) p c x

  ObjectCardinalityExact :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ℕ → ObjectPropertyExpression Sig →
    Optional (ClassExpression Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  ObjectCardinalityExact I n p c x =
    ObjectCardinalityAtLeast I n p c x
    ×
    ObjectCardinalityAtMost I n p c x

  evalOptionalDataRange :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    Optional (DataRange Sig) →
    DataDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  evalOptionalDataRange I absent y =
    Unit*
  evalOptionalDataRange I (present d) y =
    evalDataRange I d y

  DataCardinalityFiller :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    DataPropertyExpression Sig →
    Optional (DataRange Sig) →
    ObjectDomain I → DataDomain I →
    Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  DataCardinalityFiller I p d x y =
    evalDataProperty I p x y × evalOptionalDataRange I d y

  DataCardinalityAtLeast :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ℕ → DataPropertyExpression Sig →
    Optional (DataRange Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  DataCardinalityAtLeast I n p d x =
    Σ (Vec.Vec (DataDomain I) n)
      (λ ys →
        VecAll ys (DataCardinalityFiller I p d x)
        ×
        VecPairwise (λ y z → ¬ DataEq I y z) ys)

  DataCardinalityAtMost :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ℕ → DataPropertyExpression Sig →
    Optional (DataRange Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  DataCardinalityAtMost I n p d x =
    ¬ DataCardinalityAtLeast I (suc n) p d x

  DataCardinalityExact :
    ∀ {ℓSig ℓObj ℓData ℓSem}
      {Sig : Signature ℓSig} →
    (I : Interpretation Sig ℓObj ℓData ℓSem) →
    ℕ → DataPropertyExpression Sig →
    Optional (DataRange Sig) →
    ObjectDomain I → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
  DataCardinalityExact I n p d x =
    DataCardinalityAtLeast I n p d x
    ×
    DataCardinalityAtMost I n p d x

SharedObjectPropertyValue :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  ObjectPropertyExpression Sig →
  ObjectDomain I → ObjectDomain I →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
SharedObjectPropertyValue I p x y =
  Σ (ObjectDomain I)
    (λ z → evalObjectProperty I p x z × evalObjectProperty I p y z)

SharedDataPropertyValue :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  DataPropertyExpression Sig →
  ObjectDomain I → ObjectDomain I →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
SharedDataPropertyValue I p x y =
  Σ (DataDomain I)
    (λ z → evalDataProperty I p x z × evalDataProperty I p y z)

SharedKey :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  (I : Interpretation Sig ℓObj ℓData ℓSem) →
  PropertyKey Sig →
  ObjectDomain I → ObjectDomain I →
  Type (SemLevel ℓSig ℓObj ℓData ℓSem)
SharedKey I key x y =
  AllList (objectProperties key) (λ p → SharedObjectPropertyValue I p x y)
  ×
  AllList (dataProperties key) (λ p → SharedDataPropertyValue I p x y)

SatisfiesAxiom :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  Axiom Sig → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
SatisfiesAxiom I (declaration e) =
  Unit*
SatisfiesAxiom I (subClassOf c d) =
  evalClass I c ⊆ evalClass I d
SatisfiesAxiom I (equivalentClasses cs) =
  Pairwise (λ c d → SameExtension (evalClass I c) (evalClass I d)) cs
SatisfiesAxiom I (disjointClasses cs) =
  Pairwise (λ c d → Disjoint (evalClass I c) (evalClass I d)) cs

SatisfiesAxiom I (subObjectPropertyOf p q) =
  ∀ x y →
    evalSubObjectPropertyExpression I p x y →
    evalObjectProperty I q x y
SatisfiesAxiom I (equivalentObjectProperties ps) =
  Pairwise
    (λ p q →
      SameExtension
        (λ xy → evalObjectProperty I p (fst xy) (snd xy))
        (λ xy → evalObjectProperty I q (fst xy) (snd xy)))
    ps
SatisfiesAxiom I (disjointObjectProperties ps) =
  Pairwise
    (λ p q →
      Disjoint
        (λ xy → evalObjectProperty I p (fst xy) (snd xy))
        (λ xy → evalObjectProperty I q (fst xy) (snd xy)))
    ps
SatisfiesAxiom I (objectPropertyDomain p c) =
  ∀ x y → evalObjectProperty I p x y → evalClass I c x
SatisfiesAxiom I (objectPropertyRange p c) =
  ∀ x y → evalObjectProperty I p x y → evalClass I c y
SatisfiesAxiom I (functionalObjectProperty p) =
  ∀ x y z → evalObjectProperty I p x y → evalObjectProperty I p x z → ObjectEq I y z
SatisfiesAxiom I (inverseFunctionalObjectProperty p) =
  ∀ x y z → evalObjectProperty I p y x → evalObjectProperty I p z x → ObjectEq I y z
SatisfiesAxiom I (reflexiveObjectProperty p) =
  BinaryRelation.isRefl (evalObjectProperty I p)
SatisfiesAxiom I (irreflexiveObjectProperty p) =
  BinaryRelation.isIrrefl (evalObjectProperty I p)
SatisfiesAxiom I (symmetricObjectProperty p) =
  BinaryRelation.isSym (evalObjectProperty I p)
SatisfiesAxiom I (asymmetricObjectProperty p) =
  BinaryRelation.isAsym (evalObjectProperty I p)
SatisfiesAxiom I (transitiveObjectProperty p) =
  BinaryRelation.isTrans (evalObjectProperty I p)

SatisfiesAxiom I (subDataPropertyOf p q) =
  ∀ x y → evalDataProperty I p x y → evalDataProperty I q x y
SatisfiesAxiom I (equivalentDataProperties ps) =
  Pairwise
    (λ p q →
      SameExtension
        (λ xy → evalDataProperty I p (fst xy) (snd xy))
        (λ xy → evalDataProperty I q (fst xy) (snd xy)))
    ps
SatisfiesAxiom I (disjointDataProperties ps) =
  Pairwise
    (λ p q →
      Disjoint
        (λ xy → evalDataProperty I p (fst xy) (snd xy))
        (λ xy → evalDataProperty I q (fst xy) (snd xy)))
    ps
SatisfiesAxiom I (dataPropertyDomain p c) =
  ∀ x y → evalDataProperty I p x y → evalClass I c x
SatisfiesAxiom I (dataPropertyRange p d) =
  ∀ x y → evalDataProperty I p x y → evalDataRange I d y
SatisfiesAxiom I (functionalDataProperty p) =
  ∀ x y z → evalDataProperty I p x y → evalDataProperty I p x z → DataEq I y z

SatisfiesAxiom I (datatypeDefinition d r) =
  SameExtension (datatypeDenotation I d) (evalDataRange I r)
SatisfiesAxiom I (hasKey c key) =
  ∀ a b →
    evalClass I c (individualDenotation I a) →
    evalClass I c (individualDenotation I b) →
    SharedKey I key (individualDenotation I a) (individualDenotation I b) →
    ObjectEq I (individualDenotation I a) (individualDenotation I b)

SatisfiesAxiom I (sameIndividual xs) =
  Pairwise
    (λ a b → ObjectEq I (individualDenotation I a) (individualDenotation I b))
    xs
SatisfiesAxiom I (differentIndividuals xs) =
  Pairwise
    (λ a b → ¬ ObjectEq I (individualDenotation I a) (individualDenotation I b))
    xs
SatisfiesAxiom I (classAssertion c a) =
  evalClass I c (individualDenotation I a)
SatisfiesAxiom I (objectPropertyAssertion p a b) =
  evalObjectProperty I p (individualDenotation I a) (individualDenotation I b)
SatisfiesAxiom I (negativeObjectPropertyAssertion p a b) =
  ¬ evalObjectProperty I p (individualDenotation I a) (individualDenotation I b)
SatisfiesAxiom I (dataPropertyAssertion p a lit) =
  evalDataProperty I p (individualDenotation I a) (literalDenotation I lit)
SatisfiesAxiom I (negativeDataPropertyAssertion p a lit) =
  ¬ evalDataProperty I p (individualDenotation I a) (literalDenotation I lit)

SatisfiesOntology :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  Ontology Sig → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
SatisfiesOntology I O =
  AllList (axioms O) (SatisfiesAxiom I)

Model :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Interpretation Sig ℓObj ℓData ℓSem →
  Ontology Sig → Type (SemLevel ℓSig ℓObj ℓData ℓSem)
Model =
  SatisfiesOntology

Entails :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig} →
  Ontology Sig → Ontology Sig →
  Type (ℓ-suc (SemLevel ℓSig ℓObj ℓData ℓSem))
Entails {ℓObj = ℓObj} {ℓData = ℓData} {ℓSem = ℓSem} O₁ O₂ =
  (I : Interpretation _ ℓObj ℓData ℓSem) → Model I O₁ → Model I O₂