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

module OWL2.Kernel.Syntax where

open import OWL2.Prelude public
open import OWL2.Kernel.Signature public
  using (Signature)
open import OWL2.Kernel.Name public
  using
    ( ClassName
    ; ObjectPropertyName
    ; DataPropertyName
    ; AnnotationPropertyName
    ; DatatypeName
    ; FacetName
    ; IndividualName
    ; IRIName
    ; BlankNodeName
    )
open import OWL2.Kernel.DatatypeMap public
  using
    ( DatatypeMap
    ; DatatypeSupported
    ; LiteralSupported
    ; trivialDatatypeMap
    ; canonicalDatatype
    ; canonicalDatatypeMatches
    ; canonicalLiteralDatatype
    ; canonicalLiteralDatatypeMatches
    ; supportedDatatypeName
    ; supportedDatatypeMatches
    ; supportedLiteralDatatypeName
    ; supportedLiteralDatatypeMatches
    )
open import OWL2.Kernel.Regularity public
  using (SimpleObjectPropertyName)
open import OWL2.Kernel.Regularity
  using (RegularityContext)

record NonEmpty {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor nonEmpty
  field
    head : A
    tail : List A

open NonEmpty public

record AtLeastTwo {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor atLeastTwo
  field
    first  : A
    second : A
    rest   : List A

open AtLeastTwo public

data Entity (Sig : Signature) : Type₀ where
  classEntity :
    ClassName Sig → Entity Sig
  objectPropertyEntity :
    ObjectPropertyName Sig → Entity Sig
  dataPropertyEntity :
    DataPropertyName Sig → Entity Sig
  annotationPropertyEntity :
    AnnotationPropertyName Sig → Entity Sig
  datatypeEntity :
    DatatypeName Sig → Entity Sig
  individualEntity :
    IndividualName Sig → Entity Sig

data Literal (Sig : Signature) : Type₀ where
  typedLiteral :
    String →
    (datatype : DatatypeName Sig) →
    LiteralSupported Sig datatype →
    Literal Sig

record FacetRestriction (Sig : Signature) : Type₀ where
  constructor facetRestriction
  field
    facet :
      FacetName Sig
    value :
      Literal Sig

open FacetRestriction public

data DataRange (Sig : Signature) : Type₀ where
  datatype :
    (name : DatatypeName Sig) →
    DatatypeSupported Sig name →
    DataRange Sig
  dataTop :
    DataRange Sig
  dataBottom :
    DataRange Sig
  dataComplementOf :
    DataRange Sig → DataRange Sig
  dataIntersectionOf :
    NonEmpty (DataRange Sig) → DataRange Sig
  dataUnionOf :
    NonEmpty (DataRange Sig) → DataRange Sig
  dataOneOf :
    NonEmpty (Literal Sig) → DataRange Sig
  datatypeRestriction :
    (name : DatatypeName Sig) →
    DatatypeSupported Sig name →
    List (FacetRestriction Sig) →
    DataRange Sig

data ObjectPropertyExpression (Sig : Signature) : Type₀ where
  objectProperty :
    ObjectPropertyName Sig → ObjectPropertyExpression Sig
  topObjectProperty :
    ObjectPropertyExpression Sig
  bottomObjectProperty :
    ObjectPropertyExpression Sig
  objectInverseOf :
    ObjectPropertyExpression Sig → ObjectPropertyExpression Sig

data DataPropertyExpression (Sig : Signature) : Type₀ where
  dataProperty :
    DataPropertyName Sig → DataPropertyExpression Sig
  topDataProperty :
    DataPropertyExpression Sig
  bottomDataProperty :
    DataPropertyExpression Sig

record ObjectPropertyChain (Sig : Signature) : Type₀ where
  constructor objectPropertyChain
  field
    links : AtLeastTwo (ObjectPropertyExpression Sig)

open ObjectPropertyChain public

data SubObjectPropertyExpression (Sig : Signature) : Type₀ where
  subObjectProperty :
    ObjectPropertyExpression Sig → SubObjectPropertyExpression Sig
  subObjectPropertyChain :
    ObjectPropertyChain Sig → SubObjectPropertyExpression Sig

data Individual (Sig : Signature) : Type₀ where
  namedIndividual :
    IndividualName Sig → Individual Sig

data ClassExpression (Sig : Signature) : Type₀ where
  namedClass :
    ClassName Sig → ClassExpression Sig
  owlThing :
    ClassExpression Sig
  owlNothing :
    ClassExpression Sig
  objectIntersectionOf :
    NonEmpty (ClassExpression Sig) → ClassExpression Sig
  objectUnionOf :
    NonEmpty (ClassExpression Sig) → ClassExpression Sig
  objectComplementOf :
    ClassExpression Sig → ClassExpression Sig
  objectOneOf :
    NonEmpty (Individual Sig) → ClassExpression Sig
  objectSomeValuesFrom :
    ObjectPropertyExpression Sig →
    ClassExpression Sig →
    ClassExpression Sig
  objectAllValuesFrom :
    ObjectPropertyExpression Sig →
    ClassExpression Sig →
    ClassExpression Sig
  objectHasValue :
    ObjectPropertyExpression Sig →
    Individual Sig →
    ClassExpression Sig
  objectHasSelf :
    SimpleObjectPropertyName Sig →
    ClassExpression Sig
  objectMinCardinality :
    ℕ →
    SimpleObjectPropertyName Sig →
    Optional (ClassExpression Sig) →
    ClassExpression Sig
  objectMaxCardinality :
    ℕ →
    SimpleObjectPropertyName Sig →
    Optional (ClassExpression Sig) →
    ClassExpression Sig
  objectExactCardinality :
    ℕ →
    SimpleObjectPropertyName Sig →
    Optional (ClassExpression Sig) →
    ClassExpression Sig
  dataSomeValuesFrom :
    DataPropertyExpression Sig →
    DataRange Sig →
    ClassExpression Sig
  dataAllValuesFrom :
    DataPropertyExpression Sig →
    DataRange Sig →
    ClassExpression Sig
  dataHasValue :
    DataPropertyExpression Sig →
    Literal Sig →
    ClassExpression Sig
  dataMinCardinality :
    ℕ →
    DataPropertyExpression Sig →
    Optional (DataRange Sig) →
    ClassExpression Sig
  dataMaxCardinality :
    ℕ →
    DataPropertyExpression Sig →
    Optional (DataRange Sig) →
    ClassExpression Sig
  dataExactCardinality :
    ℕ →
    DataPropertyExpression Sig →
    Optional (DataRange Sig) →
    ClassExpression Sig

record PropertyKey (Sig : Signature) : Type₀ where
  constructor propertyKey
  field
    objectProperties : List (SimpleObjectPropertyName Sig)
    dataProperties   : List (DataPropertyExpression Sig)

open PropertyKey public

data AnnotationSubject (Sig : Signature) : Type₀ where
  annotationSubjectIRI :
    IRIName Sig → AnnotationSubject Sig
  annotationSubjectAnonymous :
    BlankNodeName Sig → AnnotationSubject Sig

data AnnotationValue (Sig : Signature) : Type₀ where
  annotationValueIRI :
    IRIName Sig → AnnotationValue Sig
  annotationValueAnonymous :
    BlankNodeName Sig → AnnotationValue Sig
  annotationValueLiteral :
    Literal Sig → AnnotationValue Sig

data Annotation (Sig : Signature) : Type₀ where
  annotation :
    List (Annotation Sig) →
    AnnotationPropertyName Sig →
    AnnotationValue Sig →
    Annotation Sig

record Annotated (Sig : Signature) (A : Type₀) : Type₀ where
  constructor annotated
  field
    itemAnnotations : List (Annotation Sig)
    itemBody        : A

open Annotated public

annotatedBodies :
  ∀ {Sig A} →
  List (Annotated Sig A) →
  List A
annotatedBodies [] =
  []
annotatedBodies (item ∷ items) =
  itemBody item ∷ annotatedBodies items

annotatedBodiesAppend :
  ∀ {Sig A} →
  (left right : List (Annotated Sig A)) →
  annotatedBodies (left ++ right) ≡
  annotatedBodies left ++ annotatedBodies right
annotatedBodiesAppend [] right =
  refl
annotatedBodiesAppend (item ∷ left) right =
  cong
    (λ bodies → itemBody item ∷ bodies)
    (annotatedBodiesAppend left right)

data Axiom (Sig : Signature) : Type₀ where
  declaration :
    Entity Sig → Axiom Sig

  subClassOf :
    ClassExpression Sig → ClassExpression Sig → Axiom Sig
  equivalentClasses :
    AtLeastTwo (ClassExpression Sig) → Axiom Sig
  disjointClasses :
    AtLeastTwo (ClassExpression Sig) → Axiom Sig
  disjointUnion :
    ClassName Sig → AtLeastTwo (ClassExpression Sig) → Axiom Sig

  subObjectPropertyOf :
    SubObjectPropertyExpression Sig →
    ObjectPropertyExpression Sig →
    Axiom Sig
  equivalentObjectProperties :
    AtLeastTwo (ObjectPropertyExpression Sig) → Axiom Sig
  disjointObjectProperties :
    AtLeastTwo (SimpleObjectPropertyName Sig) → Axiom Sig
  inverseObjectProperties :
    ObjectPropertyExpression Sig →
    ObjectPropertyExpression Sig →
    Axiom Sig
  objectPropertyDomain :
    ObjectPropertyExpression Sig →
    ClassExpression Sig →
    Axiom Sig
  objectPropertyRange :
    ObjectPropertyExpression Sig →
    ClassExpression Sig →
    Axiom Sig
  functionalObjectProperty :
    SimpleObjectPropertyName Sig → Axiom Sig
  inverseFunctionalObjectProperty :
    SimpleObjectPropertyName Sig → Axiom Sig
  reflexiveObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  irreflexiveObjectProperty :
    SimpleObjectPropertyName Sig → Axiom Sig
  symmetricObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  asymmetricObjectProperty :
    SimpleObjectPropertyName Sig → Axiom Sig
  transitiveObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig

  subDataPropertyOf :
    DataPropertyExpression Sig →
    DataPropertyExpression Sig →
    Axiom Sig
  equivalentDataProperties :
    AtLeastTwo (DataPropertyExpression Sig) → Axiom Sig
  disjointDataProperties :
    AtLeastTwo (DataPropertyExpression Sig) → Axiom Sig
  dataPropertyDomain :
    DataPropertyExpression Sig →
    ClassExpression Sig →
    Axiom Sig
  dataPropertyRange :
    DataPropertyExpression Sig →
    DataRange Sig →
    Axiom Sig
  functionalDataProperty :
    DataPropertyExpression Sig → Axiom Sig

  datatypeDefinition :
    (name : DatatypeName Sig) →
    DatatypeSupported Sig name →
    DataRange Sig →
    Axiom Sig
  hasKey :
    ClassExpression Sig → PropertyKey Sig → Axiom Sig

  sameIndividual :
    AtLeastTwo (Individual Sig) → Axiom Sig
  differentIndividuals :
    AtLeastTwo (Individual Sig) → Axiom Sig
  classAssertion :
    ClassExpression Sig → Individual Sig → Axiom Sig
  objectPropertyAssertion :
    ObjectPropertyExpression Sig →
    Individual Sig →
    Individual Sig →
    Axiom Sig
  negativeObjectPropertyAssertion :
    ObjectPropertyExpression Sig →
    Individual Sig →
    Individual Sig →
    Axiom Sig
  dataPropertyAssertion :
    DataPropertyExpression Sig →
    Individual Sig →
    Literal Sig →
    Axiom Sig
  negativeDataPropertyAssertion :
    DataPropertyExpression Sig →
    Individual Sig →
    Literal Sig →
    Axiom Sig

  annotationAssertion :
    AnnotationPropertyName Sig →
    AnnotationSubject Sig →
    AnnotationValue Sig →
    Axiom Sig
  subAnnotationPropertyOf :
    AnnotationPropertyName Sig →
    AnnotationPropertyName Sig →
    Axiom Sig
  annotationPropertyDomain :
    AnnotationPropertyName Sig →
    IRIName Sig →
    Axiom Sig
  annotationPropertyRange :
    AnnotationPropertyName Sig →
    IRIName Sig →
    Axiom Sig

AxiomPropertyChainFree :
  {Sig : Signature} →
  Axiom Sig →
  Type₀
AxiomPropertyChainFree
  (subObjectPropertyOf (subObjectPropertyChain chain) sup) =
  ⊥
AxiomPropertyChainFree axiom =
  Unit

AxiomsPropertyChainFree :
  {Sig : Signature} →
  List (Axiom Sig) →
  Type₀
AxiomsPropertyChainFree [] =
  Unit
AxiomsPropertyChainFree (axiom ∷ axioms) =
  AxiomPropertyChainFree axiom × AxiomsPropertyChainFree axioms

axiomsPropertyChainFreeAppend :
  {Sig : Signature} →
  (left right : List (Axiom Sig)) →
  AxiomsPropertyChainFree left →
  AxiomsPropertyChainFree right →
  AxiomsPropertyChainFree (left ++ right)
axiomsPropertyChainFreeAppend [] right leftFree rightFree =
  rightFree
axiomsPropertyChainFreeAppend
  (axiom ∷ left)
  right
  (head , tail)
  rightFree =
  head , axiomsPropertyChainFreeAppend left right tail rightFree

axiomPropertyChainFree? :
  {Sig : Signature} →
  (axiom : Axiom Sig) →
  Optional (AxiomPropertyChainFree axiom)
axiomPropertyChainFree? (declaration entity) =
  present tt
axiomPropertyChainFree? (subClassOf sub sup) =
  present tt
axiomPropertyChainFree? (equivalentClasses classes) =
  present tt
axiomPropertyChainFree? (disjointClasses classes) =
  present tt
axiomPropertyChainFree? (disjointUnion class classes) =
  present tt
axiomPropertyChainFree? (subObjectPropertyOf (subObjectProperty property) sup) =
  present tt
axiomPropertyChainFree?
  (subObjectPropertyOf (subObjectPropertyChain chain) sup) =
  absent
axiomPropertyChainFree? (equivalentObjectProperties properties) =
  present tt
axiomPropertyChainFree? (disjointObjectProperties properties) =
  present tt
axiomPropertyChainFree? (inverseObjectProperties left right) =
  present tt
axiomPropertyChainFree? (objectPropertyDomain property class) =
  present tt
axiomPropertyChainFree? (objectPropertyRange property class) =
  present tt
axiomPropertyChainFree? (functionalObjectProperty property) =
  present tt
axiomPropertyChainFree? (inverseFunctionalObjectProperty property) =
  present tt
axiomPropertyChainFree? (reflexiveObjectProperty property) =
  present tt
axiomPropertyChainFree? (irreflexiveObjectProperty property) =
  present tt
axiomPropertyChainFree? (symmetricObjectProperty property) =
  present tt
axiomPropertyChainFree? (asymmetricObjectProperty property) =
  present tt
axiomPropertyChainFree? (transitiveObjectProperty property) =
  present tt
axiomPropertyChainFree? (subDataPropertyOf sub sup) =
  present tt
axiomPropertyChainFree? (equivalentDataProperties properties) =
  present tt
axiomPropertyChainFree? (disjointDataProperties properties) =
  present tt
axiomPropertyChainFree? (dataPropertyDomain property class) =
  present tt
axiomPropertyChainFree? (dataPropertyRange property range) =
  present tt
axiomPropertyChainFree? (functionalDataProperty property) =
  present tt
axiomPropertyChainFree? (datatypeDefinition name support range) =
  present tt
axiomPropertyChainFree? (hasKey class key) =
  present tt
axiomPropertyChainFree? (sameIndividual individuals) =
  present tt
axiomPropertyChainFree? (differentIndividuals individuals) =
  present tt
axiomPropertyChainFree? (classAssertion class individual) =
  present tt
axiomPropertyChainFree?
  (objectPropertyAssertion property subject object) =
  present tt
axiomPropertyChainFree?
  (negativeObjectPropertyAssertion property subject object) =
  present tt
axiomPropertyChainFree? (dataPropertyAssertion property subject literal) =
  present tt
axiomPropertyChainFree?
  (negativeDataPropertyAssertion property subject literal) =
  present tt
axiomPropertyChainFree? (annotationAssertion property subject value) =
  present tt
axiomPropertyChainFree? (subAnnotationPropertyOf sub sup) =
  present tt
axiomPropertyChainFree? (annotationPropertyDomain property iri) =
  present tt
axiomPropertyChainFree? (annotationPropertyRange property iri) =
  present tt

mutual
  LiteralDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    Literal Sig →
    Type₀
  LiteralDatatypeSupportedBy map (typedLiteral lexical dtype support) =
    canonicalLiteralDatatype map (supportedLiteralDatatypeName support) ≡
    dtype

  FacetRestrictionDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    FacetRestriction Sig →
    Type₀
  FacetRestrictionDatatypeSupportedBy map restriction =
    LiteralDatatypeSupportedBy map (value restriction)

  FacetRestrictionsDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    List (FacetRestriction Sig) →
    Type₀
  FacetRestrictionsDatatypeSupportedBy map [] =
    Unit
  FacetRestrictionsDatatypeSupportedBy map (restriction ∷ restrictions) =
    FacetRestrictionDatatypeSupportedBy map restriction ×
    FacetRestrictionsDatatypeSupportedBy map restrictions

  DataRangeDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    DataRange Sig →
    Type₀
  DataRangeDatatypeSupportedBy map (datatype name support) =
    canonicalDatatype map (supportedDatatypeName support) ≡ name
  DataRangeDatatypeSupportedBy map dataTop =
    Unit
  DataRangeDatatypeSupportedBy map dataBottom =
    Unit
  DataRangeDatatypeSupportedBy map (dataComplementOf range) =
    DataRangeDatatypeSupportedBy map range
  DataRangeDatatypeSupportedBy map (dataIntersectionOf ranges) =
    NonEmptyDataRangesDatatypeSupportedBy map ranges
  DataRangeDatatypeSupportedBy map (dataUnionOf ranges) =
    NonEmptyDataRangesDatatypeSupportedBy map ranges
  DataRangeDatatypeSupportedBy map (dataOneOf literals) =
    NonEmptyLiteralsDatatypeSupportedBy map literals
  DataRangeDatatypeSupportedBy map (datatypeRestriction name support facets) =
    (canonicalDatatype map (supportedDatatypeName support) ≡ name) ×
    FacetRestrictionsDatatypeSupportedBy map facets

  DataRangesDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    List (DataRange Sig) →
    Type₀
  DataRangesDatatypeSupportedBy map [] =
    Unit
  DataRangesDatatypeSupportedBy map (range ∷ ranges) =
    DataRangeDatatypeSupportedBy map range ×
    DataRangesDatatypeSupportedBy map ranges

  NonEmptyDataRangesDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    NonEmpty (DataRange Sig) →
    Type₀
  NonEmptyDataRangesDatatypeSupportedBy map (nonEmpty head tail) =
    DataRangeDatatypeSupportedBy map head ×
    DataRangesDatatypeSupportedBy map tail

  LiteralsDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    List (Literal Sig) →
    Type₀
  LiteralsDatatypeSupportedBy map [] =
    Unit
  LiteralsDatatypeSupportedBy map (literal ∷ literals) =
    LiteralDatatypeSupportedBy map literal ×
    LiteralsDatatypeSupportedBy map literals

  NonEmptyLiteralsDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    NonEmpty (Literal Sig) →
    Type₀
  NonEmptyLiteralsDatatypeSupportedBy map (nonEmpty head tail) =
    LiteralDatatypeSupportedBy map head ×
    LiteralsDatatypeSupportedBy map tail

mutual
  OptionalClassExpressionDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    Optional (ClassExpression Sig) →
    Type₀
  OptionalClassExpressionDatatypeSupportedBy map absent =
    Unit
  OptionalClassExpressionDatatypeSupportedBy map (present class) =
    ClassExpressionDatatypeSupportedBy map class

  OptionalDataRangeDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    Optional (DataRange Sig) →
    Type₀
  OptionalDataRangeDatatypeSupportedBy map absent =
    Unit
  OptionalDataRangeDatatypeSupportedBy map (present range) =
    DataRangeDatatypeSupportedBy map range

  ClassExpressionDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    ClassExpression Sig →
    Type₀
  ClassExpressionDatatypeSupportedBy map (namedClass name) =
    Unit
  ClassExpressionDatatypeSupportedBy map owlThing =
    Unit
  ClassExpressionDatatypeSupportedBy map owlNothing =
    Unit
  ClassExpressionDatatypeSupportedBy map (objectIntersectionOf classes) =
    NonEmptyClassesDatatypeSupportedBy map classes
  ClassExpressionDatatypeSupportedBy map (objectUnionOf classes) =
    NonEmptyClassesDatatypeSupportedBy map classes
  ClassExpressionDatatypeSupportedBy map (objectComplementOf class) =
    ClassExpressionDatatypeSupportedBy map class
  ClassExpressionDatatypeSupportedBy map (objectOneOf individuals) =
    Unit
  ClassExpressionDatatypeSupportedBy map (objectSomeValuesFrom property class) =
    ClassExpressionDatatypeSupportedBy map class
  ClassExpressionDatatypeSupportedBy map (objectAllValuesFrom property class) =
    ClassExpressionDatatypeSupportedBy map class
  ClassExpressionDatatypeSupportedBy map (objectHasValue property individual) =
    Unit
  ClassExpressionDatatypeSupportedBy map (objectHasSelf property) =
    Unit
  ClassExpressionDatatypeSupportedBy map (objectMinCardinality n property class) =
    OptionalClassExpressionDatatypeSupportedBy map class
  ClassExpressionDatatypeSupportedBy map (objectMaxCardinality n property class) =
    OptionalClassExpressionDatatypeSupportedBy map class
  ClassExpressionDatatypeSupportedBy map (objectExactCardinality n property class) =
    OptionalClassExpressionDatatypeSupportedBy map class
  ClassExpressionDatatypeSupportedBy map (dataSomeValuesFrom property range) =
    DataRangeDatatypeSupportedBy map range
  ClassExpressionDatatypeSupportedBy map (dataAllValuesFrom property range) =
    DataRangeDatatypeSupportedBy map range
  ClassExpressionDatatypeSupportedBy map (dataHasValue property literal) =
    LiteralDatatypeSupportedBy map literal
  ClassExpressionDatatypeSupportedBy map (dataMinCardinality n property range) =
    OptionalDataRangeDatatypeSupportedBy map range
  ClassExpressionDatatypeSupportedBy map (dataMaxCardinality n property range) =
    OptionalDataRangeDatatypeSupportedBy map range
  ClassExpressionDatatypeSupportedBy map (dataExactCardinality n property range) =
    OptionalDataRangeDatatypeSupportedBy map range

  ClassesDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    List (ClassExpression Sig) →
    Type₀
  ClassesDatatypeSupportedBy map [] =
    Unit
  ClassesDatatypeSupportedBy map (class ∷ classes) =
    ClassExpressionDatatypeSupportedBy map class ×
    ClassesDatatypeSupportedBy map classes

  NonEmptyClassesDatatypeSupportedBy :
    {Sig : Signature} →
    DatatypeMap Sig →
    NonEmpty (ClassExpression Sig) →
    Type₀
  NonEmptyClassesDatatypeSupportedBy map (nonEmpty head tail) =
    ClassExpressionDatatypeSupportedBy map head ×
    ClassesDatatypeSupportedBy map tail

ListDatatypeSupportedBy :
  {A : Type₀} →
  (A → Type₀) →
  List A →
  Type₀
ListDatatypeSupportedBy P [] =
  Unit
ListDatatypeSupportedBy P (x ∷ xs) =
  P x × ListDatatypeSupportedBy P xs

AtLeastTwoDatatypeSupportedBy :
  {Sig : Signature} {A : Type₀} →
  DatatypeMap Sig →
  (A → Type₀) →
  AtLeastTwo A →
  Type₀
AtLeastTwoDatatypeSupportedBy map P (atLeastTwo first second rest) =
  P first × P second × ListDatatypeSupportedBy P rest

AnnotationValueDatatypeSupportedBy :
  {Sig : Signature} →
  DatatypeMap Sig →
  AnnotationValue Sig →
  Type₀
AnnotationValueDatatypeSupportedBy map (annotationValueIRI iri) =
  Unit
AnnotationValueDatatypeSupportedBy map (annotationValueAnonymous name) =
  Unit
AnnotationValueDatatypeSupportedBy map (annotationValueLiteral literal) =
  LiteralDatatypeSupportedBy map literal

AxiomDatatypeSupportedBy :
  {Sig : Signature} →
  DatatypeMap Sig →
  Axiom Sig →
  Type₀
AxiomDatatypeSupportedBy map (declaration entity) =
  Unit
AxiomDatatypeSupportedBy map (subClassOf sub sup) =
  ClassExpressionDatatypeSupportedBy map sub ×
  ClassExpressionDatatypeSupportedBy map sup
AxiomDatatypeSupportedBy map (equivalentClasses classes) =
  AtLeastTwoDatatypeSupportedBy map (ClassExpressionDatatypeSupportedBy map) classes
AxiomDatatypeSupportedBy map (disjointClasses classes) =
  AtLeastTwoDatatypeSupportedBy map (ClassExpressionDatatypeSupportedBy map) classes
AxiomDatatypeSupportedBy map (disjointUnion class classes) =
  AtLeastTwoDatatypeSupportedBy map (ClassExpressionDatatypeSupportedBy map) classes
AxiomDatatypeSupportedBy map (subObjectPropertyOf sub sup) =
  Unit
AxiomDatatypeSupportedBy map (equivalentObjectProperties properties) =
  Unit
AxiomDatatypeSupportedBy map (disjointObjectProperties properties) =
  Unit
AxiomDatatypeSupportedBy map (inverseObjectProperties left right) =
  Unit
AxiomDatatypeSupportedBy map (objectPropertyDomain property class) =
  ClassExpressionDatatypeSupportedBy map class
AxiomDatatypeSupportedBy map (objectPropertyRange property class) =
  ClassExpressionDatatypeSupportedBy map class
AxiomDatatypeSupportedBy map (functionalObjectProperty property) =
  Unit
AxiomDatatypeSupportedBy map (inverseFunctionalObjectProperty property) =
  Unit
AxiomDatatypeSupportedBy map (reflexiveObjectProperty property) =
  Unit
AxiomDatatypeSupportedBy map (irreflexiveObjectProperty property) =
  Unit
AxiomDatatypeSupportedBy map (symmetricObjectProperty property) =
  Unit
AxiomDatatypeSupportedBy map (asymmetricObjectProperty property) =
  Unit
AxiomDatatypeSupportedBy map (transitiveObjectProperty property) =
  Unit
AxiomDatatypeSupportedBy map (subDataPropertyOf sub sup) =
  Unit
AxiomDatatypeSupportedBy map (equivalentDataProperties properties) =
  Unit
AxiomDatatypeSupportedBy map (disjointDataProperties properties) =
  Unit
AxiomDatatypeSupportedBy map (dataPropertyDomain property class) =
  ClassExpressionDatatypeSupportedBy map class
AxiomDatatypeSupportedBy map (dataPropertyRange property range) =
  DataRangeDatatypeSupportedBy map range
AxiomDatatypeSupportedBy map (functionalDataProperty property) =
  Unit
AxiomDatatypeSupportedBy map (datatypeDefinition name support range) =
  (canonicalDatatype map (supportedDatatypeName support) ≡ name) ×
  DataRangeDatatypeSupportedBy map range
AxiomDatatypeSupportedBy map (hasKey class key) =
  ClassExpressionDatatypeSupportedBy map class
AxiomDatatypeSupportedBy map (sameIndividual individuals) =
  Unit
AxiomDatatypeSupportedBy map (differentIndividuals individuals) =
  Unit
AxiomDatatypeSupportedBy map (classAssertion class individual) =
  ClassExpressionDatatypeSupportedBy map class
AxiomDatatypeSupportedBy map (objectPropertyAssertion property subject object) =
  Unit
AxiomDatatypeSupportedBy map (negativeObjectPropertyAssertion property subject object) =
  Unit
AxiomDatatypeSupportedBy map (dataPropertyAssertion property subject literal) =
  LiteralDatatypeSupportedBy map literal
AxiomDatatypeSupportedBy map (negativeDataPropertyAssertion property subject literal) =
  LiteralDatatypeSupportedBy map literal
AxiomDatatypeSupportedBy map (annotationAssertion property subject value) =
  AnnotationValueDatatypeSupportedBy map value
AxiomDatatypeSupportedBy map (subAnnotationPropertyOf sub sup) =
  Unit
AxiomDatatypeSupportedBy map (annotationPropertyDomain property iri) =
  Unit
AxiomDatatypeSupportedBy map (annotationPropertyRange property iri) =
  Unit

AxiomsDatatypeSupportedBy :
  {Sig : Signature} →
  DatatypeMap Sig →
  List (Axiom Sig) →
  Type₀
AxiomsDatatypeSupportedBy map [] =
  Unit
AxiomsDatatypeSupportedBy map (axiom ∷ axioms) =
  AxiomDatatypeSupportedBy map axiom ×
  AxiomsDatatypeSupportedBy map axioms

mutual
  completeLiteralDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (literal : Literal Sig) →
    LiteralDatatypeSupportedBy map literal
  completeLiteralDatatypeSupportedBy map
    (typedLiteral lexical dtype support) =
    cong
      (canonicalLiteralDatatype map)
      (supportedLiteralDatatypeMatches support)
    ∙ canonicalLiteralDatatypeMatches map dtype

  completeFacetRestrictionDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (restriction : FacetRestriction Sig) →
    FacetRestrictionDatatypeSupportedBy map restriction
  completeFacetRestrictionDatatypeSupportedBy map restriction =
    completeLiteralDatatypeSupportedBy map (value restriction)

  completeFacetRestrictionsDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (restrictions : List (FacetRestriction Sig)) →
    FacetRestrictionsDatatypeSupportedBy map restrictions
  completeFacetRestrictionsDatatypeSupportedBy map [] =
    tt
  completeFacetRestrictionsDatatypeSupportedBy map (restriction ∷ restrictions) =
    completeFacetRestrictionDatatypeSupportedBy map restriction ,
    completeFacetRestrictionsDatatypeSupportedBy map restrictions

  completeDataRangeDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (range : DataRange Sig) →
    DataRangeDatatypeSupportedBy map range
  completeDataRangeDatatypeSupportedBy map (datatype name support) =
    cong (canonicalDatatype map) (supportedDatatypeMatches support) ∙
    canonicalDatatypeMatches map name
  completeDataRangeDatatypeSupportedBy map dataTop =
    tt
  completeDataRangeDatatypeSupportedBy map dataBottom =
    tt
  completeDataRangeDatatypeSupportedBy map (dataComplementOf range) =
    completeDataRangeDatatypeSupportedBy map range
  completeDataRangeDatatypeSupportedBy map (dataIntersectionOf ranges) =
    completeNonEmptyDataRangesDatatypeSupportedBy map ranges
  completeDataRangeDatatypeSupportedBy map (dataUnionOf ranges) =
    completeNonEmptyDataRangesDatatypeSupportedBy map ranges
  completeDataRangeDatatypeSupportedBy map (dataOneOf literals) =
    completeNonEmptyLiteralsDatatypeSupportedBy map literals
  completeDataRangeDatatypeSupportedBy map
    (datatypeRestriction name support facets) =
    ( cong (canonicalDatatype map) (supportedDatatypeMatches support) ∙
      canonicalDatatypeMatches map name
    ) ,
    completeFacetRestrictionsDatatypeSupportedBy map facets

  completeDataRangesDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (ranges : List (DataRange Sig)) →
    DataRangesDatatypeSupportedBy map ranges
  completeDataRangesDatatypeSupportedBy map [] =
    tt
  completeDataRangesDatatypeSupportedBy map (range ∷ ranges) =
    completeDataRangeDatatypeSupportedBy map range ,
    completeDataRangesDatatypeSupportedBy map ranges

  completeNonEmptyDataRangesDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (ranges : NonEmpty (DataRange Sig)) →
    NonEmptyDataRangesDatatypeSupportedBy map ranges
  completeNonEmptyDataRangesDatatypeSupportedBy map (nonEmpty head tail) =
    completeDataRangeDatatypeSupportedBy map head ,
    completeDataRangesDatatypeSupportedBy map tail

  completeLiteralsDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (literals : List (Literal Sig)) →
    LiteralsDatatypeSupportedBy map literals
  completeLiteralsDatatypeSupportedBy map [] =
    tt
  completeLiteralsDatatypeSupportedBy map (literal ∷ literals) =
    completeLiteralDatatypeSupportedBy map literal ,
    completeLiteralsDatatypeSupportedBy map literals

  completeNonEmptyLiteralsDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (literals : NonEmpty (Literal Sig)) →
    NonEmptyLiteralsDatatypeSupportedBy map literals
  completeNonEmptyLiteralsDatatypeSupportedBy map (nonEmpty head tail) =
    completeLiteralDatatypeSupportedBy map head ,
    completeLiteralsDatatypeSupportedBy map tail

mutual
  completeOptionalClassExpressionDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (class? : Optional (ClassExpression Sig)) →
    OptionalClassExpressionDatatypeSupportedBy map class?
  completeOptionalClassExpressionDatatypeSupportedBy map absent =
    tt
  completeOptionalClassExpressionDatatypeSupportedBy map (present class) =
    completeClassExpressionDatatypeSupportedBy map class

  completeOptionalDataRangeDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (range? : Optional (DataRange Sig)) →
    OptionalDataRangeDatatypeSupportedBy map range?
  completeOptionalDataRangeDatatypeSupportedBy map absent =
    tt
  completeOptionalDataRangeDatatypeSupportedBy map (present range) =
    completeDataRangeDatatypeSupportedBy map range

  completeClassExpressionDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (class : ClassExpression Sig) →
    ClassExpressionDatatypeSupportedBy map class
  completeClassExpressionDatatypeSupportedBy map (namedClass name) =
    tt
  completeClassExpressionDatatypeSupportedBy map owlThing =
    tt
  completeClassExpressionDatatypeSupportedBy map owlNothing =
    tt
  completeClassExpressionDatatypeSupportedBy map
    (objectIntersectionOf classes) =
    completeNonEmptyClassesDatatypeSupportedBy map classes
  completeClassExpressionDatatypeSupportedBy map (objectUnionOf classes) =
    completeNonEmptyClassesDatatypeSupportedBy map classes
  completeClassExpressionDatatypeSupportedBy map (objectComplementOf class) =
    completeClassExpressionDatatypeSupportedBy map class
  completeClassExpressionDatatypeSupportedBy map (objectOneOf individuals) =
    tt
  completeClassExpressionDatatypeSupportedBy map
    (objectSomeValuesFrom property class) =
    completeClassExpressionDatatypeSupportedBy map class
  completeClassExpressionDatatypeSupportedBy map
    (objectAllValuesFrom property class) =
    completeClassExpressionDatatypeSupportedBy map class
  completeClassExpressionDatatypeSupportedBy map
    (objectHasValue property individual) =
    tt
  completeClassExpressionDatatypeSupportedBy map (objectHasSelf property) =
    tt
  completeClassExpressionDatatypeSupportedBy map
    (objectMinCardinality n property class) =
    completeOptionalClassExpressionDatatypeSupportedBy map class
  completeClassExpressionDatatypeSupportedBy map
    (objectMaxCardinality n property class) =
    completeOptionalClassExpressionDatatypeSupportedBy map class
  completeClassExpressionDatatypeSupportedBy map
    (objectExactCardinality n property class) =
    completeOptionalClassExpressionDatatypeSupportedBy map class
  completeClassExpressionDatatypeSupportedBy map
    (dataSomeValuesFrom property range) =
    completeDataRangeDatatypeSupportedBy map range
  completeClassExpressionDatatypeSupportedBy map
    (dataAllValuesFrom property range) =
    completeDataRangeDatatypeSupportedBy map range
  completeClassExpressionDatatypeSupportedBy map
    (dataHasValue property literal) =
    completeLiteralDatatypeSupportedBy map literal
  completeClassExpressionDatatypeSupportedBy map
    (dataMinCardinality n property range) =
    completeOptionalDataRangeDatatypeSupportedBy map range
  completeClassExpressionDatatypeSupportedBy map
    (dataMaxCardinality n property range) =
    completeOptionalDataRangeDatatypeSupportedBy map range
  completeClassExpressionDatatypeSupportedBy map
    (dataExactCardinality n property range) =
    completeOptionalDataRangeDatatypeSupportedBy map range

  completeClassesDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (classes : List (ClassExpression Sig)) →
    ClassesDatatypeSupportedBy map classes
  completeClassesDatatypeSupportedBy map [] =
    tt
  completeClassesDatatypeSupportedBy map (class ∷ classes) =
    completeClassExpressionDatatypeSupportedBy map class ,
    completeClassesDatatypeSupportedBy map classes

  completeNonEmptyClassesDatatypeSupportedBy :
    {Sig : Signature} →
    (map : DatatypeMap Sig) →
    (classes : NonEmpty (ClassExpression Sig)) →
    NonEmptyClassesDatatypeSupportedBy map classes
  completeNonEmptyClassesDatatypeSupportedBy map (nonEmpty head tail) =
    completeClassExpressionDatatypeSupportedBy map head ,
    completeClassesDatatypeSupportedBy map tail

completeListDatatypeSupportedBy :
  {A : Type₀} →
  (P : A → Type₀) →
  ((value : A) → P value) →
  (values : List A) →
  ListDatatypeSupportedBy P values
completeListDatatypeSupportedBy P supported [] =
  tt
completeListDatatypeSupportedBy P supported (value ∷ values) =
  supported value ,
  completeListDatatypeSupportedBy P supported values

completeAtLeastTwoDatatypeSupportedBy :
  {Sig : Signature} {A : Type₀} →
  (map : DatatypeMap Sig) →
  (P : A → Type₀) →
  ((value : A) → P value) →
  (values : AtLeastTwo A) →
  AtLeastTwoDatatypeSupportedBy map P values
completeAtLeastTwoDatatypeSupportedBy map P supported
  (atLeastTwo first second rest) =
  supported first ,
  supported second ,
  completeListDatatypeSupportedBy P supported rest

completeAnnotationValueDatatypeSupportedBy :
  {Sig : Signature} →
  (map : DatatypeMap Sig) →
  (value : AnnotationValue Sig) →
  AnnotationValueDatatypeSupportedBy map value
completeAnnotationValueDatatypeSupportedBy map (annotationValueIRI iri) =
  tt
completeAnnotationValueDatatypeSupportedBy map
  (annotationValueAnonymous name) =
  tt
completeAnnotationValueDatatypeSupportedBy map
  (annotationValueLiteral literal) =
  completeLiteralDatatypeSupportedBy map literal

completeAxiomDatatypeSupportedBy :
  {Sig : Signature} →
  (map : DatatypeMap Sig) →
  (axiom : Axiom Sig) →
  AxiomDatatypeSupportedBy map axiom
completeAxiomDatatypeSupportedBy map (declaration entity) =
  tt
completeAxiomDatatypeSupportedBy map (subClassOf sub sup) =
  completeClassExpressionDatatypeSupportedBy map sub ,
  completeClassExpressionDatatypeSupportedBy map sup
completeAxiomDatatypeSupportedBy map (equivalentClasses classes) =
  completeAtLeastTwoDatatypeSupportedBy
    map
    (ClassExpressionDatatypeSupportedBy map)
    (completeClassExpressionDatatypeSupportedBy map)
    classes
completeAxiomDatatypeSupportedBy map (disjointClasses classes) =
  completeAtLeastTwoDatatypeSupportedBy
    map
    (ClassExpressionDatatypeSupportedBy map)
    (completeClassExpressionDatatypeSupportedBy map)
    classes
completeAxiomDatatypeSupportedBy map (disjointUnion class classes) =
  completeAtLeastTwoDatatypeSupportedBy
    map
    (ClassExpressionDatatypeSupportedBy map)
    (completeClassExpressionDatatypeSupportedBy map)
    classes
completeAxiomDatatypeSupportedBy map (subObjectPropertyOf sub sup) =
  tt
completeAxiomDatatypeSupportedBy map (equivalentObjectProperties properties) =
  tt
completeAxiomDatatypeSupportedBy map (disjointObjectProperties properties) =
  tt
completeAxiomDatatypeSupportedBy map (inverseObjectProperties left right) =
  tt
completeAxiomDatatypeSupportedBy map (objectPropertyDomain property class) =
  completeClassExpressionDatatypeSupportedBy map class
completeAxiomDatatypeSupportedBy map (objectPropertyRange property class) =
  completeClassExpressionDatatypeSupportedBy map class
completeAxiomDatatypeSupportedBy map (functionalObjectProperty property) =
  tt
completeAxiomDatatypeSupportedBy map
  (inverseFunctionalObjectProperty property) =
  tt
completeAxiomDatatypeSupportedBy map (reflexiveObjectProperty property) =
  tt
completeAxiomDatatypeSupportedBy map (irreflexiveObjectProperty property) =
  tt
completeAxiomDatatypeSupportedBy map (symmetricObjectProperty property) =
  tt
completeAxiomDatatypeSupportedBy map (asymmetricObjectProperty property) =
  tt
completeAxiomDatatypeSupportedBy map (transitiveObjectProperty property) =
  tt
completeAxiomDatatypeSupportedBy map (subDataPropertyOf sub sup) =
  tt
completeAxiomDatatypeSupportedBy map (equivalentDataProperties properties) =
  tt
completeAxiomDatatypeSupportedBy map (disjointDataProperties properties) =
  tt
completeAxiomDatatypeSupportedBy map (dataPropertyDomain property class) =
  completeClassExpressionDatatypeSupportedBy map class
completeAxiomDatatypeSupportedBy map (dataPropertyRange property range) =
  completeDataRangeDatatypeSupportedBy map range
completeAxiomDatatypeSupportedBy map (functionalDataProperty property) =
  tt
completeAxiomDatatypeSupportedBy map (datatypeDefinition name support range) =
  ( cong (canonicalDatatype map) (supportedDatatypeMatches support) ∙
    canonicalDatatypeMatches map name
  ) ,
  completeDataRangeDatatypeSupportedBy map range
completeAxiomDatatypeSupportedBy map (hasKey class key) =
  completeClassExpressionDatatypeSupportedBy map class
completeAxiomDatatypeSupportedBy map (sameIndividual individuals) =
  tt
completeAxiomDatatypeSupportedBy map (differentIndividuals individuals) =
  tt
completeAxiomDatatypeSupportedBy map (classAssertion class individual) =
  completeClassExpressionDatatypeSupportedBy map class
completeAxiomDatatypeSupportedBy map
  (objectPropertyAssertion property subject object) =
  tt
completeAxiomDatatypeSupportedBy map
  (negativeObjectPropertyAssertion property subject object) =
  tt
completeAxiomDatatypeSupportedBy map
  (dataPropertyAssertion property subject literal) =
  completeLiteralDatatypeSupportedBy map literal
completeAxiomDatatypeSupportedBy map
  (negativeDataPropertyAssertion property subject literal) =
  completeLiteralDatatypeSupportedBy map literal
completeAxiomDatatypeSupportedBy map
  (annotationAssertion property subject value) =
  completeAnnotationValueDatatypeSupportedBy map value
completeAxiomDatatypeSupportedBy map (subAnnotationPropertyOf sub sup) =
  tt
completeAxiomDatatypeSupportedBy map (annotationPropertyDomain property iri) =
  tt
completeAxiomDatatypeSupportedBy map (annotationPropertyRange property iri) =
  tt

completeAxiomsDatatypeSupportedBy :
  {Sig : Signature} →
  (map : DatatypeMap Sig) →
  (axioms : List (Axiom Sig)) →
  AxiomsDatatypeSupportedBy map axioms
completeAxiomsDatatypeSupportedBy map [] =
  tt
completeAxiomsDatatypeSupportedBy map (axiom ∷ axioms) =
  completeAxiomDatatypeSupportedBy map axiom ,
  completeAxiomsDatatypeSupportedBy map axioms

record OntologyDatatypeSupport
  (Sig : Signature) (axioms : List (Axiom Sig)) : Type₀ where
  constructor ontologyDatatypeSupport
  field
    supportedDatatypeMap : DatatypeMap Sig
    supportedAxioms      : AxiomsDatatypeSupportedBy supportedDatatypeMap axioms

open OntologyDatatypeSupport public

completeOntologyDatatypeSupport :
  {Sig : Signature} →
  (axioms : List (Axiom Sig)) →
  OntologyDatatypeSupport Sig axioms
completeOntologyDatatypeSupport axioms =
  ontologyDatatypeSupport
    trivialDatatypeMap
    (completeAxiomsDatatypeSupportedBy trivialDatatypeMap axioms)

record OntologyRegularity
  (Sig : Signature) (axioms : List (Axiom Sig)) : Type₀ where
  constructor ontologyRegularity
  field
    ontologyRegularityContext :
      RegularityContext Sig
    propertyChainsFree :
      AxiomsPropertyChainFree axioms

open OntologyRegularity public

record Ontology (Sig : Signature) : Type₀ where
  constructor ontology
  field
    ontologyAnnotations : List (Annotation Sig)
    annotatedAxioms     : List (Annotated Sig (Axiom Sig))
    axioms              : List (Axiom Sig)
    annotationErasure   : annotatedBodies annotatedAxioms ≡ axioms
    datatypeSupport : OntologyDatatypeSupport Sig axioms
    regularity      : OntologyRegularity Sig axioms

open Ontology public

plainAnnotatedAxioms :
  {Sig : Signature} →
  List (Axiom Sig) →
  List (Annotated Sig (Axiom Sig))
plainAnnotatedAxioms [] =
  []
plainAnnotatedAxioms (axiom ∷ axioms) =
  annotated [] axiom ∷ plainAnnotatedAxioms axioms

plainAnnotatedAxiomsErase :
  {Sig : Signature} →
  (axioms : List (Axiom Sig)) →
  annotatedBodies (plainAnnotatedAxioms axioms) ≡ axioms
plainAnnotatedAxiomsErase [] =
  refl
plainAnnotatedAxiomsErase (axiom ∷ axioms) =
  cong (λ rest → axiom ∷ rest) (plainAnnotatedAxiomsErase axioms)

plainOntology :
  {Sig : Signature} →
  (axioms : List (Axiom Sig)) →
  OntologyDatatypeSupport Sig axioms →
  OntologyRegularity Sig axioms →
  Ontology Sig
plainOntology axioms datatypeSupport regularity =
  ontology
    []
    (plainAnnotatedAxioms axioms)
    axioms
    (plainAnnotatedAxiomsErase axioms)
    datatypeSupport
    regularity

emptyOntology :
  {Sig : Signature} →
  OntologyDatatypeSupport Sig [] →
  OntologyRegularity Sig [] →
  Ontology Sig
emptyOntology datatypeSupport regularity =
  ontology [] [] [] refl datatypeSupport regularity

appendOntologies :
  {Sig : Signature} →
  RegularityContext Sig →
  Ontology Sig →
  Ontology Sig →
  Ontology Sig
appendOntologies context left right =
  ontology
    (ontologyAnnotations left ++ ontologyAnnotations right)
    (annotatedAxioms left ++ annotatedAxioms right)
    (axioms left ++ axioms right)
    ( annotatedBodiesAppend (annotatedAxioms left) (annotatedAxioms right)
    ∙ cong₂ _++_ (annotationErasure left) (annotationErasure right)
    )
    (completeOntologyDatatypeSupport (axioms left ++ axioms right))
    (ontologyRegularity
      context
      (axiomsPropertyChainFreeAppend
        (axioms left)
        (axioms right)
        (propertyChainsFree (regularity left))
        (propertyChainsFree (regularity right))))