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

module OWL2.Corpus.Accepted.Morphism where

open import OWL2.Prelude
open import OWL2.Kernel
import OWL2.Corpus.Accepted.Kernel as KernelCorpus

kernelIdentityMorphism :
  SignatureMorphism
    KernelCorpus.kernelSemanticsSignature
    KernelCorpus.kernelSemanticsSignature
kernelIdentityMorphism =
  identitySignatureMorphism KernelCorpus.kernelSemanticsSignature

kernelAxiomsIdentityRenamed :
  renameAxioms
    kernelIdentityMorphism
    KernelCorpus.kernelSemanticAxioms ≡
  KernelCorpus.kernelSemanticAxioms
kernelAxiomsIdentityRenamed =
  refl

kernelAxiomsChainFreeRenamed :
  AxiomsPropertyChainFree
    (renameAxioms
      kernelIdentityMorphism
      KernelCorpus.kernelSemanticAxioms)
kernelAxiomsChainFreeRenamed =
  renameAxiomsPropertyChainFree
    kernelIdentityMorphism
    KernelCorpus.kernelSemanticAxioms
    KernelCorpus.kernelSemanticAxiomsChainFree

kernelOntologyIdentityRenamedAxioms :
  axioms
    (renameOntology
      kernelIdentityMorphism
      trivialRegularityContext
      KernelCorpus.kernelSemanticOntology) ≡
  KernelCorpus.kernelSemanticAxioms
kernelOntologyIdentityRenamedAxioms =
  refl

morphismSourceSignature morphismTargetSignature morphismFinalSignature :
  Signature
morphismSourceSignature =
  signature          noPunning
morphismTargetSignature =
  signature          noPunning
morphismFinalSignature =
  signature          noPunning

morphismSourceClass : ClassName morphismSourceSignature
morphismSourceClass =
  className fzero

morphismTargetClass : ClassName morphismTargetSignature
morphismTargetClass =
  className (fsuc fzero)

morphismFinalClass : ClassName morphismFinalSignature
morphismFinalClass =
  className (fsuc (fsuc fzero))

morphismSourceObjectProperty : ObjectPropertyName morphismSourceSignature
morphismSourceObjectProperty =
  objectPropertyName fzero

morphismTargetObjectProperty : ObjectPropertyName morphismTargetSignature
morphismTargetObjectProperty =
  objectPropertyName (fsuc fzero)

morphismFinalObjectProperty : ObjectPropertyName morphismFinalSignature
morphismFinalObjectProperty =
  objectPropertyName (fsuc (fsuc fzero))

morphismSourceDataProperty : DataPropertyName morphismSourceSignature
morphismSourceDataProperty =
  dataPropertyName fzero

morphismTargetDataProperty : DataPropertyName morphismTargetSignature
morphismTargetDataProperty =
  dataPropertyName (fsuc fzero)

morphismFinalDataProperty : DataPropertyName morphismFinalSignature
morphismFinalDataProperty =
  dataPropertyName (fsuc (fsuc fzero))

morphismSourceAnnotationProperty :
  AnnotationPropertyName morphismSourceSignature
morphismSourceAnnotationProperty =
  annotationPropertyName fzero

morphismTargetAnnotationProperty :
  AnnotationPropertyName morphismTargetSignature
morphismTargetAnnotationProperty =
  annotationPropertyName (fsuc fzero)

morphismFinalAnnotationProperty :
  AnnotationPropertyName morphismFinalSignature
morphismFinalAnnotationProperty =
  annotationPropertyName (fsuc (fsuc fzero))

morphismSourceDatatype : DatatypeName morphismSourceSignature
morphismSourceDatatype =
  datatypeName fzero

morphismTargetDatatype : DatatypeName morphismTargetSignature
morphismTargetDatatype =
  datatypeName (fsuc fzero)

morphismFinalDatatype : DatatypeName morphismFinalSignature
morphismFinalDatatype =
  datatypeName (fsuc (fsuc fzero))

morphismSourceFacet : FacetName morphismSourceSignature
morphismSourceFacet =
  facetName fzero

morphismTargetFacet : FacetName morphismTargetSignature
morphismTargetFacet =
  facetName (fsuc fzero)

morphismFinalFacet : FacetName morphismFinalSignature
morphismFinalFacet =
  facetName (fsuc (fsuc fzero))

morphismSourceIndividual : IndividualName morphismSourceSignature
morphismSourceIndividual =
  individualName fzero

morphismTargetIndividual : IndividualName morphismTargetSignature
morphismTargetIndividual =
  individualName (fsuc fzero)

morphismFinalIndividual : IndividualName morphismFinalSignature
morphismFinalIndividual =
  individualName (fsuc (fsuc fzero))

morphismSourceIRI : IRIName morphismSourceSignature
morphismSourceIRI =
  iriName fzero

morphismTargetIRI : IRIName morphismTargetSignature
morphismTargetIRI =
  iriName (fsuc fzero)

morphismFinalIRI : IRIName morphismFinalSignature
morphismFinalIRI =
  iriName (fsuc (fsuc fzero))

morphismSourceBlankNode : BlankNodeName morphismSourceSignature
morphismSourceBlankNode =
  blankNodeName fzero

morphismTargetBlankNode : BlankNodeName morphismTargetSignature
morphismTargetBlankNode =
  blankNodeName (fsuc fzero)

morphismFinalBlankNode : BlankNodeName morphismFinalSignature
morphismFinalBlankNode =
  blankNodeName (fsuc (fsuc fzero))

morphismSourceSimpleObjectProperty :
  SimpleObjectPropertyName morphismSourceSignature
morphismSourceSimpleObjectProperty =
  simpleObjectPropertyName
    morphismSourceObjectProperty
    (trivialSimpleObjectProperty morphismSourceObjectProperty)

morphismTargetSimpleObjectProperty :
  SimpleObjectPropertyName morphismTargetSignature
morphismTargetSimpleObjectProperty =
  simpleObjectPropertyName
    morphismTargetObjectProperty
    (trivialSimpleObjectProperty morphismTargetObjectProperty)

morphismFinalSimpleObjectProperty :
  SimpleObjectPropertyName morphismFinalSignature
morphismFinalSimpleObjectProperty =
  simpleObjectPropertyName
    morphismFinalObjectProperty
    (trivialSimpleObjectProperty morphismFinalObjectProperty)

nontrivialKernelMorphism :
  SignatureMorphism morphismSourceSignature morphismTargetSignature
nontrivialKernelMorphism =
  signatureMorphism
    (λ name → morphismTargetClass)
    (λ name → morphismTargetObjectProperty)
    (λ name → morphismTargetDataProperty)
    (λ name → morphismTargetAnnotationProperty)
    (λ name → morphismTargetDatatype)
    (λ name → morphismTargetFacet)
    (λ name → morphismTargetIndividual)
    (λ name → morphismTargetIRI)
    (λ name → morphismTargetBlankNode)
    (λ name → morphismTargetSimpleObjectProperty)

targetToFinalKernelMorphism :
  SignatureMorphism morphismTargetSignature morphismFinalSignature
targetToFinalKernelMorphism =
  signatureMorphism
    (λ name → morphismFinalClass)
    (λ name → morphismFinalObjectProperty)
    (λ name → morphismFinalDataProperty)
    (λ name → morphismFinalAnnotationProperty)
    (λ name → morphismFinalDatatype)
    (λ name → morphismFinalFacet)
    (λ name → morphismFinalIndividual)
    (λ name → morphismFinalIRI)
    (λ name → morphismFinalBlankNode)
    (λ name → morphismFinalSimpleObjectProperty)

composedKernelMorphism :
  SignatureMorphism morphismSourceSignature morphismFinalSignature
composedKernelMorphism =
  composeSignatureMorphism
    targetToFinalKernelMorphism
    nontrivialKernelMorphism

nontrivialClassDeclarationRenamed :
  renameAxiom
    nontrivialKernelMorphism
    (declaration (classEntity morphismSourceClass)) ≡
  declaration (classEntity morphismTargetClass)
nontrivialClassDeclarationRenamed =
  refl

nontrivialSubClassRenamed :
  renameAxiom
    nontrivialKernelMorphism
    (subClassOf
      (namedClass morphismSourceClass)
      (objectSomeValuesFrom
        (objectProperty morphismSourceObjectProperty)
        (namedClass morphismSourceClass))) ≡
  subClassOf
    (namedClass morphismTargetClass)
    (objectSomeValuesFrom
      (objectProperty morphismTargetObjectProperty)
      (namedClass morphismTargetClass))
nontrivialSubClassRenamed =
  refl

nontrivialTypedLiteralRenamed :
  renameLiteral
    nontrivialKernelMorphism
    (typedLiteral
      "literal"
      morphismSourceDatatype
      (trivialLiteralSupported morphismSourceDatatype)) ≡
  typedLiteral
    "literal"
    morphismTargetDatatype
    (trivialLiteralSupported morphismTargetDatatype)
nontrivialTypedLiteralRenamed =
  refl

nontrivialSimpleObjectPropertyRenamed :
  renameClassExpression
    nontrivialKernelMorphism
    (objectHasSelf morphismSourceSimpleObjectProperty) ≡
  objectHasSelf morphismTargetSimpleObjectProperty
nontrivialSimpleObjectPropertyRenamed =
  refl

composedClassDeclarationRenamed :
  renameAxiom
    composedKernelMorphism
    (declaration (classEntity morphismSourceClass)) ≡
  declaration (classEntity morphismFinalClass)
composedClassDeclarationRenamed =
  refl

composedSimpleObjectPropertyRenamed :
  renameClassExpression
    composedKernelMorphism
    (objectHasSelf morphismSourceSimpleObjectProperty) ≡
  objectHasSelf morphismFinalSimpleObjectProperty
composedSimpleObjectPropertyRenamed =
  refl

nontrivialAnnotationAssertionRenamed :
  renameAxiom
    nontrivialKernelMorphism
    (annotationAssertion
      morphismSourceAnnotationProperty
      (annotationSubjectIRI morphismSourceIRI)
      (annotationValueAnonymous morphismSourceBlankNode)) ≡
  annotationAssertion
    morphismTargetAnnotationProperty
    (annotationSubjectIRI morphismTargetIRI)
    (annotationValueAnonymous morphismTargetBlankNode)
nontrivialAnnotationAssertionRenamed =
  refl