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

module OWL2.Kernel.Morphism where

open import OWL2.Prelude
open import OWL2.Kernel.DatatypeMap
  using (datatypeSupported; literalSupported)
open import OWL2.Kernel.Regularity
  using (RegularityContext)
open import OWL2.Kernel.Syntax

record SignatureMorphism (Source Target : Signature) : Type₀ where
  constructor signatureMorphism
  field
    mapClassName :
      ClassName Source → ClassName Target
    mapObjectPropertyName :
      ObjectPropertyName Source → ObjectPropertyName Target
    mapDataPropertyName :
      DataPropertyName Source → DataPropertyName Target
    mapAnnotationPropertyName :
      AnnotationPropertyName Source → AnnotationPropertyName Target
    mapDatatypeName :
      DatatypeName Source → DatatypeName Target
    mapFacetName :
      FacetName Source → FacetName Target
    mapIndividualName :
      IndividualName Source → IndividualName Target
    mapIRIName :
      IRIName Source → IRIName Target
    mapBlankNodeName :
      BlankNodeName Source → BlankNodeName Target
    mapSimpleObjectPropertyName :
      SimpleObjectPropertyName Source → SimpleObjectPropertyName Target

open SignatureMorphism public

identitySignatureMorphism :
  (Sig : Signature) →
  SignatureMorphism Sig Sig
identitySignatureMorphism Sig =
  signatureMorphism
    (λ name → name)
    (λ name → name)
    (λ name → name)
    (λ name → name)
    (λ name → name)
    (λ name → name)
    (λ name → name)
    (λ name → name)
    (λ name → name)
    (λ name → name)

composeSignatureMorphism :
  ∀ {Source Middle Target} →
  SignatureMorphism Middle Target →
  SignatureMorphism Source Middle →
  SignatureMorphism Source Target
composeSignatureMorphism outer inner =
  signatureMorphism
    (λ name → mapClassName outer (mapClassName inner name))
    (λ name → mapObjectPropertyName outer (mapObjectPropertyName inner name))
    (λ name → mapDataPropertyName outer (mapDataPropertyName inner name))
    (λ name →
      mapAnnotationPropertyName outer (mapAnnotationPropertyName inner name))
    (λ name → mapDatatypeName outer (mapDatatypeName inner name))
    (λ name → mapFacetName outer (mapFacetName inner name))
    (λ name → mapIndividualName outer (mapIndividualName inner name))
    (λ name → mapIRIName outer (mapIRIName inner name))
    (λ name → mapBlankNodeName outer (mapBlankNodeName inner name))
    (λ name →
      mapSimpleObjectPropertyName outer
        (mapSimpleObjectPropertyName inner name))

renameList :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → B) →
  List A →
  List B
renameList f [] =
  []
renameList f (x ∷ xs) =
  f x ∷ renameList f xs

renameOptional :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → B) →
  Optional A →
  Optional B
renameOptional f absent =
  absent
renameOptional f (present x) =
  present (f x)

renameNonEmpty :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → B) →
  NonEmpty A →
  NonEmpty B
renameNonEmpty f (nonEmpty head tail) =
  nonEmpty (f head) (renameList f tail)

renameAtLeastTwo :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → B) →
  AtLeastTwo A →
  AtLeastTwo B
renameAtLeastTwo f (atLeastTwo first second rest) =
  atLeastTwo (f first) (f second) (renameList f rest)

renameDatatypeSupported :
  ∀ {Source Target}
    (morphism : SignatureMorphism Source Target)
    {datatype : DatatypeName Source} →
  DatatypeSupported Source datatype →
  DatatypeSupported Target (mapDatatypeName morphism datatype)
renameDatatypeSupported morphism support =
  datatypeSupported
    (mapDatatypeName morphism (supportedDatatypeName support))
    (cong (mapDatatypeName morphism) (supportedDatatypeMatches support))

renameLiteralSupported :
  ∀ {Source Target}
    (morphism : SignatureMorphism Source Target)
    {datatype : DatatypeName Source} →
  LiteralSupported Source datatype →
  LiteralSupported Target (mapDatatypeName morphism datatype)
renameLiteralSupported morphism support =
  literalSupported
    (mapDatatypeName morphism (supportedLiteralDatatypeName support))
    (cong (mapDatatypeName morphism) (supportedLiteralDatatypeMatches support))

renameEntity :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  Entity Source →
  Entity Target
renameEntity morphism (classEntity name) =
  classEntity (mapClassName morphism name)
renameEntity morphism (objectPropertyEntity name) =
  objectPropertyEntity (mapObjectPropertyName morphism name)
renameEntity morphism (dataPropertyEntity name) =
  dataPropertyEntity (mapDataPropertyName morphism name)
renameEntity morphism (annotationPropertyEntity name) =
  annotationPropertyEntity (mapAnnotationPropertyName morphism name)
renameEntity morphism (datatypeEntity name) =
  datatypeEntity (mapDatatypeName morphism name)
renameEntity morphism (individualEntity name) =
  individualEntity (mapIndividualName morphism name)

renameLiteral :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  Literal Source →
  Literal Target
renameLiteral morphism (typedLiteral lexical dtype support) =
  typedLiteral
    lexical
    (mapDatatypeName morphism dtype)
    (renameLiteralSupported morphism support)

renameFacetRestriction :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  FacetRestriction Source →
  FacetRestriction Target
renameFacetRestriction morphism restriction =
  facetRestriction
    (mapFacetName morphism (facet restriction))
    (renameLiteral morphism (value restriction))

mutual
  renameDataRange :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    DataRange Source →
    DataRange Target
  renameDataRange morphism (datatype name support) =
    datatype
      (mapDatatypeName morphism name)
      (renameDatatypeSupported morphism support)
  renameDataRange morphism dataTop =
    dataTop
  renameDataRange morphism dataBottom =
    dataBottom
  renameDataRange morphism (dataComplementOf range) =
    dataComplementOf (renameDataRange morphism range)
  renameDataRange morphism (dataIntersectionOf ranges) =
    dataIntersectionOf (renameNonEmptyDataRanges morphism ranges)
  renameDataRange morphism (dataUnionOf ranges) =
    dataUnionOf (renameNonEmptyDataRanges morphism ranges)
  renameDataRange morphism (dataOneOf literals) =
    dataOneOf (renameNonEmpty (renameLiteral morphism) literals)
  renameDataRange morphism (datatypeRestriction name support restrictions) =
    datatypeRestriction
      (mapDatatypeName morphism name)
      (renameDatatypeSupported morphism support)
      (renameList (renameFacetRestriction morphism) restrictions)

  renameOptionalDataRange :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    Optional (DataRange Source) →
    Optional (DataRange Target)
  renameOptionalDataRange morphism absent =
    absent
  renameOptionalDataRange morphism (present range) =
    present (renameDataRange morphism range)

  renameDataRanges :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    List (DataRange Source) →
    List (DataRange Target)
  renameDataRanges morphism [] =
    []
  renameDataRanges morphism (range ∷ ranges) =
    renameDataRange morphism range ∷ renameDataRanges morphism ranges

  renameNonEmptyDataRanges :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    NonEmpty (DataRange Source) →
    NonEmpty (DataRange Target)
  renameNonEmptyDataRanges morphism (nonEmpty head tail) =
    nonEmpty (renameDataRange morphism head) (renameDataRanges morphism tail)

renameObjectPropertyExpression :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  ObjectPropertyExpression Source →
  ObjectPropertyExpression Target
renameObjectPropertyExpression morphism (objectProperty name) =
  objectProperty (mapObjectPropertyName morphism name)
renameObjectPropertyExpression morphism topObjectProperty =
  topObjectProperty
renameObjectPropertyExpression morphism bottomObjectProperty =
  bottomObjectProperty
renameObjectPropertyExpression morphism (objectInverseOf property) =
  objectInverseOf (renameObjectPropertyExpression morphism property)

renameDataPropertyExpression :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  DataPropertyExpression Source →
  DataPropertyExpression Target
renameDataPropertyExpression morphism (dataProperty name) =
  dataProperty (mapDataPropertyName morphism name)
renameDataPropertyExpression morphism topDataProperty =
  topDataProperty
renameDataPropertyExpression morphism bottomDataProperty =
  bottomDataProperty

renameObjectPropertyChain :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  ObjectPropertyChain Source →
  ObjectPropertyChain Target
renameObjectPropertyChain morphism chain =
  objectPropertyChain
    (renameAtLeastTwo (renameObjectPropertyExpression morphism) (links chain))

renameSubObjectPropertyExpression :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  SubObjectPropertyExpression Source →
  SubObjectPropertyExpression Target
renameSubObjectPropertyExpression morphism (subObjectProperty property) =
  subObjectProperty (renameObjectPropertyExpression morphism property)
renameSubObjectPropertyExpression morphism (subObjectPropertyChain chain) =
  subObjectPropertyChain (renameObjectPropertyChain morphism chain)

renameIndividual :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  Individual Source →
  Individual Target
renameIndividual morphism (namedIndividual name) =
  namedIndividual (mapIndividualName morphism name)

mutual
  renameClassExpression :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    ClassExpression Source →
    ClassExpression Target
  renameClassExpression morphism (namedClass name) =
    namedClass (mapClassName morphism name)
  renameClassExpression morphism owlThing =
    owlThing
  renameClassExpression morphism owlNothing =
    owlNothing
  renameClassExpression morphism (objectIntersectionOf classes) =
    objectIntersectionOf (renameNonEmptyClassExpressions morphism classes)
  renameClassExpression morphism (objectUnionOf classes) =
    objectUnionOf (renameNonEmptyClassExpressions morphism classes)
  renameClassExpression morphism (objectComplementOf class) =
    objectComplementOf (renameClassExpression morphism class)
  renameClassExpression morphism (objectOneOf individuals) =
    objectOneOf (renameNonEmpty (renameIndividual morphism) individuals)
  renameClassExpression morphism (objectSomeValuesFrom property class) =
    objectSomeValuesFrom
      (renameObjectPropertyExpression morphism property)
      (renameClassExpression morphism class)
  renameClassExpression morphism (objectAllValuesFrom property class) =
    objectAllValuesFrom
      (renameObjectPropertyExpression morphism property)
      (renameClassExpression morphism class)
  renameClassExpression morphism (objectHasValue property individual) =
    objectHasValue
      (renameObjectPropertyExpression morphism property)
      (renameIndividual morphism individual)
  renameClassExpression morphism (objectHasSelf property) =
    objectHasSelf (mapSimpleObjectPropertyName morphism property)
  renameClassExpression morphism (objectMinCardinality n property class) =
    objectMinCardinality
      n
      (mapSimpleObjectPropertyName morphism property)
      (renameOptionalClassExpression morphism class)
  renameClassExpression morphism (objectMaxCardinality n property class) =
    objectMaxCardinality
      n
      (mapSimpleObjectPropertyName morphism property)
      (renameOptionalClassExpression morphism class)
  renameClassExpression morphism (objectExactCardinality n property class) =
    objectExactCardinality
      n
      (mapSimpleObjectPropertyName morphism property)
      (renameOptionalClassExpression morphism class)
  renameClassExpression morphism (dataSomeValuesFrom property range) =
    dataSomeValuesFrom
      (renameDataPropertyExpression morphism property)
      (renameDataRange morphism range)
  renameClassExpression morphism (dataAllValuesFrom property range) =
    dataAllValuesFrom
      (renameDataPropertyExpression morphism property)
      (renameDataRange morphism range)
  renameClassExpression morphism (dataHasValue property literal) =
    dataHasValue
      (renameDataPropertyExpression morphism property)
      (renameLiteral morphism literal)
  renameClassExpression morphism (dataMinCardinality n property range) =
    dataMinCardinality
      n
      (renameDataPropertyExpression morphism property)
      (renameOptionalDataRange morphism range)
  renameClassExpression morphism (dataMaxCardinality n property range) =
    dataMaxCardinality
      n
      (renameDataPropertyExpression morphism property)
      (renameOptionalDataRange morphism range)
  renameClassExpression morphism (dataExactCardinality n property range) =
    dataExactCardinality
      n
      (renameDataPropertyExpression morphism property)
      (renameOptionalDataRange morphism range)

  renameOptionalClassExpression :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    Optional (ClassExpression Source) →
    Optional (ClassExpression Target)
  renameOptionalClassExpression morphism absent =
    absent
  renameOptionalClassExpression morphism (present class) =
    present (renameClassExpression morphism class)

  renameClassExpressions :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    List (ClassExpression Source) →
    List (ClassExpression Target)
  renameClassExpressions morphism [] =
    []
  renameClassExpressions morphism (class ∷ classes) =
    renameClassExpression morphism class ∷
    renameClassExpressions morphism classes

  renameNonEmptyClassExpressions :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    NonEmpty (ClassExpression Source) →
    NonEmpty (ClassExpression Target)
  renameNonEmptyClassExpressions morphism (nonEmpty head tail) =
    nonEmpty
      (renameClassExpression morphism head)
      (renameClassExpressions morphism tail)

renamePropertyKey :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  PropertyKey Source →
  PropertyKey Target
renamePropertyKey morphism key =
  propertyKey
    (renameList
      (mapSimpleObjectPropertyName morphism)
      (objectProperties key))
    (renameList
      (renameDataPropertyExpression morphism)
      (dataProperties key))

renameAnnotationSubject :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  AnnotationSubject Source →
  AnnotationSubject Target
renameAnnotationSubject morphism (annotationSubjectIRI iri) =
  annotationSubjectIRI (mapIRIName morphism iri)
renameAnnotationSubject morphism (annotationSubjectAnonymous name) =
  annotationSubjectAnonymous (mapBlankNodeName morphism name)

renameAnnotationValue :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  AnnotationValue Source →
  AnnotationValue Target
renameAnnotationValue morphism (annotationValueIRI iri) =
  annotationValueIRI (mapIRIName morphism iri)
renameAnnotationValue morphism (annotationValueAnonymous name) =
  annotationValueAnonymous (mapBlankNodeName morphism name)
renameAnnotationValue morphism (annotationValueLiteral literal) =
  annotationValueLiteral (renameLiteral morphism literal)

mutual
  renameAnnotation :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    Annotation Source →
    Annotation Target
  renameAnnotation morphism (annotation annotations property value) =
    annotation
      (renameAnnotations morphism annotations)
      (mapAnnotationPropertyName morphism property)
      (renameAnnotationValue morphism value)

  renameAnnotations :
    ∀ {Source Target} →
    SignatureMorphism Source Target →
    List (Annotation Source) →
    List (Annotation Target)
  renameAnnotations morphism [] =
    []
  renameAnnotations morphism (item ∷ annotations) =
    renameAnnotation morphism item ∷
    renameAnnotations morphism annotations

renameAnnotated :
  ∀ {Source Target A B} →
  SignatureMorphism Source Target →
  (A → B) →
  Annotated Source A →
  Annotated Target B
renameAnnotated morphism f item =
  annotated
    (renameAnnotations morphism (itemAnnotations item))
    (f (itemBody item))

renameAxiom :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  Axiom Source →
  Axiom Target
renameAxiom morphism (declaration entity) =
  declaration (renameEntity morphism entity)
renameAxiom morphism (subClassOf sub sup) =
  subClassOf
    (renameClassExpression morphism sub)
    (renameClassExpression morphism sup)
renameAxiom morphism (equivalentClasses classes) =
  equivalentClasses
    (renameAtLeastTwo (renameClassExpression morphism) classes)
renameAxiom morphism (disjointClasses classes) =
  disjointClasses
    (renameAtLeastTwo (renameClassExpression morphism) classes)
renameAxiom morphism (disjointUnion class classes) =
  disjointUnion
    (mapClassName morphism class)
    (renameAtLeastTwo (renameClassExpression morphism) classes)
renameAxiom morphism (subObjectPropertyOf sub sup) =
  subObjectPropertyOf
    (renameSubObjectPropertyExpression morphism sub)
    (renameObjectPropertyExpression morphism sup)
renameAxiom morphism (equivalentObjectProperties properties) =
  equivalentObjectProperties
    (renameAtLeastTwo (renameObjectPropertyExpression morphism) properties)
renameAxiom morphism (disjointObjectProperties properties) =
  disjointObjectProperties
    (renameAtLeastTwo (mapSimpleObjectPropertyName morphism) properties)
renameAxiom morphism (inverseObjectProperties left right) =
  inverseObjectProperties
    (renameObjectPropertyExpression morphism left)
    (renameObjectPropertyExpression morphism right)
renameAxiom morphism (objectPropertyDomain property class) =
  objectPropertyDomain
    (renameObjectPropertyExpression morphism property)
    (renameClassExpression morphism class)
renameAxiom morphism (objectPropertyRange property class) =
  objectPropertyRange
    (renameObjectPropertyExpression morphism property)
    (renameClassExpression morphism class)
renameAxiom morphism (functionalObjectProperty property) =
  functionalObjectProperty (mapSimpleObjectPropertyName morphism property)
renameAxiom morphism (inverseFunctionalObjectProperty property) =
  inverseFunctionalObjectProperty
    (mapSimpleObjectPropertyName morphism property)
renameAxiom morphism (reflexiveObjectProperty property) =
  reflexiveObjectProperty
    (renameObjectPropertyExpression morphism property)
renameAxiom morphism (irreflexiveObjectProperty property) =
  irreflexiveObjectProperty (mapSimpleObjectPropertyName morphism property)
renameAxiom morphism (symmetricObjectProperty property) =
  symmetricObjectProperty
    (renameObjectPropertyExpression morphism property)
renameAxiom morphism (asymmetricObjectProperty property) =
  asymmetricObjectProperty (mapSimpleObjectPropertyName morphism property)
renameAxiom morphism (transitiveObjectProperty property) =
  transitiveObjectProperty
    (renameObjectPropertyExpression morphism property)
renameAxiom morphism (subDataPropertyOf sub sup) =
  subDataPropertyOf
    (renameDataPropertyExpression morphism sub)
    (renameDataPropertyExpression morphism sup)
renameAxiom morphism (equivalentDataProperties properties) =
  equivalentDataProperties
    (renameAtLeastTwo (renameDataPropertyExpression morphism) properties)
renameAxiom morphism (disjointDataProperties properties) =
  disjointDataProperties
    (renameAtLeastTwo (renameDataPropertyExpression morphism) properties)
renameAxiom morphism (dataPropertyDomain property class) =
  dataPropertyDomain
    (renameDataPropertyExpression morphism property)
    (renameClassExpression morphism class)
renameAxiom morphism (dataPropertyRange property range) =
  dataPropertyRange
    (renameDataPropertyExpression morphism property)
    (renameDataRange morphism range)
renameAxiom morphism (functionalDataProperty property) =
  functionalDataProperty
    (renameDataPropertyExpression morphism property)
renameAxiom morphism (datatypeDefinition name support range) =
  datatypeDefinition
    (mapDatatypeName morphism name)
    (renameDatatypeSupported morphism support)
    (renameDataRange morphism range)
renameAxiom morphism (hasKey class key) =
  hasKey
    (renameClassExpression morphism class)
    (renamePropertyKey morphism key)
renameAxiom morphism (sameIndividual individuals) =
  sameIndividual
    (renameAtLeastTwo (renameIndividual morphism) individuals)
renameAxiom morphism (differentIndividuals individuals) =
  differentIndividuals
    (renameAtLeastTwo (renameIndividual morphism) individuals)
renameAxiom morphism (classAssertion class individual) =
  classAssertion
    (renameClassExpression morphism class)
    (renameIndividual morphism individual)
renameAxiom morphism (objectPropertyAssertion property subject object) =
  objectPropertyAssertion
    (renameObjectPropertyExpression morphism property)
    (renameIndividual morphism subject)
    (renameIndividual morphism object)
renameAxiom morphism (negativeObjectPropertyAssertion property subject object) =
  negativeObjectPropertyAssertion
    (renameObjectPropertyExpression morphism property)
    (renameIndividual morphism subject)
    (renameIndividual morphism object)
renameAxiom morphism (dataPropertyAssertion property subject literal) =
  dataPropertyAssertion
    (renameDataPropertyExpression morphism property)
    (renameIndividual morphism subject)
    (renameLiteral morphism literal)
renameAxiom morphism (negativeDataPropertyAssertion property subject literal) =
  negativeDataPropertyAssertion
    (renameDataPropertyExpression morphism property)
    (renameIndividual morphism subject)
    (renameLiteral morphism literal)
renameAxiom morphism (annotationAssertion property subject value) =
  annotationAssertion
    (mapAnnotationPropertyName morphism property)
    (renameAnnotationSubject morphism subject)
    (renameAnnotationValue morphism value)
renameAxiom morphism (subAnnotationPropertyOf sub sup) =
  subAnnotationPropertyOf
    (mapAnnotationPropertyName morphism sub)
    (mapAnnotationPropertyName morphism sup)
renameAxiom morphism (annotationPropertyDomain property iri) =
  annotationPropertyDomain
    (mapAnnotationPropertyName morphism property)
    (mapIRIName morphism iri)
renameAxiom morphism (annotationPropertyRange property iri) =
  annotationPropertyRange
    (mapAnnotationPropertyName morphism property)
    (mapIRIName morphism iri)

renameAxioms :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  List (Axiom Source) →
  List (Axiom Target)
renameAxioms morphism =
  renameList (renameAxiom morphism)

renameAnnotatedAxiom :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  Annotated Source (Axiom Source) →
  Annotated Target (Axiom Target)
renameAnnotatedAxiom morphism =
  renameAnnotated morphism (renameAxiom morphism)

renameAnnotatedAxioms :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  List (Annotated Source (Axiom Source)) →
  List (Annotated Target (Axiom Target))
renameAnnotatedAxioms morphism =
  renameList (renameAnnotatedAxiom morphism)

renameAnnotatedBodies :
  ∀ {Source Target}
    (morphism : SignatureMorphism Source Target)
    (items : List (Annotated Source (Axiom Source))) →
  annotatedBodies (renameAnnotatedAxioms morphism items) ≡
  renameAxioms morphism (annotatedBodies items)
renameAnnotatedBodies morphism [] =
  refl
renameAnnotatedBodies morphism (item ∷ items) =
  cong
    (λ rest → renameAxiom morphism (itemBody item) ∷ rest)
    (renameAnnotatedBodies morphism items)

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

renameAxiomsPropertyChainFree :
  ∀ {Source Target}
    (morphism : SignatureMorphism Source Target)
    (axioms : List (Axiom Source)) →
  AxiomsPropertyChainFree axioms →
  AxiomsPropertyChainFree (renameAxioms morphism axioms)
renameAxiomsPropertyChainFree morphism [] proof =
  tt
renameAxiomsPropertyChainFree morphism (axiom ∷ axioms) (head , tail) =
  renameAxiomPropertyChainFree morphism axiom head ,
  renameAxiomsPropertyChainFree morphism axioms tail

renameOntology :
  ∀ {Source Target} →
  SignatureMorphism Source Target →
  RegularityContext Target →
  Ontology Source →
  Ontology Target
renameOntology {Target = Target} morphism targetContext source =
  ontology
    (renameAnnotations morphism (ontologyAnnotations source))
    (renameAnnotatedAxioms morphism (annotatedAxioms source))
    renamedAxioms
    ( renameAnnotatedBodies morphism (annotatedAxioms source)
    ∙ cong (renameAxioms morphism) (annotationErasure source)
    )
    (completeOntologyDatatypeSupport renamedAxioms)
    (ontologyRegularity
      targetContext
      (renameAxiomsPropertyChainFree
        morphism
        (axioms source)
        (propertyChainsFree (regularity source))))
  where
  renamedAxioms : List (Axiom Target)
  renamedAxioms =
    renameAxioms morphism (axioms source)