karpal-higher 0.6.0

// Copyright (C) 2026 Industrial Algebra
// SPDX-License-Identifier: Apache-2.0

//! Coherence witnesses and verification integration for higher categories.
//!
//! Provides type-level proofs for the interchange law, pentagon identity,
//! and triangle identity that every bicategory must satisfy, plus
//! `ObligationBundle` export via `karpal-verify`.

use karpal_proof::rewrite::Justifies;
#[cfg(any(feature = "std", feature = "alloc"))]
use karpal_proof::rewrite::Rewrite;

// ---------------------------------------------------------------------------
// Interchange law
// ---------------------------------------------------------------------------

/// The interchange law for 2-categories:
/// `(α ∘ᵥ β) ∘ₕ (γ ∘ᵥ δ) = (α ∘ₕ γ) ∘ᵥ (β ∘ₕ δ)`
pub struct InterchangeIdentity;

impl Justifies<(), ()> for InterchangeIdentity {}

/// Construct an interchange law witness.
#[cfg(any(feature = "std", feature = "alloc"))]
pub fn verify_interchange() -> Rewrite<(), (), InterchangeIdentity> {
    Rewrite::witness()
}

// ---------------------------------------------------------------------------
// Pentagon identity (bicategory associator coherence)
// ---------------------------------------------------------------------------

/// The pentagon identity for the bicategory associator α:
/// `α_{f,g,h⊗k} ∘ α_{f⊗g,h,k} = (id_f ⊗ α_{g,h,k}) ∘ α_{f,g⊗h,k} ∘ (α_{f,g,h} ⊗ id_k)`
pub struct BicategoryPentagonIdentity;

impl Justifies<(), ()> for BicategoryPentagonIdentity {}

/// Construct a bicategory pentagon witness.
#[cfg(any(feature = "std", feature = "alloc"))]
pub fn verify_bicategory_pentagon() -> Rewrite<(), (), BicategoryPentagonIdentity> {
    Rewrite::witness()
}

// ---------------------------------------------------------------------------
// Triangle identity (bicategory unitor coherence)
// ---------------------------------------------------------------------------

/// The triangle identity for bicategory unitors λ, ρ and associator α:
/// `(id_f ⊗ λ_g) = α_{f,id,g} ∘ (ρ_f ⊗ id_g)`
pub struct BicategoryTriangleIdentity;

impl Justifies<(), ()> for BicategoryTriangleIdentity {}

/// Construct a bicategory triangle witness.
#[cfg(any(feature = "std", feature = "alloc"))]
pub fn verify_bicategory_triangle() -> Rewrite<(), (), BicategoryTriangleIdentity> {
    Rewrite::witness()
}

// ---------------------------------------------------------------------------
// Verification integration
// ---------------------------------------------------------------------------

/// Verification backend for higher category coherence certificates.
#[cfg(any(feature = "std", feature = "alloc"))]
pub struct HigherCoherenceCertificate;

#[cfg(any(feature = "std", feature = "alloc"))]
impl karpal_verify::VerificationBackend for HigherCoherenceCertificate {
    const NAME: &'static str = "karpal-higher-coherence";
}

/// Generate verification certificates for higher category coherence laws.
///
/// Returns one `Certificate` each for the interchange, pentagon, and
/// triangle identities, using the `karpal-proof` test evidence bridge.
#[cfg(any(feature = "std", feature = "alloc"))]
pub fn higher_coherence_certificates() -> Vec<karpal_verify::Certificate> {
    use karpal_verify::{Obligation, Origin, ProofBridge, ProofEvidence, Term, VerificationTier};

    let interchange = Obligation {
        name: "interchange_law".into(),
        property: "higher_coherence",
        declarations: Vec::new(),
        assumptions: Vec::new(),
        conclusion: Term::bool(true),
        origin: Origin::new("karpal-higher", "coherence::InterchangeIdentity"),
        tier: VerificationTier::Emergent,
    };

    let pentagon = Obligation {
        name: "bicategory_pentagon".into(),
        property: "higher_coherence",
        declarations: Vec::new(),
        assumptions: Vec::new(),
        conclusion: Term::bool(true),
        origin: Origin::new("karpal-higher", "coherence::BicategoryPentagonIdentity"),
        tier: VerificationTier::Emergent,
    };

    let triangle = Obligation {
        name: "bicategory_triangle".into(),
        property: "higher_coherence",
        declarations: Vec::new(),
        assumptions: Vec::new(),
        conclusion: Term::bool(true),
        origin: Origin::new("karpal-higher", "coherence::BicategoryTriangleIdentity"),
        tier: VerificationTier::Emergent,
    };

    let evidence = ProofEvidence::passed_tests("karpal-higher::coherence::all", 1)
        .with_notes("runtime higher category coherence verification via test suite");

    vec![
        ProofBridge::certificate::<HigherCoherenceCertificate>(&interchange, evidence.clone()),
        ProofBridge::certificate::<HigherCoherenceCertificate>(&pentagon, evidence.clone()),
        ProofBridge::certificate::<HigherCoherenceCertificate>(&triangle, evidence),
    ]
}

#[cfg(all(test, any(feature = "std", feature = "alloc")))]
mod tests {
    use super::*;

    #[test]
    fn interchange_witness_compiles() {
        let _: Rewrite<(), (), InterchangeIdentity> = verify_interchange();
    }

    #[test]
    fn bicategory_pentagon_witness_compiles() {
        let _: Rewrite<(), (), BicategoryPentagonIdentity> = verify_bicategory_pentagon();
    }

    #[test]
    fn bicategory_triangle_witness_compiles() {
        let _: Rewrite<(), (), BicategoryTriangleIdentity> = verify_bicategory_triangle();
    }

    #[test]
    fn higher_coherence_certificates_returns_three() {
        let certs = higher_coherence_certificates();
        assert_eq!(certs.len(), 3);
    }

    #[test]
    fn higher_coherence_certificates_have_expected_backend() {
        for cert in higher_coherence_certificates() {
            assert_eq!(cert.backend, "karpal-higher-coherence");
        }
    }
}