OWL2.Corpus.Accepted.RawImports

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

module OWL2.Corpus.Accepted.RawImports where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab
open import OWL2.Elab.ImportProject.Legacy
open import OWL2.Foundation.Fin
open import OWL2.Foundation.List
open import OWL2.Import.OBOGraph.Raw using (rawOntologyFromOBOGraph)
open import OWL2.Kernel.Semantics
open import OWL2.OBOGraph.Syntax using (Graph; graph; graphDocument; edge; emptyMeta)
open import OWL2.Raw
open import OWL2.Semantics.ImportProject
open import OWL2.Semantics.ImportProject.Legacy
import OWL2.Examples.OBOGraph.References as OBOGraphReferences
import OWL2.Check.Bundle as Bundle
import OWL2.Kernel as K

vocabularyOntologyIRI projectOntologyIRI : RawIRI
vocabularyOntologyIRI =
  rawIRI "http://example.test/imports/vocabulary"
projectOntologyIRI =
  rawIRI "http://example.test/imports/project"

vocabularyVersionIRI : RawIRI
vocabularyVersionIRI =
  rawIRI "http://example.test/imports/vocabulary/version/1"

transitiveLeafOntologyIRI transitiveMiddleOntologyIRI
  transitiveProjectOntologyIRI : RawIRI
transitiveLeafOntologyIRI =
  rawIRI "http://example.test/imports/transitive/leaf"
transitiveMiddleOntologyIRI =
  rawIRI "http://example.test/imports/transitive/middle"
transitiveProjectOntologyIRI =
  rawIRI "http://example.test/imports/transitive/project"

resourceClassIRI projectDatasetClassIRI : RawIRI
resourceClassIRI =
  rawIRI "http://example.test/imports#Resource"
projectDatasetClassIRI =
  rawIRI "http://example.test/imports#ProjectDataset"

transitiveLeafClassIRI transitiveMiddleClassIRI
  transitiveRootClassIRI : RawIRI
transitiveLeafClassIRI =
  rawIRI "http://example.test/imports/transitive#LeafResource"
transitiveMiddleClassIRI =
  rawIRI "http://example.test/imports/transitive#MiddleResource"
transitiveRootClassIRI =
  rawIRI "http://example.test/imports/transitive#RootDataset"

resourceDeclaration : RawAnnotated RawAxiom
resourceDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass resourceClassIRI))

projectDatasetDeclaration : RawAnnotated RawAxiom
projectDatasetDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass projectDatasetClassIRI))

projectDatasetSubClassResourceAxiom : RawAnnotated RawAxiom
projectDatasetSubClassResourceAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass projectDatasetClassIRI)
      (rawNamedClass resourceClassIRI))

transitiveLeafDeclaration transitiveMiddleDeclaration
  transitiveRootDeclaration : RawAnnotated RawAxiom
transitiveLeafDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass transitiveLeafClassIRI))
transitiveMiddleDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass transitiveMiddleClassIRI))
transitiveRootDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass transitiveRootClassIRI))

transitiveMiddleSubClassLeafAxiom : RawAnnotated RawAxiom
transitiveMiddleSubClassLeafAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass transitiveMiddleClassIRI)
      (rawNamedClass transitiveLeafClassIRI))

transitiveRootSubClassMiddleAxiom : RawAnnotated RawAxiom
transitiveRootSubClassMiddleAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass transitiveRootClassIRI)
      (rawNamedClass transitiveMiddleClassIRI))

vocabularyDocument projectDocument : RawOntology
vocabularyDocument =
  rawOntology
    anonymousSource
    (present vocabularyOntologyIRI)
    absent
    []
    []
    (resourceDeclaration ∷ [])
projectDocument =
  rawOntology
    anonymousSource
    (present projectOntologyIRI)
    absent
    (vocabularyOntologyIRI ∷ [])
    []
    (projectDatasetDeclaration ∷ [])

sharedProjectDocument : RawOntology
sharedProjectDocument =
  rawOntology
    anonymousSource
    (present projectOntologyIRI)
    absent
    (vocabularyOntologyIRI ∷ [])
    []
    ( projectDatasetDeclaration
    ∷ projectDatasetSubClassResourceAxiom
    ∷ [] )

versionedVocabularyDocument : RawOntology
versionedVocabularyDocument =
  rawOntology
    anonymousSource
    (present vocabularyOntologyIRI)
    (present vocabularyVersionIRI)
    []
    []
    (resourceDeclaration ∷ [])

transitiveLeafDocument transitiveMiddleDocument
  transitiveProjectDocument : RawOntology
transitiveLeafDocument =
  rawOntology
    anonymousSource
    (present transitiveLeafOntologyIRI)
    absent
    []
    []
    (transitiveLeafDeclaration ∷ [])
transitiveMiddleDocument =
  rawOntology
    anonymousSource
    (present transitiveMiddleOntologyIRI)
    absent
    (transitiveLeafOntologyIRI ∷ [])
    []
    ( transitiveMiddleDeclaration
    ∷ transitiveMiddleSubClassLeafAxiom
    ∷ [] )
transitiveProjectDocument =
  rawOntology
    anonymousSource
    (present transitiveProjectOntologyIRI)
    absent
    (transitiveMiddleOntologyIRI ∷ [])
    []
    ( transitiveRootDeclaration
    ∷ transitiveRootSubClassMiddleAxiom
    ∷ [] )

acceptedImportProject : RawImportProject
acceptedImportProject =
  rawImportProject projectDocument (vocabularyDocument ∷ [])

sharedImportProject : RawImportProject
sharedImportProject =
  rawImportProject sharedProjectDocument (vocabularyDocument ∷ [])

versionedImportProject : RawImportProject
versionedImportProject =
  rawImportProject projectDocument (versionedVocabularyDocument ∷ [])

transitiveImportProject : RawImportProject
transitiveImportProject =
  rawImportProject
    transitiveProjectDocument
    (transitiveMiddleDocument ∷ transitiveLeafDocument ∷ [])

acceptedImportProjectResult :
  ImportProjectElaborationResult strictPolicy
acceptedImportProjectResult =
  elaborateImportProjectStrict acceptedImportProject

acceptedImportProjectDiagnostics :
  diagnostics acceptedImportProjectResult ≡ noDiagnostics
acceptedImportProjectDiagnostics =
  refl

acceptedImportProjectClean : Clean acceptedImportProjectResult
acceptedImportProjectClean =
  tt

acceptedImportProjectEvidence :
  EvidenceAvailable acceptedImportProjectResult
acceptedImportProjectEvidence =
  cleanEvidence acceptedImportProjectResult acceptedImportProjectClean

acceptedImportProjectScoped :
  ProjectScopedImportProject strictPolicy acceptedImportProject
acceptedImportProjectScoped =
  evidenceFromClean
    acceptedImportProjectResult
    acceptedImportProjectClean

acceptedImportProjectScopedSound :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    acceptedImportProject
    acceptedImportProjectScoped
acceptedImportProjectScopedSound =
  soundFromClean
    acceptedImportProjectResult
    acceptedImportProjectClean

acceptedCheckedImportProjectResult :
  CheckedImportProjectElaborationResult strictPolicy
acceptedCheckedImportProjectResult =
  elaborateCheckedImportProjectStrict acceptedImportProject

acceptedCheckedImportProjectDiagnostics :
  diagnostics acceptedCheckedImportProjectResult ≡ noDiagnostics
acceptedCheckedImportProjectDiagnostics =
  refl

acceptedCheckedImportProjectClean :
  Clean acceptedCheckedImportProjectResult
acceptedCheckedImportProjectClean =
  tt

acceptedImportProjectChecked :
  CheckedImportProject strictPolicy acceptedImportProject
acceptedImportProjectChecked =
  evidenceFromClean
    acceptedCheckedImportProjectResult
    acceptedCheckedImportProjectClean

acceptedImportProjectSound :
  ElaboratesToCheckedImportProject
    strictPolicy
    acceptedImportProject
    acceptedImportProjectChecked
acceptedImportProjectSound =
  soundFromClean
    acceptedCheckedImportProjectResult
    acceptedCheckedImportProjectClean

acceptedImportProjectRootSourceImports :
  projectDocumentSourceImports
    (checkedRootDocument acceptedImportProjectChecked) ≡
  vocabularyOntologyIRI ∷ []
acceptedImportProjectRootSourceImports =
  refl

acceptedImportProjectRootHeaderErased :
  ontologyIRI (eraseRawOntologyHeader projectDocument) ≡ absent
acceptedImportProjectRootHeaderErased =
  refl

acceptedImportProjectRootImportsErased :
  imports (eraseRawOntologyHeader projectDocument) ≡ []
acceptedImportProjectRootImportsErased =
  projectDocumentNormalizedImportsClosed
    (checkedRootDocument acceptedImportProjectChecked)

acceptedImportProjectRootCheckedImportsClosed :
  requestedImports
    (sourceImportClosure
      (projectDocumentChecked
        (checkedRootDocument acceptedImportProjectChecked))) ≡
  []
acceptedImportProjectRootCheckedImportsClosed =
  refl

acceptedImportProjectRootClassCount :
  K.classCount
    (signature
      (projectDocumentChecked
        (checkedRootDocument acceptedImportProjectChecked))) ≡
  1
acceptedImportProjectRootClassCount =
  refl

acceptedImportProjectImportedCheckedCount :
  listCount
    (projectDocumentsChecked
      (checkedImportDocuments acceptedImportProjectChecked)) ≡
  1
acceptedImportProjectImportedCheckedCount =
  refl

acceptedImportProjectMissingImportsClean :
  CleanDiagnostics (projectMissingDiagnostics acceptedImportProject)
acceptedImportProjectMissingImportsClean =
  missingImportsClean acceptedImportProjectChecked

acceptedImportProjectDuplicateOntologyIDsClean :
  CleanDiagnostics (projectDuplicateDiagnostics acceptedImportProject)
acceptedImportProjectDuplicateOntologyIDsClean =
  duplicateOntologyIDsClean acceptedImportProjectChecked

acceptedImportProjectRootSound :
  ElaboratesToCheckedImport
    (eraseRawOntologyHeader projectDocument)
    (projectDocumentChecked
      (checkedRootDocument acceptedImportProjectChecked))
acceptedImportProjectRootSound =
  checkedRootSound acceptedImportProjectSound

acceptedImportProjectOntologyIDCount :
  listCount (projectOntologyIDs acceptedImportProject) ≡
  2
acceptedImportProjectOntologyIDCount =
  refl

acceptedImportProjectRootOntologyIDIRI :
  ontologyIDIRI (sourceOntologyID projectDocument) ≡
  present projectOntologyIRI
acceptedImportProjectRootOntologyIDIRI =
  refl

acceptedImportProjectRootOntologyIDVersionAbsent :
  ontologyIDVersionIRI (sourceOntologyID projectDocument) ≡
  absent
acceptedImportProjectRootOntologyIDVersionAbsent =
  refl

acceptedImportProjectVocabularyOntologyIDIRI :
  ontologyIDIRI (sourceOntologyID vocabularyDocument) ≡
  present vocabularyOntologyIRI
acceptedImportProjectVocabularyOntologyIDIRI =
  refl

acceptedVersionedVocabularyOntologyIDVersionIRI :
  ontologyIDVersionIRI (sourceOntologyID versionedVocabularyDocument) ≡
  present vocabularyVersionIRI
acceptedVersionedVocabularyOntologyIDVersionIRI =
  refl

acceptedImportProjectVocabularyImportIDFound :
  ontologyIDInDocuments
    (importOntologyID vocabularyOntologyIRI)
    (projectDocuments acceptedImportProject) ≡
  true
acceptedImportProjectVocabularyImportIDFound =
  refl

versionedImportProjectResult :
  CheckedImportProjectElaborationResult strictPolicy
versionedImportProjectResult =
  elaborateCheckedImportProjectStrict versionedImportProject

versionedImportProjectDiagnostics :
  diagnostics versionedImportProjectResult ≡ noDiagnostics
versionedImportProjectDiagnostics =
  refl

versionedImportProjectClean : Clean versionedImportProjectResult
versionedImportProjectClean =
  tt

versionedImportProjectEvidence :
  EvidenceAvailable versionedImportProjectResult
versionedImportProjectEvidence =
  cleanEvidence versionedImportProjectResult versionedImportProjectClean

versionedImportProjectChecked :
  CheckedImportProject strictPolicy versionedImportProject
versionedImportProjectChecked =
  evidenceFromClean
    versionedImportProjectResult
    versionedImportProjectClean

versionedImportProjectVocabularyImportIRIFound :
  ontologyIRIInDocuments
    vocabularyOntologyIRI
    (projectDocuments versionedImportProject) ≡
  true
versionedImportProjectVocabularyImportIRIFound =
  refl

versionedImportProjectUnversionedImportIDAbsent :
  ontologyIDInDocuments
    (importOntologyID vocabularyOntologyIRI)
    (projectDocuments versionedImportProject) ≡
  false
versionedImportProjectUnversionedImportIDAbsent =
  refl

versionedVocabularyDocumentNotDuplicateOfUnversioned :
  rawOntologyIDInList
    (sourceOntologyID versionedVocabularyDocument)
    (sourceOntologyID vocabularyDocument ∷ []) ≡
  false
versionedVocabularyDocumentNotDuplicateOfUnversioned =
  refl

transitiveImportProjectResult :
  ImportProjectElaborationResult strictPolicy
transitiveImportProjectResult =
  elaborateImportProjectStrict transitiveImportProject

transitiveImportProjectDiagnostics :
  diagnostics transitiveImportProjectResult ≡ noDiagnostics
transitiveImportProjectDiagnostics =
  refl

transitiveImportProjectMissingDiagnostics :
  projectMissingDiagnostics transitiveImportProject ≡ noDiagnostics
transitiveImportProjectMissingDiagnostics =
  refl

transitiveImportProjectDocuments :
  projectDocuments transitiveImportProject ≡
  transitiveProjectDocument ∷
  transitiveMiddleDocument ∷
  transitiveLeafDocument ∷
  []
transitiveImportProjectDocuments =
  refl

transitiveImportProjectMiddleImportFound :
  ontologyIDInDocuments
    (importOntologyID transitiveMiddleOntologyIRI)
    (projectDocuments transitiveImportProject) ≡
  true
transitiveImportProjectMiddleImportFound =
  refl

transitiveImportProjectLeafImportFound :
  ontologyIDInDocuments
    (importOntologyID transitiveLeafOntologyIRI)
    (projectDocuments transitiveImportProject) ≡
  true
transitiveImportProjectLeafImportFound =
  refl

transitiveImportProjectClean :
  Clean transitiveImportProjectResult
transitiveImportProjectClean =
  tt

transitiveImportProjectScoped :
  ProjectScopedImportProject strictPolicy transitiveImportProject
transitiveImportProjectScoped =
  evidenceFromClean
    transitiveImportProjectResult
    transitiveImportProjectClean

transitiveImportProjectSound :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    transitiveImportProject
    transitiveImportProjectScoped
transitiveImportProjectSound =
  soundFromClean
    transitiveImportProjectResult
    transitiveImportProjectClean

transitiveImportProjectImportOntologyCount :
  listCount
    (importProjectImportOntologies transitiveImportProjectScoped) ≡
  2
transitiveImportProjectImportOntologyCount =
  refl

transitiveImportProjectMergedAxiomCount :
  listCount
    (K.axioms
      (importProjectMergedOntology transitiveImportProjectScoped)) ≡
  5
transitiveImportProjectMergedAxiomCount =
  refl

transitiveImportProjectCheckedImport : CheckedImport
transitiveImportProjectCheckedImport =
  importProjectCheckedImport transitiveImportProjectScoped

transitiveImportProjectCheckedImportClassCount :
  K.classCount (signature transitiveImportProjectCheckedImport) ≡
  3
transitiveImportProjectCheckedImportClassCount =
  refl

transitiveImportProjectCheckedImportDeclarationIRIs :
  declarationClassIRIs
    (sourceDeclarationEvidence transitiveImportProjectCheckedImport) ≡
  transitiveRootClassIRI ∷
  transitiveMiddleClassIRI ∷
  transitiveLeafClassIRI ∷
  []
transitiveImportProjectCheckedImportDeclarationIRIs =
  refl

transitiveImportProjectCheckedImportImportsClosed :
  requestedImports
    (sourceImportClosure transitiveImportProjectCheckedImport) ≡
  []
transitiveImportProjectCheckedImportImportsClosed =
  refl

acceptedImportProjectRootSourceSymbolTableClasses :
  classIRIs (sourceSymbolTable projectDocument) ≡
  projectDatasetClassIRI ∷ []
acceptedImportProjectRootSourceSymbolTableClasses =
  refl

acceptedImportProjectImportedSourceSymbolTableClasses :
  classIRIs (sourceSymbolTable vocabularyDocument) ≡
  resourceClassIRI ∷ []
acceptedImportProjectImportedSourceSymbolTableClasses =
  refl

acceptedImportProjectRootSymbolTableClasses :
  classIRIs (projectRootSymbolTable acceptedImportProject) ≡
  projectDatasetClassIRI ∷ []
acceptedImportProjectRootSymbolTableClasses =
  refl

acceptedImportProjectImportsSymbolTableClasses :
  classIRIs (projectImportsSymbolTable acceptedImportProject) ≡
  resourceClassIRI ∷ []
acceptedImportProjectImportsSymbolTableClasses =
  refl

acceptedImportProjectSymbolTableClasses :
  classIRIs (projectSymbolTable acceptedImportProject) ≡
  projectDatasetClassIRI ∷ resourceClassIRI ∷ []
acceptedImportProjectSymbolTableClasses =
  refl

acceptedImportProjectSymbolTableClassCount :
  K.classCount
    (symbolTableSignature
      (projectSymbolTable acceptedImportProject)) ≡
  2
acceptedImportProjectSymbolTableClassCount =
  refl

acceptedImportProjectSymbolTables :
  ProjectSymbolTables acceptedImportProject
acceptedImportProjectSymbolTables =
  projectSymbolTablesOf acceptedImportProject

acceptedImportProjectSymbolTablesRootRecorded :
  rootTable acceptedImportProjectSymbolTables ≡
  projectRootSymbolTable acceptedImportProject
acceptedImportProjectSymbolTablesRootRecorded =
  rootTableRecorded acceptedImportProjectSymbolTables

acceptedImportProjectSymbolTablesImportsRecorded :
  importTables acceptedImportProjectSymbolTables ≡
  projectImportsSymbolTable acceptedImportProject
acceptedImportProjectSymbolTablesImportsRecorded =
  importTablesRecorded acceptedImportProjectSymbolTables

acceptedImportProjectSymbolTablesCombinedRecorded :
  combinedTable acceptedImportProjectSymbolTables ≡
  projectSymbolTable acceptedImportProject
acceptedImportProjectSymbolTablesCombinedRecorded =
  combinedTableRecorded acceptedImportProjectSymbolTables

acceptedImportProjectRootToProjectMorphism :
  K.SignatureMorphism
    (symbolTableSignature
      (projectRootSymbolTable acceptedImportProject))
    (symbolTableSignature
      (projectSymbolTable acceptedImportProject))
acceptedImportProjectRootToProjectMorphism =
  rootToProjectMorphism acceptedImportProjectSymbolTables

acceptedImportProjectImportsToProjectMorphism :
  K.SignatureMorphism
    (symbolTableSignature
      (projectImportsSymbolTable acceptedImportProject))
    (symbolTableSignature
      (projectSymbolTable acceptedImportProject))
acceptedImportProjectImportsToProjectMorphism =
  importsToProjectMorphism acceptedImportProjectSymbolTables

acceptedImportProjectRootClassMapsToProjectDataset :
  lookupByFin
    (classIRIs (projectSymbolTable acceptedImportProject))
    (K.symbol
      (K.mapClassName
        acceptedImportProjectRootToProjectMorphism
        (K.className fzero))) ≡
  projectDatasetClassIRI
acceptedImportProjectRootClassMapsToProjectDataset =
  refl

acceptedImportProjectImportedClassMapsToResource :
  lookupByFin
    (classIRIs (projectSymbolTable acceptedImportProject))
    (K.symbol
      (K.mapClassName
        acceptedImportProjectImportsToProjectMorphism
        (K.className fzero))) ≡
  resourceClassIRI
acceptedImportProjectImportedClassMapsToResource =
  refl

acceptedImportProjectImportDocumentMorphisms :
  ProjectImportDocumentMorphisms
    acceptedImportProject
    (projectImports acceptedImportProject)
acceptedImportProjectImportDocumentMorphisms =
  projectImportDocumentMorphismsOf acceptedImportProject

acceptedImportProjectVocabularyToProjectMorphism :
  K.SignatureMorphism
    (symbolTableSignature (sourceSymbolTable vocabularyDocument))
    (symbolTableSignature (projectSymbolTable acceptedImportProject))
acceptedImportProjectVocabularyToProjectMorphism =
  projectImportDocumentHeadMorphism
    acceptedImportProjectImportDocumentMorphisms

acceptedImportProjectImportDocumentTailEmpty :
  projectImportDocumentTailMorphisms
    acceptedImportProjectImportDocumentMorphisms ≡
  projectImportDocumentMorphisms[]
acceptedImportProjectImportDocumentTailEmpty =
  refl

acceptedImportProjectVocabularyClassMapsToResource :
  lookupByFin
    (classIRIs (projectSymbolTable acceptedImportProject))
    (K.symbol
      (K.mapClassName
        acceptedImportProjectVocabularyToProjectMorphism
        (K.className fzero))) ≡
  resourceClassIRI
acceptedImportProjectVocabularyClassMapsToResource =
  refl

acceptedImportProjectCheckedMorphisms :
  CheckedImportProjectMorphisms acceptedImportProjectChecked
acceptedImportProjectCheckedMorphisms =
  checkedImportProjectMorphismsOf acceptedImportProjectChecked

acceptedImportProjectCheckedRootToProjectMorphism :
  K.SignatureMorphism
    (signature
      (projectDocumentChecked
        (checkedRootDocument acceptedImportProjectChecked)))
    (symbolTableSignature (projectSymbolTable acceptedImportProject))
acceptedImportProjectCheckedRootToProjectMorphism =
  checkedRootToProjectMorphism acceptedImportProjectCheckedMorphisms

acceptedImportProjectCheckedImportsToProjectMorphisms :
  CheckedProjectDocumentMorphisms
    strictPolicy
    acceptedImportProject
    (projectImports acceptedImportProject)
    (checkedImportDocuments acceptedImportProjectChecked)
acceptedImportProjectCheckedImportsToProjectMorphisms =
  checkedImportsToProjectMorphisms acceptedImportProjectCheckedMorphisms

acceptedImportProjectCheckedImportDocumentTailEmpty :
  checkedProjectDocumentTailMorphisms
    acceptedImportProjectCheckedImportsToProjectMorphisms ≡
  checkedProjectDocumentMorphisms[]
acceptedImportProjectCheckedImportDocumentTailEmpty =
  refl

acceptedImportProjectProjectionContext :
  K.RegularityContext
    (symbolTableSignature (projectSymbolTable acceptedImportProject))
acceptedImportProjectProjectionContext =
  K.trivialRegularityContext

acceptedImportProjectProjection :
  CheckedImportProjectProjection
    acceptedImportProjectChecked
    acceptedImportProjectProjectionContext
acceptedImportProjectProjection =
  checkedImportProjectProjectionOf
    acceptedImportProjectChecked
    acceptedImportProjectProjectionContext

acceptedImportProjectProjectedRootAxiomCount :
  listCount
    (K.axioms
      (projectedRootOntology acceptedImportProjectProjection)) ≡
  1
acceptedImportProjectProjectedRootAxiomCount =
  refl

acceptedImportProjectProjectedImportOntologyCount :
  listCount
    (projectedImportOntologies acceptedImportProjectProjection) ≡
  1
acceptedImportProjectProjectedImportOntologyCount =
  refl

acceptedImportProjectProjectedOntologyCount :
  listCount (projectedOntologies acceptedImportProjectProjection) ≡
  2
acceptedImportProjectProjectedOntologyCount =
  refl

acceptedImportProjectMergedProjectedAxiomCount :
  listCount
    (K.axioms
      (mergedProjectedOntology acceptedImportProjectProjection)) ≡
  2
acceptedImportProjectMergedProjectedAxiomCount =
  refl

acceptedImportProjectMergedProjectedAnnotatedAxiomCount :
  listCount
    (K.annotatedAxioms
      (mergedProjectedOntology acceptedImportProjectProjection)) ≡
  2
acceptedImportProjectMergedProjectedAnnotatedAxiomCount =
  refl

acceptedImportProjectMergedProjectedAnnotationErasure :
  K.annotatedBodies
    (K.annotatedAxioms
      (mergedProjectedOntology acceptedImportProjectProjection)) ≡
  K.axioms (mergedProjectedOntology acceptedImportProjectProjection)
acceptedImportProjectMergedProjectedAnnotationErasure =
  K.annotationErasure (mergedProjectedOntology acceptedImportProjectProjection)

trivialImportProjectInterpretation :
  (Sig : K.Signature) → Interpretation Sig
trivialImportProjectInterpretation Sig .ObjectDomain =
  Unit
trivialImportProjectInterpretation Sig .DataDomain =
  Unit
trivialImportProjectInterpretation Sig .classDenotation name value =
  Unit
trivialImportProjectInterpretation Sig .objectPropertyDenotation name subject object =
  Unit
trivialImportProjectInterpretation Sig .dataPropertyDenotation name subject value =
  Unit
trivialImportProjectInterpretation Sig .individualDenotation name =
  tt
trivialImportProjectInterpretation Sig .literalDenotation literal =
  tt
trivialImportProjectInterpretation Sig .datatypeDenotation name value =
  Unit
trivialImportProjectInterpretation Sig .facetRestrictionDenotation restriction value =
  Unit

acceptedImportProjectProjectionInterpretation :
  ProjectedCheckedImportProjectInterpretation acceptedImportProjectChecked
acceptedImportProjectProjectionInterpretation =
  trivialImportProjectInterpretation
    (symbolTableSignature (projectSymbolTable acceptedImportProject))

acceptedImportProjectProjectedModel :
  ProjectedCheckedImportProjectModel
    {context = acceptedImportProjectProjectionContext}
    acceptedImportProjectChecked
acceptedImportProjectProjectedModel =
  projectedCheckedImportProjectModel
    acceptedImportProjectProjection
    acceptedImportProjectProjectionInterpretation
    (all∷ tt all[] , (all∷ tt all[] , tt))

acceptedImportProjectMergedProjectedModel :
  SatisfiesOntology
    acceptedImportProjectProjectionInterpretation
    (mergedProjectedOntology acceptedImportProjectProjection)
acceptedImportProjectMergedProjectedModel =
  all∷ tt (all∷ tt all[])

acceptedImportProjectProjectedModelToMerged :
  SatisfiesOntology
    acceptedImportProjectProjectionInterpretation
    (mergedProjectedOntology acceptedImportProjectProjection)
acceptedImportProjectProjectedModelToMerged =
  projectedCheckedModelToMergedOntology
    acceptedImportProjectProjection
    acceptedImportProjectProjectionInterpretation
    (projectedSatisfies acceptedImportProjectProjectedModel)

acceptedImportProjectMergedToProjectedModel :
  ModelOfProjectedCheckedImportProject
    acceptedImportProjectProjection
    acceptedImportProjectProjectionInterpretation
acceptedImportProjectMergedToProjectedModel =
  mergedOntologyToProjectedCheckedModel
    acceptedImportProjectProjection
    acceptedImportProjectProjectionInterpretation
    acceptedImportProjectMergedProjectedModel

trivialImportProjectDocumentInterpretations :
  ∀ {policy sources} →
  (documents : CheckedProjectDocuments policy sources) →
  ProjectDocumentInterpretations documents
trivialImportProjectDocumentInterpretations checkedProjectDocuments[] =
  lift tt
trivialImportProjectDocumentInterpretations
  (checkedProjectDocuments∷ document documents) =
  trivialImportProjectInterpretation
    (signature (projectDocumentChecked document))
  ,
  trivialImportProjectDocumentInterpretations documents

acceptedImportProjectInterpretations :
  CheckedImportProjectInterpretations acceptedImportProjectChecked
acceptedImportProjectInterpretations =
  trivialImportProjectInterpretation
    (signature
      (projectDocumentChecked
        (checkedRootDocument acceptedImportProjectChecked)))
  ,
  trivialImportProjectDocumentInterpretations
    (checkedImportDocuments acceptedImportProjectChecked)

acceptedImportProjectCompleteModel :
  CompleteCheckedImportProjectModel acceptedImportProjectChecked
acceptedImportProjectCompleteModel =
  completeCheckedImportProjectModel
    acceptedImportProjectInterpretations
    (all∷ tt all[] , (all∷ tt all[] , tt))

sharedImportProjectResult :
  ImportProjectElaborationResult strictPolicy
sharedImportProjectResult =
  elaborateImportProjectStrict sharedImportProject

sharedImportProjectDiagnostics :
  diagnostics sharedImportProjectResult ≡ noDiagnostics
sharedImportProjectDiagnostics =
  refl

sharedImportProjectRootScopedDiagnostics :
  projectDocumentScopedDiagnostics
    sharedImportProject
    sharedProjectDocument ≡
  noDiagnostics
sharedImportProjectRootScopedDiagnostics =
  refl

sharedImportProjectLegacyDiagnostics :
  diagnostics (elaborateCheckedImportProjectStrict sharedImportProject) ≡
  singleDiagnostic (undeclaredClassDiagnostic resourceClassIRI)
sharedImportProjectLegacyDiagnostics =
  refl

sharedImportProjectClean : Clean sharedImportProjectResult
sharedImportProjectClean =
  tt

sharedImportProjectEvidence :
  EvidenceAvailable sharedImportProjectResult
sharedImportProjectEvidence =
  cleanEvidence sharedImportProjectResult sharedImportProjectClean

sharedImportProjectScoped :
  ProjectScopedImportProject strictPolicy sharedImportProject
sharedImportProjectScoped =
  evidenceFromClean
    sharedImportProjectResult
    sharedImportProjectClean

sharedImportProjectSound :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    sharedImportProject
    sharedImportProjectScoped
sharedImportProjectSound =
  soundFromClean
    sharedImportProjectResult
    sharedImportProjectClean

sharedImportProjectScopedFromClean :
  ProjectScopedImportProject strictPolicy sharedImportProject
sharedImportProjectScopedFromClean =
  projectScopedFromClean
    sharedImportProjectResult
    sharedImportProjectClean

sharedImportProjectSoundFromClean :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    sharedImportProject
    sharedImportProjectScopedFromClean
sharedImportProjectSoundFromClean =
  projectScopedSoundFromClean
    sharedImportProjectResult
    sharedImportProjectClean

sharedImportProjectFromCleanMergedAxiomCount :
  listCount
    (K.axioms
      (importProjectMergedOntology sharedImportProjectScopedFromClean)) ≡
  3
sharedImportProjectFromCleanMergedAxiomCount =
  refl

sharedImportProjectRootAxiomCount :
  listCount
    (K.axioms
      (importProjectRootOntology sharedImportProjectScoped)) ≡
  2
sharedImportProjectRootAxiomCount =
  refl

sharedImportProjectImportOntologyCount :
  listCount
    (importProjectImportOntologies sharedImportProjectScoped) ≡
  1
sharedImportProjectImportOntologyCount =
  refl

sharedImportProjectMergedAxiomCount :
  listCount
    (K.axioms
      (importProjectMergedOntology sharedImportProjectScoped)) ≡
  3
sharedImportProjectMergedAxiomCount =
  refl

sharedImportProjectInterpretation :
  ImportProjectInterpretation sharedImportProjectScoped
sharedImportProjectInterpretation =
  trivialImportProjectInterpretation
    (symbolTableSignature (projectSymbolTable sharedImportProject))

sharedImportProjectModel :
  ImportProjectModel sharedImportProjectScoped
sharedImportProjectModel =
  importProjectModel
    sharedImportProjectInterpretation
    ( all∷ tt
      (all∷ (λ value member → tt) all[])
    ,
      (all∷ tt all[] , tt))

sharedImportProjectMergedModel :
  SatisfiesOntology
    sharedImportProjectInterpretation
    (importProjectMergedOntology sharedImportProjectScoped)
sharedImportProjectMergedModel =
  all∷ tt
  (all∷ (λ value member → tt)
  (all∷ tt all[]))

sharedImportProjectModelToMerged :
  SatisfiesOntology
    sharedImportProjectInterpretation
    (importProjectMergedOntology sharedImportProjectScoped)
sharedImportProjectModelToMerged =
  importProjectModelToMergedOntology
    sharedImportProjectScoped
    sharedImportProjectInterpretation
    (importProjectSatisfies sharedImportProjectModel)

sharedImportProjectMergedToModel :
  ModelOfImportProject
    sharedImportProjectScoped
    sharedImportProjectInterpretation
sharedImportProjectMergedToModel =
  mergedOntologyToImportProjectModel
    sharedImportProjectScoped
    sharedImportProjectInterpretation
    sharedImportProjectMergedModel

sharedImportProjectCheckedImport :
  CheckedImport
sharedImportProjectCheckedImport =
  importProjectCheckedImport sharedImportProjectScoped

sharedImportProjectCheckedImportAxiomCount :
  listCount
    (K.axioms (ontology sharedImportProjectCheckedImport)) ≡
  3
sharedImportProjectCheckedImportAxiomCount =
  refl

sharedImportProjectCheckedImportSignatureClassCount :
  K.classCount (signature sharedImportProjectCheckedImport) ≡
  2
sharedImportProjectCheckedImportSignatureClassCount =
  refl

sharedImportProjectCheckedImportImportsClosed :
  requestedImports
    (sourceImportClosure sharedImportProjectCheckedImport) ≡
  []
sharedImportProjectCheckedImportImportsClosed =
  refl

sharedImportProjectCheckedImportDeclarationIRIs :
  declarationClassIRIs
    (sourceDeclarationEvidence sharedImportProjectCheckedImport) ≡
  projectDatasetClassIRI ∷ resourceClassIRI ∷ []
sharedImportProjectCheckedImportDeclarationIRIs =
  refl

sharedImportProjectCheckedImportTraceHasNoRawSource :
  traceRawEvidence
    (declarationTrace
      (sourceDeclarationEvidence sharedImportProjectCheckedImport)) ≡
  absent
sharedImportProjectCheckedImportTraceHasNoRawSource =
  refl

sharedImportProjectCheckedImportDeclarationTraceTable :
  traceTable
    (declarationTrace
      (sourceDeclarationEvidence sharedImportProjectCheckedImport)) ≡
  projectSymbolTable sharedImportProject
sharedImportProjectCheckedImportDeclarationTraceTable =
  refl

sharedImportProjectCheckedImportPropertyRoleTraceTable :
  traceTable
    (propertyRoleTrace
      (sourcePropertyRoleEvidence sharedImportProjectCheckedImport)) ≡
  projectSymbolTable sharedImportProject
sharedImportProjectCheckedImportPropertyRoleTraceTable =
  refl

sharedImportProjectCheckedImportModel :
  ImportProjectCheckedImportModel sharedImportProjectScoped
sharedImportProjectCheckedImportModel =
  importProjectModelToCheckedImportModel
    sharedImportProjectScoped
    sharedImportProjectModel

sharedImportProjectCheckedImportModelToProject :
  ImportProjectModel sharedImportProjectScoped
sharedImportProjectCheckedImportModelToProject =
  checkedImportModelToImportProjectModel
    sharedImportProjectScoped
    sharedImportProjectCheckedImportModel

sharedRelatedToIRI : RawIRI
sharedRelatedToIRI =
  rawIRI "http://example.test/imports#relatedTo"

sharedRelatedToDeclaration : RawAnnotated RawAxiom
sharedRelatedToDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawObjectProperty sharedRelatedToIRI))

sharedRelatedToSomeResourceAxiom : RawAnnotated RawAxiom
sharedRelatedToSomeResourceAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass projectDatasetClassIRI)
      (rawObjectSomeValuesFrom
        (rawObjectProperty sharedRelatedToIRI)
        (rawNamedClass resourceClassIRI)))

sharedObjectPropertyProjectDocument : RawOntology
sharedObjectPropertyProjectDocument =
  rawOntology
    anonymousSource
    (present projectOntologyIRI)
    absent
    (vocabularyOntologyIRI ∷ [])
    []
    ( projectDatasetDeclaration
    ∷ sharedRelatedToSomeResourceAxiom
    ∷ [] )

sharedObjectPropertyVocabularyDocument : RawOntology
sharedObjectPropertyVocabularyDocument =
  rawOntology
    anonymousSource
    (present vocabularyOntologyIRI)
    absent
    []
    []
    ( resourceDeclaration
    ∷ sharedRelatedToDeclaration
    ∷ [] )

sharedObjectPropertyImportProject : RawImportProject
sharedObjectPropertyImportProject =
  rawImportProject
    sharedObjectPropertyProjectDocument
    (sharedObjectPropertyVocabularyDocument ∷ [])

sharedObjectPropertyImportProjectResult :
  ImportProjectElaborationResult strictPolicy
sharedObjectPropertyImportProjectResult =
  elaborateImportProjectStrict sharedObjectPropertyImportProject

sharedObjectPropertyImportProjectDiagnostics :
  diagnostics sharedObjectPropertyImportProjectResult ≡ noDiagnostics
sharedObjectPropertyImportProjectDiagnostics =
  refl

sharedObjectPropertyImportProjectRootScopedDiagnostics :
  projectDocumentScopedDiagnostics
    sharedObjectPropertyImportProject
    sharedObjectPropertyProjectDocument ≡
  noDiagnostics
sharedObjectPropertyImportProjectRootScopedDiagnostics =
  refl

sharedObjectPropertyImportProjectLegacyDiagnostics :
  diagnostics
    (elaborateCheckedImportProjectStrict
      sharedObjectPropertyImportProject) ≡
  singleDiagnostic (undeclaredObjectPropertyDiagnostic sharedRelatedToIRI) ++
  singleDiagnostic (undeclaredClassDiagnostic resourceClassIRI)
sharedObjectPropertyImportProjectLegacyDiagnostics =
  refl

sharedObjectPropertyImportProjectClean :
  Clean sharedObjectPropertyImportProjectResult
sharedObjectPropertyImportProjectClean =
  tt

sharedObjectPropertyImportProjectEvidence :
  EvidenceAvailable sharedObjectPropertyImportProjectResult
sharedObjectPropertyImportProjectEvidence =
  cleanEvidence
    sharedObjectPropertyImportProjectResult
    sharedObjectPropertyImportProjectClean

sharedObjectPropertyImportProjectScoped :
  ProjectScopedImportProject strictPolicy sharedObjectPropertyImportProject
sharedObjectPropertyImportProjectScoped =
  evidenceFromClean
    sharedObjectPropertyImportProjectResult
    sharedObjectPropertyImportProjectClean

sharedObjectPropertyImportProjectSound :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    sharedObjectPropertyImportProject
    sharedObjectPropertyImportProjectScoped
sharedObjectPropertyImportProjectSound =
  soundFromClean
    sharedObjectPropertyImportProjectResult
    sharedObjectPropertyImportProjectClean

sharedObjectPropertyImportProjectMergedAxiomCount :
  listCount
    (K.axioms
      (importProjectMergedOntology
        sharedObjectPropertyImportProjectScoped)) ≡
  4
sharedObjectPropertyImportProjectMergedAxiomCount =
  refl

sharedObjectPropertyCheckedImport : CheckedImport
sharedObjectPropertyCheckedImport =
  importProjectCheckedImport sharedObjectPropertyImportProjectScoped

sharedObjectPropertyCheckedImportClassCount :
  K.classCount (signature sharedObjectPropertyCheckedImport) ≡
  2
sharedObjectPropertyCheckedImportClassCount =
  refl

sharedObjectPropertyCheckedImportObjectPropertyCount :
  K.objectPropertyCount (signature sharedObjectPropertyCheckedImport) ≡
  1
sharedObjectPropertyCheckedImportObjectPropertyCount =
  refl

sharedObjectPropertyCheckedImportDeclarationObjectPropertyIRIs :
  declarationObjectPropertyIRIs
    (sourceDeclarationEvidence sharedObjectPropertyCheckedImport) ≡
  sharedRelatedToIRI ∷ []
sharedObjectPropertyCheckedImportDeclarationObjectPropertyIRIs =
  refl

sharedObjectPropertyCheckedImportRoleObjectPropertyIRIs :
  roleObjectPropertyIRIs
    (sourcePropertyRoleEvidence sharedObjectPropertyCheckedImport) ≡
  sharedRelatedToIRI ∷ []
sharedObjectPropertyCheckedImportRoleObjectPropertyIRIs =
  refl

sharedObjectPropertyCheckedImportImportsClosed :
  requestedImports
    (sourceImportClosure sharedObjectPropertyCheckedImport) ≡
  []
sharedObjectPropertyCheckedImportImportsClosed =
  refl

importedKeyCardinalityVocabularyOntologyIRI
  importedKeyCardinalityProjectOntologyIRI : RawIRI
importedKeyCardinalityVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/key-cardinality/vocabulary"
importedKeyCardinalityProjectOntologyIRI =
  rawIRI "http://example.test/imports/key-cardinality/project"

importedKeyCardinalityDatasetIRI importedKeyCardinalityResourceIRI
  importedKeyCardinalityRelatedToIRI : RawIRI
importedKeyCardinalityDatasetIRI =
  rawIRI "http://example.test/imports/key-cardinality#Dataset"
importedKeyCardinalityResourceIRI =
  rawIRI "http://example.test/imports/key-cardinality#Resource"
importedKeyCardinalityRelatedToIRI =
  rawIRI "http://example.test/imports/key-cardinality#relatedTo"

importedKeyCardinalityDatasetDeclaration
  importedKeyCardinalityResourceDeclaration
  importedKeyCardinalityRelatedToDeclaration : RawAnnotated RawAxiom
importedKeyCardinalityDatasetDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass importedKeyCardinalityDatasetIRI))
importedKeyCardinalityResourceDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass importedKeyCardinalityResourceIRI))
importedKeyCardinalityRelatedToDeclaration =
  rawAnnotated []
    (rawDeclaration
      (rawEntity rawObjectProperty importedKeyCardinalityRelatedToIRI))

importedKeyCardinalityMinAxiom : RawAnnotated RawAxiom
importedKeyCardinalityMinAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass importedKeyCardinalityDatasetIRI)
      (rawObjectMinCardinality
        1
        (rawObjectProperty importedKeyCardinalityRelatedToIRI)
        (present (rawNamedClass importedKeyCardinalityResourceIRI))))

importedKeyCardinalityHasKeyAxiom : RawAnnotated RawAxiom
importedKeyCardinalityHasKeyAxiom =
  rawAnnotated []
    (rawHasKey
      (rawNamedClass importedKeyCardinalityDatasetIRI)
      (rawObjectProperty importedKeyCardinalityRelatedToIRI ∷ [])
      [])

importedKeyCardinalityProjectDocument
  importedKeyCardinalityVocabularyDocument : RawOntology
importedKeyCardinalityProjectDocument =
  rawOntology
    anonymousSource
    (present importedKeyCardinalityProjectOntologyIRI)
    absent
    (importedKeyCardinalityVocabularyOntologyIRI ∷ [])
    []
    ( importedKeyCardinalityDatasetDeclaration
    ∷ importedKeyCardinalityMinAxiom
    ∷ importedKeyCardinalityHasKeyAxiom
    ∷ [] )
importedKeyCardinalityVocabularyDocument =
  rawOntology
    anonymousSource
    (present importedKeyCardinalityVocabularyOntologyIRI)
    absent
    []
    []
    ( importedKeyCardinalityResourceDeclaration
    ∷ importedKeyCardinalityRelatedToDeclaration
    ∷ [] )

importedKeyAndCardinalityProject : RawImportProject
importedKeyAndCardinalityProject =
  rawImportProject
    importedKeyCardinalityProjectDocument
    (importedKeyCardinalityVocabularyDocument ∷ [])

importedKeyAndCardinalityProjectResult :
  ImportProjectElaborationResult strictPolicy
importedKeyAndCardinalityProjectResult =
  elaborateImportProjectStrict importedKeyAndCardinalityProject

importedKeyAndCardinalityProjectDiagnostics :
  diagnostics importedKeyAndCardinalityProjectResult ≡ noDiagnostics
importedKeyAndCardinalityProjectDiagnostics =
  refl

importedKeyAndCardinalityProjectRootScopedDiagnostics :
  projectDocumentScopedDiagnostics
    importedKeyAndCardinalityProject
    importedKeyCardinalityProjectDocument ≡
  noDiagnostics
importedKeyAndCardinalityProjectRootScopedDiagnostics =
  refl

importedKeyAndCardinalityProjectLegacyDiagnostics :
  diagnostics
    (elaborateCheckedImportProjectStrict
      importedKeyAndCardinalityProject) ≡
  singleDiagnostic
    (undeclaredObjectPropertyDiagnostic importedKeyCardinalityRelatedToIRI) ++
  singleDiagnostic
    (undeclaredClassDiagnostic importedKeyCardinalityResourceIRI) ++
  singleDiagnostic
    (undeclaredObjectPropertyDiagnostic importedKeyCardinalityRelatedToIRI)
importedKeyAndCardinalityProjectLegacyDiagnostics =
  refl

importedKeyAndCardinalityProjectClean :
  Clean importedKeyAndCardinalityProjectResult
importedKeyAndCardinalityProjectClean =
  tt

importedKeyAndCardinalityProjectScoped :
  ProjectScopedImportProject strictPolicy importedKeyAndCardinalityProject
importedKeyAndCardinalityProjectScoped =
  evidenceFromClean
    importedKeyAndCardinalityProjectResult
    importedKeyAndCardinalityProjectClean

importedKeyAndCardinalityProjectSound :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    importedKeyAndCardinalityProject
    importedKeyAndCardinalityProjectScoped
importedKeyAndCardinalityProjectSound =
  soundFromClean
    importedKeyAndCardinalityProjectResult
    importedKeyAndCardinalityProjectClean

importedKeyAndCardinalityProjectMergedAxiomCount :
  listCount
    (K.axioms
      (importProjectMergedOntology
        importedKeyAndCardinalityProjectScoped)) ≡
  5
importedKeyAndCardinalityProjectMergedAxiomCount =
  refl

importedKeyAndCardinalityCheckedImport : CheckedImport
importedKeyAndCardinalityCheckedImport =
  importProjectCheckedImport importedKeyAndCardinalityProjectScoped

importedKeyAndCardinalityCheckedImportClassCount :
  K.classCount (signature importedKeyAndCardinalityCheckedImport) ≡
  2
importedKeyAndCardinalityCheckedImportClassCount =
  refl

importedKeyAndCardinalityCheckedImportObjectPropertyCount :
  K.objectPropertyCount
    (signature importedKeyAndCardinalityCheckedImport) ≡
  1
importedKeyAndCardinalityCheckedImportObjectPropertyCount =
  refl

importedKeyAndCardinalityCheckedImportRoleObjectPropertyIRIs :
  roleObjectPropertyIRIs
    (sourcePropertyRoleEvidence importedKeyAndCardinalityCheckedImport) ≡
  importedKeyCardinalityRelatedToIRI ∷ []
importedKeyAndCardinalityCheckedImportRoleObjectPropertyIRIs =
  refl

importedKeyAndCardinalityCheckedImportRegularityGenerated :
  CheckedEvidence
    importedKeyAndCardinalityCheckedImport
    Bundle.regularityEvidence
importedKeyAndCardinalityCheckedImportRegularityGenerated =
  Bundle.storedEvidenceOf
    (K.regularity (ontology importedKeyAndCardinalityCheckedImport))

importedKeyAndCardinalityCheckedImportImportsClosed :
  requestedImports
    (sourceImportClosure importedKeyAndCardinalityCheckedImport) ≡
  []
importedKeyAndCardinalityCheckedImportImportsClosed =
  refl

sharedDataVocabularyOntologyIRI sharedDataProjectOntologyIRI : RawIRI
sharedDataVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/data/vocabulary"
sharedDataProjectOntologyIRI =
  rawIRI "http://example.test/imports/data/project"

sharedTitleIRI sharedStringDatatypeIRI sharedDatasetOneIRI
  sharedDataDatasetClassIRI : RawIRI
sharedTitleIRI =
  rawIRI "http://example.test/imports/data#title"
sharedStringDatatypeIRI =
  rawIRI "http://www.w3.org/2001/XMLSchema#string"
sharedDatasetOneIRI =
  rawIRI "http://example.test/imports/data#dataset-1"
sharedDataDatasetClassIRI =
  rawIRI "http://example.test/imports/data#Dataset"

sharedTitleDeclaration sharedStringDatatypeDeclaration
  sharedDatasetOneDeclaration sharedDataDatasetDeclaration :
  RawAnnotated RawAxiom
sharedTitleDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawDataProperty sharedTitleIRI))
sharedStringDatatypeDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawDatatype sharedStringDatatypeIRI))
sharedDatasetOneDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawIndividual sharedDatasetOneIRI))
sharedDataDatasetDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass sharedDataDatasetClassIRI))

sharedTitleRangeAxiom : RawAnnotated RawAxiom
sharedTitleRangeAxiom =
  rawAnnotated []
    (rawDataPropertyRange
      (rawDataProperty sharedTitleIRI)
      (rawDatatype sharedStringDatatypeIRI))

sharedDatasetOneClassAssertion : RawAnnotated RawAxiom
sharedDatasetOneClassAssertion =
  rawAnnotated []
    (rawClassAssertion
      (rawNamedClass sharedDataDatasetClassIRI)
      (rawNamedIndividual sharedDatasetOneIRI))

sharedTitleLiteral : RawLiteral
sharedTitleLiteral =
  rawLiteral "Dataset one" (present sharedStringDatatypeIRI) absent

sharedDatasetTitleAssertion : RawAnnotated RawAxiom
sharedDatasetTitleAssertion =
  rawAnnotated []
    (rawDataPropertyAssertion
      (rawDataProperty sharedTitleIRI)
      (rawNamedIndividual sharedDatasetOneIRI)
      sharedTitleLiteral)

sharedDataProjectDocument sharedDataVocabularyDocument : RawOntology
sharedDataProjectDocument =
  rawOntology
    anonymousSource
    (present sharedDataProjectOntologyIRI)
    absent
    (sharedDataVocabularyOntologyIRI ∷ [])
    []
    ( sharedDataDatasetDeclaration
    ∷ sharedDatasetOneDeclaration
    ∷ sharedDatasetOneClassAssertion
    ∷ sharedDatasetTitleAssertion
    ∷ [] )
sharedDataVocabularyDocument =
  rawOntology
    anonymousSource
    (present sharedDataVocabularyOntologyIRI)
    absent
    []
    []
    ( sharedTitleDeclaration
    ∷ sharedStringDatatypeDeclaration
    ∷ sharedTitleRangeAxiom
    ∷ [] )

sharedDataPropertyDatatypeImportProject : RawImportProject
sharedDataPropertyDatatypeImportProject =
  rawImportProject
    sharedDataProjectDocument
    (sharedDataVocabularyDocument ∷ [])

sharedDataPropertyDatatypeImportProjectResult :
  ImportProjectElaborationResult strictPolicy
sharedDataPropertyDatatypeImportProjectResult =
  elaborateImportProjectStrict sharedDataPropertyDatatypeImportProject

sharedDataPropertyDatatypeImportProjectDiagnostics :
  diagnostics sharedDataPropertyDatatypeImportProjectResult ≡ noDiagnostics
sharedDataPropertyDatatypeImportProjectDiagnostics =
  refl

sharedDataPropertyDatatypeImportProjectRootScopedDiagnostics :
  projectDocumentScopedDiagnostics
    sharedDataPropertyDatatypeImportProject
    sharedDataProjectDocument ≡
  noDiagnostics
sharedDataPropertyDatatypeImportProjectRootScopedDiagnostics =
  refl

sharedDataPropertyDatatypeImportProjectLegacyDiagnostics :
  diagnostics
    (elaborateCheckedImportProjectStrict
      sharedDataPropertyDatatypeImportProject) ≡
  singleDiagnostic (undeclaredDataPropertyDiagnostic sharedTitleIRI) ++
  singleDiagnostic (undeclaredDatatypeDiagnostic sharedStringDatatypeIRI)
sharedDataPropertyDatatypeImportProjectLegacyDiagnostics =
  refl

sharedDataPropertyDatatypeImportProjectClean :
  Clean sharedDataPropertyDatatypeImportProjectResult
sharedDataPropertyDatatypeImportProjectClean =
  tt

sharedDataPropertyDatatypeImportProjectScoped :
  ProjectScopedImportProject
    strictPolicy
    sharedDataPropertyDatatypeImportProject
sharedDataPropertyDatatypeImportProjectScoped =
  evidenceFromClean
    sharedDataPropertyDatatypeImportProjectResult
    sharedDataPropertyDatatypeImportProjectClean

sharedDataPropertyDatatypeImportProjectSound :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    sharedDataPropertyDatatypeImportProject
    sharedDataPropertyDatatypeImportProjectScoped
sharedDataPropertyDatatypeImportProjectSound =
  soundFromClean
    sharedDataPropertyDatatypeImportProjectResult
    sharedDataPropertyDatatypeImportProjectClean

sharedDataPropertyDatatypeImportProjectImportOntologyCount :
  listCount
    (importProjectImportOntologies
      sharedDataPropertyDatatypeImportProjectScoped) ≡
  1
sharedDataPropertyDatatypeImportProjectImportOntologyCount =
  refl

sharedDataPropertyDatatypeImportProjectMergedAxiomCount :
  listCount
    (K.axioms
      (importProjectMergedOntology
        sharedDataPropertyDatatypeImportProjectScoped)) ≡
  7
sharedDataPropertyDatatypeImportProjectMergedAxiomCount =
  refl

sharedDataPropertyDatatypeCheckedImport : CheckedImport
sharedDataPropertyDatatypeCheckedImport =
  importProjectCheckedImport sharedDataPropertyDatatypeImportProjectScoped

sharedDataPropertyDatatypeCheckedImportClassCount :
  K.classCount (signature sharedDataPropertyDatatypeCheckedImport) ≡
  1
sharedDataPropertyDatatypeCheckedImportClassCount =
  refl

sharedDataPropertyDatatypeCheckedImportDataPropertyCount :
  K.dataPropertyCount (signature sharedDataPropertyDatatypeCheckedImport) ≡
  1
sharedDataPropertyDatatypeCheckedImportDataPropertyCount =
  refl

sharedDataPropertyDatatypeCheckedImportDatatypeCount :
  K.datatypeCount (signature sharedDataPropertyDatatypeCheckedImport) ≡
  1
sharedDataPropertyDatatypeCheckedImportDatatypeCount =
  refl

sharedDataPropertyDatatypeCheckedImportIndividualCount :
  K.individualCount (signature sharedDataPropertyDatatypeCheckedImport) ≡
  1
sharedDataPropertyDatatypeCheckedImportIndividualCount =
  refl

sharedDataPropertyDatatypeCheckedImportDeclarationDataPropertyIRIs :
  declarationDataPropertyIRIs
    (sourceDeclarationEvidence sharedDataPropertyDatatypeCheckedImport) ≡
  sharedTitleIRI ∷ []
sharedDataPropertyDatatypeCheckedImportDeclarationDataPropertyIRIs =
  refl

sharedDataPropertyDatatypeCheckedImportDeclarationDatatypeIRIs :
  declarationDatatypeIRIs
    (sourceDeclarationEvidence sharedDataPropertyDatatypeCheckedImport) ≡
  sharedStringDatatypeIRI ∷ []
sharedDataPropertyDatatypeCheckedImportDeclarationDatatypeIRIs =
  refl

sharedDataPropertyDatatypeCheckedImportRoleDataPropertyIRIs :
  roleDataPropertyIRIs
    (sourcePropertyRoleEvidence sharedDataPropertyDatatypeCheckedImport) ≡
  sharedTitleIRI ∷ []
sharedDataPropertyDatatypeCheckedImportRoleDataPropertyIRIs =
  refl

sharedDataPropertyDatatypeCheckedImportDatatypeSupportGenerated :
  K.datatypeSupport (ontology sharedDataPropertyDatatypeCheckedImport) ≡
  K.completeOntologyDatatypeSupport
    (K.axioms (ontology sharedDataPropertyDatatypeCheckedImport))
sharedDataPropertyDatatypeCheckedImportDatatypeSupportGenerated =
  refl

sharedDataPropertyDatatypeCheckedImportImportsClosed :
  requestedImports
    (sourceImportClosure sharedDataPropertyDatatypeCheckedImport) ≡
  []
sharedDataPropertyDatatypeCheckedImportImportsClosed =
  refl

obographVocabularyOntologyIRI obographProjectOntologyIRI : RawIRI
obographVocabularyOntologyIRI =
  rawIRI "http://example.test/imports/obograph/vocabulary"
obographProjectOntologyIRI =
  rawIRI "http://example.test/imports/obograph/project"

obographAIRI obographBIRI obographRIRI obographProjectDatasetIRI :
  RawIRI
obographAIRI =
  rawIRI "A"
obographBIRI =
  rawIRI "B"
obographRIRI =
  rawIRI "R"
obographProjectDatasetIRI =
  rawIRI "http://example.test/imports/obograph#ProjectDataset"

obographVocabularyGraph : Graph
obographVocabularyGraph =
  graph
    (present "http://example.test/imports/obograph/vocabulary")
    absent
    emptyMeta
    ( OBOGraphReferences.nodeClass "A"
    ∷ OBOGraphReferences.nodeClass "B"
    ∷ OBOGraphReferences.nodeObjectProperty "R"
    ∷ [] )
    (edge "A" "R" "B" emptyMeta ∷ [])
    []
    []
    []
    []
    []

obographVocabularyDocument : RawOntology
obographVocabularyDocument =
  rawOntologyFromOBOGraph
    (graphDocument (obographVocabularyGraph ∷ []))

obographProjectDatasetDeclaration : RawAnnotated RawAxiom
obographProjectDatasetDeclaration =
  rawAnnotated []
    (rawDeclaration (rawEntity rawClass obographProjectDatasetIRI))

obographProjectRestrictionAxiom : RawAnnotated RawAxiom
obographProjectRestrictionAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass obographProjectDatasetIRI)
      (rawObjectSomeValuesFrom
        (rawObjectProperty obographRIRI)
        (rawNamedClass obographBIRI)))

obographProjectDocument : RawOntology
obographProjectDocument =
  rawOntology
    anonymousSource
    (present obographProjectOntologyIRI)
    absent
    (obographVocabularyOntologyIRI ∷ [])
    []
    ( obographProjectDatasetDeclaration
    ∷ obographProjectRestrictionAxiom
    ∷ [] )

obographVocabularyImportProject : RawImportProject
obographVocabularyImportProject =
  rawImportProject
    obographProjectDocument
    (obographVocabularyDocument ∷ [])

obographVocabularyImportProjectResult :
  ImportProjectElaborationResult strictPolicy
obographVocabularyImportProjectResult =
  elaborateImportProjectStrict obographVocabularyImportProject

obographVocabularyImportProjectDiagnostics :
  diagnostics obographVocabularyImportProjectResult ≡ noDiagnostics
obographVocabularyImportProjectDiagnostics =
  refl

obographVocabularyImportProjectLegacyDiagnostics :
  diagnostics
    (elaborateCheckedImportProjectStrict obographVocabularyImportProject) ≡
  singleDiagnostic (undeclaredObjectPropertyDiagnostic obographRIRI) ++
  singleDiagnostic (undeclaredClassDiagnostic obographBIRI)
obographVocabularyImportProjectLegacyDiagnostics =
  refl

obographVocabularyDocumentOntologyIRI :
  ontologyIRI obographVocabularyDocument ≡
  present obographVocabularyOntologyIRI
obographVocabularyDocumentOntologyIRI =
  refl

obographVocabularyImportProjectClean :
  Clean obographVocabularyImportProjectResult
obographVocabularyImportProjectClean =
  tt

obographVocabularyImportProjectScoped :
  ProjectScopedImportProject strictPolicy obographVocabularyImportProject
obographVocabularyImportProjectScoped =
  evidenceFromClean
    obographVocabularyImportProjectResult
    obographVocabularyImportProjectClean

obographVocabularyImportProjectSound :
  ElaboratesToProjectScopedImportProject
    strictPolicy
    obographVocabularyImportProject
    obographVocabularyImportProjectScoped
obographVocabularyImportProjectSound =
  soundFromClean
    obographVocabularyImportProjectResult
    obographVocabularyImportProjectClean

obographVocabularyImportProjectRawImportAxiomCount :
  listCount (axioms obographVocabularyDocument) ≡
  4
obographVocabularyImportProjectRawImportAxiomCount =
  refl

obographVocabularyImportProjectMergedAxiomCount :
  listCount
    (K.axioms
      (importProjectMergedOntology obographVocabularyImportProjectScoped)) ≡
  6
obographVocabularyImportProjectMergedAxiomCount =
  refl

obographVocabularyCheckedImport : CheckedImport
obographVocabularyCheckedImport =
  importProjectCheckedImport obographVocabularyImportProjectScoped

obographVocabularyCheckedImportClassCount :
  K.classCount (signature obographVocabularyCheckedImport) ≡
  3
obographVocabularyCheckedImportClassCount =
  refl

obographVocabularyCheckedImportObjectPropertyCount :
  K.objectPropertyCount (signature obographVocabularyCheckedImport) ≡
  1
obographVocabularyCheckedImportObjectPropertyCount =
  refl

obographVocabularyCheckedImportDeclarationObjectPropertyIRIs :
  declarationObjectPropertyIRIs
    (sourceDeclarationEvidence obographVocabularyCheckedImport) ≡
  obographRIRI ∷ []
obographVocabularyCheckedImportDeclarationObjectPropertyIRIs =
  refl

obographVocabularyCheckedImportRoleObjectPropertyIRIs :
  roleObjectPropertyIRIs
    (sourcePropertyRoleEvidence obographVocabularyCheckedImport) ≡
  obographRIRI ∷ []
obographVocabularyCheckedImportRoleObjectPropertyIRIs =
  refl

obographVocabularyCheckedImportImportsClosed :
  requestedImports
    (sourceImportClosure obographVocabularyCheckedImport) ≡
  []
obographVocabularyCheckedImportImportsClosed =
  refl

resourceSubClassThingAxiom : RawAnnotated RawAxiom
resourceSubClassThingAxiom =
  rawAnnotated []
    (rawSubClassOf
      (rawNamedClass resourceClassIRI)
      rawOwlThing)

semanticVocabularyDocument : RawOntology
semanticVocabularyDocument =
  rawOntology
    anonymousSource
    (present vocabularyOntologyIRI)
    absent
    []
    []
    ( resourceDeclaration
    ∷ resourceSubClassThingAxiom
    ∷ [] )

semanticImportProject : RawImportProject
semanticImportProject =
  rawImportProject projectDocument (semanticVocabularyDocument ∷ [])

semanticImportProjectResult :
  CheckedImportProjectElaborationResult strictPolicy
semanticImportProjectResult =
  elaborateCheckedImportProjectStrict semanticImportProject

semanticImportProjectDiagnostics :
  diagnostics semanticImportProjectResult ≡ noDiagnostics
semanticImportProjectDiagnostics =
  refl

semanticImportProjectClean : Clean semanticImportProjectResult
semanticImportProjectClean =
  tt

semanticImportProjectChecked :
  CheckedImportProject strictPolicy semanticImportProject
semanticImportProjectChecked =
  evidenceFromClean
    semanticImportProjectResult
    semanticImportProjectClean

semanticImportProjectRootClassCount :
  K.classCount
    (signature
      (projectDocumentChecked
        (checkedRootDocument semanticImportProjectChecked))) ≡
  1
semanticImportProjectRootClassCount =
  refl

semanticImportProjectImportedCheckedCount :
  listCount
    (projectDocumentsChecked
      (checkedImportDocuments semanticImportProjectChecked)) ≡
  1
semanticImportProjectImportedCheckedCount =
  refl

semanticImportProjectSymbolTableClassCount :
  K.classCount
    (symbolTableSignature
      (projectSymbolTable semanticImportProject)) ≡
  2
semanticImportProjectSymbolTableClassCount =
  refl

semanticImportProjectProjectionContext :
  K.RegularityContext
    (symbolTableSignature (projectSymbolTable semanticImportProject))
semanticImportProjectProjectionContext =
  K.trivialRegularityContext

semanticImportProjectProjection :
  CheckedImportProjectProjection
    semanticImportProjectChecked
    semanticImportProjectProjectionContext
semanticImportProjectProjection =
  checkedImportProjectProjectionOf
    semanticImportProjectChecked
    semanticImportProjectProjectionContext

semanticImportProjectProjectedRootAxiomCount :
  listCount
    (K.axioms
      (projectedRootOntology semanticImportProjectProjection)) ≡
  1
semanticImportProjectProjectedRootAxiomCount =
  refl

semanticImportProjectProjectedImportOntologyCount :
  listCount
    (projectedImportOntologies semanticImportProjectProjection) ≡
  1
semanticImportProjectProjectedImportOntologyCount =
  refl

semanticImportProjectMergedProjectedAxiomCount :
  listCount
    (K.axioms
      (mergedProjectedOntology semanticImportProjectProjection)) ≡
  3
semanticImportProjectMergedProjectedAxiomCount =
  refl

semanticImportProjectProjectionInterpretation :
  ProjectedCheckedImportProjectInterpretation semanticImportProjectChecked
semanticImportProjectProjectionInterpretation =
  trivialImportProjectInterpretation
    (symbolTableSignature (projectSymbolTable semanticImportProject))

semanticImportProjectProjectedModel :
  ProjectedCheckedImportProjectModel
    {context = semanticImportProjectProjectionContext}
    semanticImportProjectChecked
semanticImportProjectProjectedModel =
  projectedCheckedImportProjectModel
    semanticImportProjectProjection
    semanticImportProjectProjectionInterpretation
    ( all∷ tt all[]
    ,
      ( all∷ tt
        (all∷ (λ value member → tt) all[])
      ,
        tt ))

semanticImportProjectMergedProjectedModel :
  SatisfiesOntology
    semanticImportProjectProjectionInterpretation
    (mergedProjectedOntology semanticImportProjectProjection)
semanticImportProjectMergedProjectedModel =
  all∷ tt
  (all∷ tt
  (all∷ (λ value member → tt) all[]))

semanticImportProjectProjectedModelToMerged :
  SatisfiesOntology
    semanticImportProjectProjectionInterpretation
    (mergedProjectedOntology semanticImportProjectProjection)
semanticImportProjectProjectedModelToMerged =
  projectedCheckedModelToMergedOntology
    semanticImportProjectProjection
    semanticImportProjectProjectionInterpretation
    (projectedSatisfies semanticImportProjectProjectedModel)

semanticImportProjectMergedToProjectedModel :
  ModelOfProjectedCheckedImportProject
    semanticImportProjectProjection
    semanticImportProjectProjectionInterpretation
semanticImportProjectMergedToProjectedModel =
  mergedOntologyToProjectedCheckedModel
    semanticImportProjectProjection
    semanticImportProjectProjectionInterpretation
    semanticImportProjectMergedProjectedModel