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

module OWL2.DirectSemantics.Lemmas where

open import OWL2.Prelude
import Cubical.Data.Prod.Base as Prod
import Cubical.Data.Vec.Base as Vec
open import OWL2.Syntax
open import OWL2.DirectSemantics

subsetRefl :
  ∀ {ℓA ℓP} {A : Type ℓA} {P : A → Type ℓP} →
  P ⊆ P
subsetRefl x px =
  px

subsetTrans :
  ∀ {ℓA ℓP ℓQ ℓR}
    {A : Type ℓA}
    {P : A → Type ℓP}
    {Q : A → Type ℓQ}
    {R : A → Type ℓR} →
  P ⊆ Q → Q ⊆ R → P ⊆ R
subsetTrans pq qr x px =
  qr x (pq x px)

sameExtensionRefl :
  ∀ {ℓA ℓP} {A : Type ℓA} {P : A → Type ℓP} →
  SameExtension P P
sameExtensionRefl =
  subsetRefl , subsetRefl

sameExtensionIntro :
  ∀ {ℓA ℓP ℓQ}
    {A : Type ℓA}
    {P : A → Type ℓP}
    {Q : A → Type ℓQ} →
  P ⊆ Q → Q ⊆ P → SameExtension P Q
sameExtensionIntro pq qp =
  pq , qp

sameExtensionSym :
  ∀ {ℓA ℓP ℓQ}
    {A : Type ℓA}
    {P : A → Type ℓP}
    {Q : A → Type ℓQ} →
  SameExtension P Q → SameExtension Q P
sameExtensionSym pq =
  snd pq , fst pq

sameExtensionTrans :
  ∀ {ℓA ℓP ℓQ ℓR}
    {A : Type ℓA}
    {P : A → Type ℓP}
    {Q : A → Type ℓQ}
    {R : A → Type ℓR} →
  SameExtension P Q → SameExtension Q R → SameExtension P R
sameExtensionTrans pq qr =
  subsetTrans (fst pq) (fst qr) ,
  subsetTrans (snd qr) (snd pq)

disjointSym :
  ∀ {ℓA ℓP ℓQ}
    {A : Type ℓA}
    {P : A → Type ℓP}
    {Q : A → Type ℓQ} →
  Disjoint P Q → Disjoint Q P
disjointSym disjoint x qx px =
  disjoint x px qx

classSubsumption :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d : ClassExpression Sig}
    {x : ObjectDomain I} →
  SatisfiesAxiom I (subClassOf c d) →
  evalClass I c x → evalClass I d x
classSubsumption cd cx =
  cd _ cx

subClassRefl :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassExpression Sig} →
  SatisfiesAxiom I (subClassOf c c)
subClassRefl =
  subsetRefl

subClassTrans :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d e : ClassExpression Sig} →
  SatisfiesAxiom I (subClassOf c d) →
  SatisfiesAxiom I (subClassOf d e) →
  SatisfiesAxiom I (subClassOf c e)
subClassTrans cd de =
  subsetTrans cd de

equivalentClassesFirst :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d : ClassExpression Sig}
    {cs : List (ClassExpression Sig)} →
  SatisfiesAxiom I (equivalentClasses (c ∷ d ∷ cs)) →
  SameExtension (evalClass I c) (evalClass I d)
equivalentClassesFirst eq =
  Prod.proj₁ (fst eq)

equivalentClassForward :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d : ClassExpression Sig}
    {x : ObjectDomain I} →
  SameExtension (evalClass I c) (evalClass I d) →
  evalClass I c x → evalClass I d x
equivalentClassForward eq =
  fst eq _

equivalentClassBackward :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d : ClassExpression Sig}
    {x : ObjectDomain I} →
  SameExtension (evalClass I c) (evalClass I d) →
  evalClass I d x → evalClass I c x
equivalentClassBackward eq =
  snd eq _

equivalentClasses₂Intro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d : ClassExpression Sig} →
  SatisfiesAxiom I (subClassOf c d) →
  SatisfiesAxiom I (subClassOf d c) →
  SatisfiesAxiom I (equivalentClasses (c ∷ d ∷ []))
equivalentClasses₂Intro cd dc =
  Prod._,_ (sameExtensionIntro cd dc) (lift tt) ,
  (lift tt , lift tt)

disjointClassesFirst :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d : ClassExpression Sig}
    {cs : List (ClassExpression Sig)} →
  SatisfiesAxiom I (disjointClasses (c ∷ d ∷ cs)) →
  Disjoint (evalClass I c) (evalClass I d)
disjointClassesFirst disjoint =
  Prod.proj₁ (fst disjoint)

disjointClasses₂Sym :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c d : ClassExpression Sig} →
  SatisfiesAxiom I (disjointClasses (c ∷ d ∷ [])) →
  SatisfiesAxiom I (disjointClasses (d ∷ c ∷ []))
disjointClasses₂Sym {I = I} {c = c} {d = d} disjoint =
  Prod._,_
    ( disjointSym
      {P = evalClass I c}
      {Q = evalClass I d}
      (disjointClassesFirst {I = I} {c = c} {d = d} {cs = []} disjoint))
    (lift tt) ,
  (lift tt , lift tt)

objectSubProperty :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : SubObjectPropertyExpression Sig}
    {q : ObjectPropertyExpression Sig}
    {x y : ObjectDomain I} →
  SatisfiesAxiom I (subObjectPropertyOf p q) →
  evalSubObjectPropertyExpression I p x y → evalObjectProperty I q x y
objectSubProperty pq pxy =
  pq _ _ pxy

subObjectPropertyRefl :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig} →
  SatisfiesAxiom I (subObjectPropertyOf (subObjectProperty p) p)
subObjectPropertyRefl x y pxy =
  pxy

subObjectPropertyTrans :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p q r : ObjectPropertyExpression Sig} →
  SatisfiesAxiom I (subObjectPropertyOf (subObjectProperty p) q) →
  SatisfiesAxiom I (subObjectPropertyOf (subObjectProperty q) r) →
  SatisfiesAxiom I (subObjectPropertyOf (subObjectProperty p) r)
subObjectPropertyTrans pq qr x y pxy =
  qr x y (pq x y pxy)

objectPropertyChain₂Intro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p q : ObjectPropertyExpression Sig}
    {x y z : ObjectDomain I} →
  evalObjectProperty I p x y →
  evalObjectProperty I q y z →
  evalSubObjectPropertyExpression I (subObjectPropertyChain p q []) x z
objectPropertyChain₂Intro pxy qyz =
  _ , (pxy , qyz)

sharedObjectPropertyValueIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {x y z : ObjectDomain I} →
  evalObjectProperty I p x z →
  evalObjectProperty I p y z →
  SharedObjectPropertyValue I p x y
sharedObjectPropertyValueIntro pxz pyz =
  _ , (pxz , pyz)

sharedDataPropertyValueIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {x y : ObjectDomain I}
    {z : DataDomain I} →
  evalDataProperty I p x z →
  evalDataProperty I p y z →
  SharedDataPropertyValue I p x y
sharedDataPropertyValueIntro pxz pyz =
  _ , (pxz , pyz)

hasKeyApply :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassExpression Sig}
    {key : PropertyKey Sig}
    {a b : IndividualName Sig} →
  SatisfiesAxiom I (hasKey c key) →
  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)
hasKeyApply keyAxiom ca cb shared =
  keyAxiom _ _ ca cb shared

objectCardinalityAtLeastOneIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : Optional (ClassExpression Sig)}
    {x y : ObjectDomain I} →
  ObjectCardinalityFiller I p c x y →
  ObjectCardinalityAtLeast I  p c x
objectCardinalityAtLeastOneIntro {I = I} {p = p} {c = c} {x = x} {y = y} filler =
  y Vec.∷ Vec.[] ,
  ((filler , lift tt) , (lift tt , lift tt))

objectCardinalityAtMostOneFromUnique :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : Optional (ClassExpression Sig)}
    {x : ObjectDomain I} →
  (∀ y z →
    ObjectCardinalityFiller I p c x y →
    ObjectCardinalityFiller I p c x z →
    ObjectEq I y z) →
  ObjectCardinalityAtMost I  p c x
objectCardinalityAtMostOneFromUnique {I = I} {p = p} {c = c} {x = x} unique
  (y Vec.∷ z Vec.∷ Vec.[] ,
   ((fy , (fz , _)) , ((notSame , _) , _))) =
  notSame (unique y z fy fz)

objectCardinalityExactOneIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : Optional (ClassExpression Sig)}
    {x y : ObjectDomain I} →
  ObjectCardinalityFiller I p c x y →
  (∀ y z →
    ObjectCardinalityFiller I p c x y →
    ObjectCardinalityFiller I p c x z →
    ObjectEq I y z) →
  ObjectCardinalityExact I  p c x
objectCardinalityExactOneIntro
  {I = I} {p = p} {c = c} {x = x} {y = y} filler unique =
  objectCardinalityAtLeastOneIntro
    {I = I} {p = p} {c = c} {x = x} {y = y} filler ,
  objectCardinalityAtMostOneFromUnique
    {I = I} {p = p} {c = c} {x = x} unique

dataCardinalityAtLeastOneIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : Optional (DataRange Sig)}
    {x : ObjectDomain I}
    {y : DataDomain I} →
  DataCardinalityFiller I p d x y →
  DataCardinalityAtLeast I  p d x
dataCardinalityAtLeastOneIntro {I = I} {p = p} {d = d} {x = x} {y = y} filler =
  y Vec.∷ Vec.[] ,
  ((filler , lift tt) , (lift tt , lift tt))

dataCardinalityAtMostOneFromUnique :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : Optional (DataRange Sig)}
    {x : ObjectDomain I} →
  (∀ y z →
    DataCardinalityFiller I p d x y →
    DataCardinalityFiller I p d x z →
    DataEq I y z) →
  DataCardinalityAtMost I  p d x
dataCardinalityAtMostOneFromUnique {I = I} {p = p} {d = d} {x = x} unique
  (y Vec.∷ z Vec.∷ Vec.[] ,
   ((fy , (fz , _)) , ((notSame , _) , _))) =
  notSame (unique y z fy fz)

dataCardinalityExactOneIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : Optional (DataRange Sig)}
    {x : ObjectDomain I}
    {y : DataDomain I} →
  DataCardinalityFiller I p d x y →
  (∀ y z →
    DataCardinalityFiller I p d x y →
    DataCardinalityFiller I p d x z →
    DataEq I y z) →
  DataCardinalityExact I  p d x
dataCardinalityExactOneIntro
  {I = I} {p = p} {d = d} {x = x} {y = y} filler unique =
  dataCardinalityAtLeastOneIntro
    {I = I} {p = p} {d = d} {x = x} {y = y} filler ,
  dataCardinalityAtMostOneFromUnique
    {I = I} {p = p} {d = d} {x = x} unique

objectDomainInfer :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : ClassExpression Sig}
    {x y : ObjectDomain I} →
  SatisfiesAxiom I (objectPropertyDomain p c) →
  evalObjectProperty I p x y → evalClass I c x
objectDomainInfer domain pxy =
  domain _ _ pxy

objectRangeInfer :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : ClassExpression Sig}
    {x y : ObjectDomain I} →
  SatisfiesAxiom I (objectPropertyRange p c) →
  evalObjectProperty I p x y → evalClass I c y
objectRangeInfer range pxy =
  range _ _ pxy

objectSomeIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : ClassExpression Sig}
    {x y : ObjectDomain I} →
  evalObjectProperty I p x y →
  evalClass I c y →
  evalClass I (objectSomeValuesFrom p c) x
objectSomeIntro pxy cy =
  _ , (pxy , cy)

objectSomeElim :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : ClassExpression Sig}
    {x : ObjectDomain I} →
  evalClass I (objectSomeValuesFrom p c) x →
  Σ (ObjectDomain I) (λ y → evalObjectProperty I p x y × evalClass I c y)
objectSomeElim some =
  some

objectSomeElimWith :
  ∀ {ℓSig ℓObj ℓData ℓSem ℓR}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : ClassExpression Sig}
    {x : ObjectDomain I}
    {R : Type ℓR} →
  evalClass I (objectSomeValuesFrom p c) x →
  ((y : ObjectDomain I) →
    evalObjectProperty I p x y →
    evalClass I c y →
    R) →
  R
objectSomeElimWith (y , (pxy , cy)) k =
  k y pxy cy

objectAllApply :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : ObjectPropertyExpression Sig}
    {c : ClassExpression Sig}
    {x y : ObjectDomain I} →
  evalClass I (objectAllValuesFrom p c) x →
  evalObjectProperty I p x y →
  evalClass I c y
objectAllApply all pxy =
  all _ pxy

objectIntersectionIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassExpression Sig}
    {cs : List (ClassExpression Sig)}
    {x : ObjectDomain I} →
  evalClass I c x →
  evalClass I (objectIntersectionOf cs) x →
  evalClass I (objectIntersectionOf (c ∷ cs)) x
objectIntersectionIntro cx cxs =
  cx , cxs

objectIntersectionHead :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassExpression Sig}
    {cs : List (ClassExpression Sig)}
    {x : ObjectDomain I} →
  evalClass I (objectIntersectionOf (c ∷ cs)) x →
  evalClass I c x
objectIntersectionHead =
  fst

objectIntersectionTail :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassExpression Sig}
    {cs : List (ClassExpression Sig)}
    {x : ObjectDomain I} →
  evalClass I (objectIntersectionOf (c ∷ cs)) x →
  evalClass I (objectIntersectionOf cs) x
objectIntersectionTail =
  snd

objectUnionLeft :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassExpression Sig}
    {cs : List (ClassExpression Sig)}
    {x : ObjectDomain I} →
  evalClass I c x →
  evalClass I (objectUnionOf (c ∷ cs)) x
objectUnionLeft =
  inl

objectUnionRight :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {c : ClassExpression Sig}
    {cs : List (ClassExpression Sig)}
    {x : ObjectDomain I} →
  evalClass I (objectUnionOf cs) x →
  evalClass I (objectUnionOf (c ∷ cs)) x
objectUnionRight =
  inr

dataSubProperty :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p q : DataPropertyExpression Sig}
    {x : ObjectDomain I}
    {y : DataDomain I} →
  SatisfiesAxiom I (subDataPropertyOf p q) →
  evalDataProperty I p x y → evalDataProperty I q x y
dataSubProperty pq pxy =
  pq _ _ pxy

subDataPropertyRefl :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig} →
  SatisfiesAxiom I (subDataPropertyOf p p)
subDataPropertyRefl x y pxy =
  pxy

subDataPropertyTrans :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p q r : DataPropertyExpression Sig} →
  SatisfiesAxiom I (subDataPropertyOf p q) →
  SatisfiesAxiom I (subDataPropertyOf q r) →
  SatisfiesAxiom I (subDataPropertyOf p r)
subDataPropertyTrans pq qr x y pxy =
  qr x y (pq x y pxy)

dataDomainInfer :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {c : ClassExpression Sig}
    {x : ObjectDomain I}
    {y : DataDomain I} →
  SatisfiesAxiom I (dataPropertyDomain p c) →
  evalDataProperty I p x y → evalClass I c x
dataDomainInfer domain pxy =
  domain _ _ pxy

dataRangeInfer :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : DataRange Sig}
    {x : ObjectDomain I}
    {y : DataDomain I} →
  SatisfiesAxiom I (dataPropertyRange p d) →
  evalDataProperty I p x y → evalDataRange I d y
dataRangeInfer range pxy =
  range _ _ pxy

dataSomeIntro :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : DataRange Sig}
    {x : ObjectDomain I}
    {y : DataDomain I} →
  evalDataProperty I p x y →
  evalDataRange I d y →
  evalClass I (dataSomeValuesFrom p d) x
dataSomeIntro pxy dy =
  _ , (pxy , dy)

dataSomeElim :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : DataRange Sig}
    {x : ObjectDomain I} →
  evalClass I (dataSomeValuesFrom p d) x →
  Σ (DataDomain I) (λ y → evalDataProperty I p x y × evalDataRange I d y)
dataSomeElim some =
  some

dataSomeElimWith :
  ∀ {ℓSig ℓObj ℓData ℓSem ℓR}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : DataRange Sig}
    {x : ObjectDomain I}
    {R : Type ℓR} →
  evalClass I (dataSomeValuesFrom p d) x →
  ((y : DataDomain I) →
    evalDataProperty I p x y →
    evalDataRange I d y →
    R) →
  R
dataSomeElimWith (y , (pxy , dy)) k =
  k y pxy dy

dataAllApply :
  ∀ {ℓSig ℓObj ℓData ℓSem}
    {Sig : Signature ℓSig}
    {I : Interpretation Sig ℓObj ℓData ℓSem}
    {p : DataPropertyExpression Sig}
    {d : DataRange Sig}
    {x : ObjectDomain I}
    {y : DataDomain I} →
  evalClass I (dataAllValuesFrom p d) x →
  evalDataProperty I p x y →
  evalDataRange I d y
dataAllApply all pxy =
  all _ pxy