Compose Two Ontologies via Functor

This page is the practical guide for writing a cross-domain functor in pr4xis — the mechanism that lets two ontologies compose with mathematical proof that the composition is sound.

When you need a functor

If you have an ontology that uses concepts from another ontology — explicitly or implicitly — you should write a functor between them. Examples from the existing workspace:

Pharmacology talks about molecular targets → PharmacologyToMolecular
Biology talks about bioelectric phenomena → BiologyToBioelectric
Concurrency talks about events → ConcurrencyToEvents
Chess talks about state machines → ChessToConcurrency, ChessToEvents

The functor makes the implicit dependency explicit, and proves at test time that the dependency preserves structure.

What a functor must do

A functor F: Source → Target is a Rust impl of pr4xis::category::Functor. It must:

Map every object in the source category to an object in the target category.
Map every morphism in the source category to a morphism in the target category, with matching source and target.
Preserve identities: F(id_x) = id_{F(x)}.
Preserve composition: F(g ∘ f) = F(g) ∘ F(f).

If the laws hold, the functor is a categorical theorem that the source domain’s structure faithfully embeds in the target. If they don’t hold, your encoding has a bug or the composition you proposed isn’t actually structural — either way, the failing test surfaces it before the functor ships.

The pattern

Skeleton for a functor between two existing ontologies:

use pr4xis::category::{Arrow, Functor};

use crate::domain_a::{ACategory, AConcept, ARelation};
use crate::domain_b::{BCategory, BConcept, BRelation};

pub struct AToB;

impl Functor for AToB {
    type Source = ACategory;
    type Target = BCategory;

    fn map_object(obj: &AConcept) -> BConcept {
        match obj {
            AConcept::Foo => BConcept::CorrespondingFoo,
            AConcept::Bar => BConcept::CorrespondingBar,
            // … one arm per source concept
        }
    }

    fn map_morphism(m: &ARelation) -> BRelation {
        BRelation {
            from: Self::map_object(&m.source()),
            to: Self::map_object(&m.target()),
            kind: /* map kinds analogously */ todo!(),
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use pr4xis::category::laws::assert_functor_laws;

    #[test]
    fn test_a_to_b_functor_laws() {
        // Panics with the failing law's name if any law breaks.
        assert_functor_laws::<AToB>();
    }
}

That’s it. assert_functor_laws iterates the functor laws as Axiom impls: for every source concept it maps the identity morphism and checks F(id_x) == id_{F(x)}, and for every composable morphism pair it checks F(g ∘ f) == F(g) ∘ F(f). Each law’s verify() returns a typed Verdict (a proof or a counterexample, never a bool); the assert_* helper pattern-matches it and panics on the first counterexample.

If the test passes, the functor is verified. If it fails, the panic names the specific law that broke (e.g. FunctorIdentityLaw), and you fix the map_object arm that’s wrong. When you’d rather inspect each result yourself instead of panicking, iterate pr4xis::category::laws::functor_law_axioms::<AToB>() and match each Verdict.

Three things to know

1. `map_object` must be total

Every variant of AConcept must have a corresponding case in the match. The Rust compiler enforces this — exhaustiveness checking is your friend. If the source ontology adds a new concept, the compiler tells you to add a new case to every functor that uses it. This is one of the safety guarantees of writing functors as Rust types instead of as runtime mappings.

2. `map_object` does not need to be injective

Two distinct source concepts can map to the same target concept. This is how the molecular-bioelectric functor collapses 27 molecular concepts onto 4 unique bioelectric concepts (the 85.2% collapse from Gap detection). The collapse is not a bug — it’s a measurement of how much information the target ontology cannot represent.

If you want to detect collapses, pair your forward functor with a reverse functor and check whether they form an adjunction. The round-trip G(F(x)) will collapse onto a different concept for every concept the source ontology distinguishes that the target cannot.

3. The functor is a theorem, not a translation

A functor is not just “convert objects from A to B”. It is the claim that the conversion preserves structure. If you can write map_object correctly but assert_functor_laws fails, you have not proven the functor — the conversion does not actually preserve composition or identity, which means the source domain’s structure is not faithfully present in the target. The failing test is telling you the proposed embedding doesn’t hold.

When that happens, two paths forward:

Find a different target. Maybe the source belongs in a different ontology, with different morphism structure.
Restrict the source. Maybe only a subset of the source’s morphisms map cleanly. Write the functor over the restricted source category; document what’s left out and why.

Either is fine. The wrong move is to fudge the map_object to make the test pass — that hides the structural mismatch instead of surfacing it.

When you also need an adjunction

If you have two functors F: A → B and G: B → A going in opposite directions, you may have an adjunction. Adjunctions enable gap detection — the round-trip G(F(x)) surfaces concepts that one side cannot represent.

To check whether your functor pair is an adjunction, implement the Adjunction trait:

use pr4xis::category::Adjunction;

pub struct ABAdjunction;

impl Adjunction for ABAdjunction {
    type Left = AToB;
    type Right = BToA;

    fn unit(obj: &AConcept) -> ARelation {
        // η_A: A → G(F(A))
        let round_trip = BToA::map_object(&AToB::map_object(obj));
        ARelation { from: *obj, to: round_trip, kind: /* … */ todo!() }
    }

    fn counit(obj: &BConcept) -> BRelation {
        // ε_B: F(G(B)) → B
        let round_trip = AToB::map_object(&BToA::map_object(obj));
        BRelation { from: round_trip, to: *obj, kind: /* … */ todo!() }
    }
}

Then run the gap-analysis pattern from crates/domains/src/formal/meta/gap_analysis.rs against your adjunction. The collapses the analysis surfaces are missing distinctions in your source ontology — fix them with ContextDef::resolve or by splitting the entity, and the gap closes.

Where to look in the codebase

crates/domains/src/natural/biomedical/adjunctions.rs — the three biomedical adjunctions, with unit and counit implementations and the full law-checking test suite
crates/domains/src/natural/biomedical/biochemistry/bioelectricity_functor.rs — a clean single-functor example, no adjunction
crates/pr4xis/src/category/laws.rs — the functor laws as Axiom impls (functor_law_axioms / assert_functor_laws)
crates/domains/src/formal/meta/gap_analysis.rs — the gap-analysis pattern that uses the adjunctions

Build an ontology from a paper — the upstream tutorial; if you are writing a functor, you have probably already authored both source and target ontologies
Write axioms — domain-specific axioms that go beyond the structural laws functors enforce
Concepts — the categorical machinery, with examples
Gap detection — the bioelectricity result, the canonical example of an adjunction surfacing a real ontological gap
Glossary — formal definition of a functor

Document date: 2026-04-14

Keyboard shortcuts

Praxis Documentation