namespace http://mathhub.info/MitM/core/graphs❚

import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/core/typedsets ❚
import num http://mathhub.info/MitM/core/arithmetics ❚

theory VertexColoredGraphs : base:?Logic =
    include ?Graphs ❙

    theory vertexcoloredgraph_theory : base:?Logic =
        include ☞?Graphs/ugraph_theory ❙

        colors :set ℕ ❙ // we assume at most countably many colors indexed by ℕ ❙
        color : nodetype ⟶ asType colors ❙
    ❚

    theory undirectedVertexcoloredgraph_theory : base:?Logic =
        include ☞?Graphs/ugraph_theory ❙
        include ☞?VertexColoredGraphs/vertexcoloredgraph_theory ❙
    ❚
❚

theory EdgeColoredGraphs : base:?Logic =
    include ?Graphs ❙

    theory edgecoloredgraph_theory : base:?Logic =
        include ☞?Graphs/dgraph_theory ❙

        colors : set ℕ ❙ // we assume at most countably many colors indexed by ℕ ❙
        colorOf : {a,b:nodetype} ⊦ edges a b ⟶ asType colors ❘ # color 1 2 %I3 ❙


        color_symm_prop : prop ❘ = ∀[a] ∀[b] ∀[p] ∀[q] edges a b ⇒ colorOf a b p ≐ colorOf b a q ❙
        // TODO needs eliminating the second proof argument ❙
    ❚

    theory undirectedEdgecoloredgraph_theory : base:?Logic =
        include ☞?Graphs/ugraph_theory ❙
        include ☞?EdgeColoredGraphs/edgecoloredgraph_theory ❙


        color_symm : ⊦ color_symm_prop ❙
        proper_prop :prop ❘ = ∀[a] ∀ ∈ (neighbours a) . [b] ∀ ∈ (neighbours a) . [c] ∀[p] ∀[q] b ≠ c ⇒ colorOf a b p ≠ colorOf a c q ❙
        // TODO needs eliminating the second proof argument ❙
    ❚

    uecGraph : Mod ☞?EdgeColoredGraphs/undirectedEdgecoloredgraph_theory ❙


    theory properEdgecoloredgraph_theory : base:?Logic =
        include ☞?EdgeColoredGraphs/undirectedEdgecoloredgraph_theory ❙

        is_proper : ⊦ proper_prop ❙
    ❚

    properedgecoloredGraph = Mod ☞?EdgeColoredGraphs/properEdgecoloredgraph_theory ❙

    subGraph : properedgecoloredGraph ⟶ (nodetype ⟶ prop) ⟶ (nodetype ⟶ nodetype ⟶ prop) ⟶ properedgecoloredGraph ❙
    // TODO definiens ❙
    // TODO generalize ❙

    components: properedgecoloredGraph ⟶ set properedgecoloredGraph ❙
❚

theory ColoredGraphMorphisms : base:?Logic =
    include ?GraphMorphisms ❙
    include ?EdgeColoredGraphs ❙
    include ☞base:?InformalProofs ❙

    theory colorPreservingMorphism > g1 : uecGraph, g2 : uecGraph ❘ =
        include ☞?GraphMorphisms/graphMorphism_theory g1 g2 ❙

        // preservation_property : ⊦ ∀ ∈ (g1.nodes) . [n1] ∀ ∈ (g1.nodes) . [n2] ∀ [p : ⊦ (g1.edges) n1 n2]
            (g1.colorOf)  n1 n2 p ≐ (g2.colorOf) (fun n1) (fun n2) trivial ❙
    ❚
❚

theory Maniplexes :base:?Logic =
    include ?EdgeColoredGraphs ❙

    theory maniplex_theory : base:?Logic > rank : ℕ ❘ =
        include ☞?Graphs/ugraph_theory ❙

        structure colored : ?EdgeColoredGraphs/properEdgecoloredgraph_theory =
            nodes = nodes ❙
            edges = edges ❙
            colors @ colors ❘ = ⟪ (fullset ℕ) | ([x] x < rank) ⟫ ❙
            colorOf @ colorOf ❙
        ❚

        this : properedgecoloredGraph ❙ // TODO ❙

        is_n_regular : ⊦ n_regular rank ❙
        subgraph_induced_by_colors : {i : ℕ, j : ℕ} properedgecoloredGraph ❙
        // TODO ❙

        has_squares_prop : prop ❘ // = ∀ ∈ colors . [i] ∀ ∈ colors . [j] ((max i j) - (min i j)) > 1 ⇒
                                                ∀ ∈ (components (subgraph_induced_by_colors i j)) . [C] ∃= 4 ∈ (C.nodes) . [x] true ❙

        has_squares : ⊦ has_squares_prop ❙


        pathIntersection_property : prop ❙
        // For every pair of nodes (u,v) and every pair of colors (i,j):
            if there is a path (TODO!) from u to v that only uses colors >i and a second path that only uses colors <j,
            then there's a path that only uses colors c with i<c<j
         ❙
    ❚

    maniplex = [n:ℕ] Mod ☞?Maniplexes/maniplex_theory n ❙

    dual : {n:ℕ} maniplex n ⟶ maniplex n ❘
        // swaps edges of color i with edges of color n - 1 - i  ❙

    k_faces : {rank : ℕ} maniplex rank ⟶ ℕ ⟶ set properedgecoloredGraph ❘
      // = [r,M,k] components (subGraph M ([x] true) ([x,y] (M.color) x y ≠ k)) ❙

    k_face_flagGraph : {rank : ℕ} maniplex rank ⟶ ℕ ⟶ set properedgecoloredGraph ❘
        // = [r,M,k] components (subGraph M ([x] true) ([x,y] (M.color) x y < k)) ❙
    // return type should be set (maniplex k) ❙

    facet : {rank : ℕ} maniplex rank ⟶ set properedgecoloredGraph ❘
        // = [r,M] k_face_flagGraph r M (r-1) ❙
    // return type should be set (maiplex rank-1) ❙

    // k_face_flagGraph preserves pathIntersection_property i.e. return type polytopeFlagGraph ❙

    vertex_figures : {rank : ℕ} maniplex rank ⟶ set properedgecoloredGraph ❘
        = [r,M] k_face_flagGraph r M 0 ❙ // ...and shift colors to get maniplex/polytopeFlagGraph again ❙

    theory polytopeFlagGraph_theory : base:?Logic > rank : ℕ ❘ =
        include ☞?Maniplexes/maniplex_theory (rank) ❙

        hasPathIntersection : ⊦ pathIntersection_property ❙
    ❚
❚