metacat 0.2.1

metacat: a categorical theorem prover
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

//! # Lift functors into categories of definitions

use open_hypergraphs::lax::{
    OpenHypergraph,
    functor::{Functor, try_define_map_arrow},
};

pub use super::types::*;

/// Given an identity-on-objects functor F : C → D,
/// lift it to one Def(C) → Def(D).
#[derive(Clone, PartialEq)]
pub struct Lift<F> {
    functor: F,
}

impl<F: Functor<O, A1, O, A2> + Clone, K: Clone, O: Clone + PartialEq, A1: Clone, A2: Clone>
    Functor<O, Def<K, A1>, O, Def<K, A2>> for Lift<F>
{
    fn map_object(&self, o: &O) -> impl ExactSizeIterator<Item = O> {
        std::iter::once(o.clone())
    }

    fn map_operation(
        &self,
        a: &Def<K, A1>,
        source: &[O],
        target: &[O],
    ) -> OpenHypergraph<O, Def<K, A2>> {
        match a {
            Def::Def(k) => {
                OpenHypergraph::singleton(Def::Def(k.clone()), source.to_vec(), target.to_vec())
            }
            Def::Arr(a) => {
                let g = self.functor.map_operation(a, source, target);
                g.map_edges(|e| Def::Arr(e))
            }
        }
    }

    fn map_arrow(&self, f: &OpenHypergraph<O, Def<K, A1>>) -> OpenHypergraph<O, Def<K, A2>> {
        try_define_map_arrow(self, f).unwrap()
    }
}

/// Apply a functor lifted to a category of definitions.
pub fn lift<F: Functor<O, T, O, U> + Clone, K: Clone, O: Clone + PartialEq, T: Clone, U: Clone>(
    functor: F,
    term: OpenHypergraph<O, Def<K, T>>,
) -> OpenHypergraph<O, Def<K, U>> {
    Lift { functor }.map_arrow(&term)
}