{
 "cells": [
  {
   "cell_type": "markdown",
   "source": [
    "# Preorders\n",
    "\n",
    "\n",
    "Many of the ideas in category theory can be viewed as generalizations of\n",
    "preorders or monoids. This sketch shows some features of Catlab through the\n",
    "lens of preorders.\n",
    "You will see examples of defining GATs, Presentations, Syntax, and Functors.\n",
    "These are illustrated with preorders or thin categories, which are particularly\n",
    "simple cases of categories."
   ],
   "metadata": {}
  },
  {
   "outputs": [],
   "cell_type": "code",
   "source": [
    "using Core: GeneratedFunctionStub\n",
    "using Test\n",
    "\n",
    "using Catlab.Theories, Catlab.CategoricalAlgebra\n",
    "import Catlab.Theories: compose"
   ],
   "metadata": {},
   "execution_count": 1
  },
  {
   "cell_type": "markdown",
   "source": [
    "# Definition of a Preorder formalized as a GAT\n",
    "\n",
    "The following definitions can be found in the `Catlab.Theories` module.\n",
    "\n",
    "```julia\n",
    "\"\"\" Theory of *preorders*\n",
    "\n",
    "Preorders encode the axioms of reflexivity and transitivity as term constructors.\n",
    "\"\"\"\n",
    "@theory Preorder{El,Leq} begin\n",
    "  El::TYPE\n",
    "  Leq(lhs::El, rhs::El)::TYPE\n",
    "  @op (≤) := Leq\n",
    "\n",
    "  # Preorder axioms are lifted to term constructors in the GAT.\n",
    "  reflexive(A::El)::(A≤A) # ∀ A there is a term reflexive(A) which implies A≤A\n",
    "  transitive(f::(A≤B), g::(B≤C))::(A≤C) ⊣ (A::El, B::El, C::El)\n",
    "\n",
    "  # Axioms of the GAT are equivalences on terms or simplification rules in the logic\n",
    "  f == g ⊣ (A::El, B::El, f::(A≤B), g::(A≤B))\n",
    "  # Read as (f⟹ A≤B ∧ g⟹ A≤B) ⟹ f ≡ g\n",
    "end\n",
    "```\n",
    "\n",
    "# Preorders are Thin Categories\n",
    "\n",
    "Definition of a thin category\n",
    "```julia\n",
    "@theory ThinCategory{Ob,Hom} <: Category{Ob,Hom} begin\n",
    "  f == g ⊣ (A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B))\n",
    "end\n",
    "```\n",
    "\n",
    "of course this definition extends the GAT of categories\n",
    "\n",
    "```julia\n",
    "@theory Category{Ob,Hom} begin\n",
    "  # Unicode aliases.\n",
    "  @op begin\n",
    "  (→) := Hom\n",
    "  (⋅) := compose\n",
    "  end\n",
    "\n",
    "  \"\"\" Object in a category \"\"\"\n",
    "  Ob::TYPE\n",
    "\n",
    "  \"\"\" Morphism in a category \"\"\"\n",
    "  Hom(dom::Ob,codom::Ob)::TYPE\n",
    "\n",
    "  id(A::Ob)::(A → A)\n",
    "  compose(f::(A → B), g::(B → C))::(A → C) ⊣ (A::Ob, B::Ob, C::Ob)\n",
    "\n",
    "  # Category axioms.\n",
    "  ((f ⋅ g) ⋅ h == f ⋅ (g ⋅ h)\n",
    "  ⊣ (A::Ob, B::Ob, C::Ob, D::Ob, f::(A → B), g::(B → C), h::(C → D)))\n",
    "  f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B))\n",
    "  id(A) ⋅ f == f ⊣ (A::Ob, B::Ob, f::(A → B))\n",
    "end\n",
    "```\n",
    "\n",
    "Exercise: construct an isomorphism between the theory of thin categories and\n",
    "the theory of preorders. Show that they have the same models."
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "Once you have a GAT defined using the `@theory` macro, you can define presentations,\n",
    "which are logical syntax for giving examples of the theory. The GAT contains type\n",
    "and term constructors that you can use to write expressions. A presentation uses\n",
    "those expressions to create a specific example of the theory. We define `P` to be a preorder\n",
    "with 3 elements and 2 ≤ relationships."
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "Presentation{Catlab.Theories.ThThinCategory.Meta.T, Symbol}(Catlab.Theories.FreeThinCategory, (Ob = Catlab.Theories.FreeThinCategory.Ob{:generator}[X, Y, Z], Hom = Catlab.Theories.FreeThinCategory.Hom{:generator}[f, g]), Dict(:Z => (:Ob => 3), :f => (:Hom => 1), :X => (:Ob => 1), :Y => (:Ob => 2), :g => (:Hom => 2)), Pair[])"
     },
     "metadata": {},
     "execution_count": 2
    }
   ],
   "cell_type": "code",
   "source": [
    "@present P(FreeThinCategory) begin\n",
    "  (X,Y,Z)::Ob\n",
    "  f::Hom(X,Y)\n",
    "  g::Hom(Y,Z)\n",
    "end"
   ],
   "metadata": {},
   "execution_count": 2
  },
  {
   "cell_type": "markdown",
   "source": [
    "another example"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "Presentation{Catlab.Theories.ThThinCategory.Meta.T, Symbol}(Catlab.Theories.FreeThinCategory, (Ob = Catlab.Theories.FreeThinCategory.Ob{:generator}[X, Y, Z, Y′], Hom = Catlab.Theories.FreeThinCategory.Hom{:generator}[f, g, f′, g′]), Dict(:Z => (:Ob => 3), :f => (:Hom => 1), :f′ => (:Hom => 3), :X => (:Ob => 1), :Y => (:Ob => 2), :g => (:Hom => 2), :Y′ => (:Ob => 4), :g′ => (:Hom => 4)), Pair[])"
     },
     "metadata": {},
     "execution_count": 3
    }
   ],
   "cell_type": "code",
   "source": [
    "@present Q(FreeThinCategory) begin\n",
    "  (X,Y,Z)::Ob\n",
    "  f::Hom(X,Y)\n",
    "  g::Hom(Y,Z)\n",
    "  Y′::Ob\n",
    "  f′::Hom(X,Y′)\n",
    "  g′::Hom(Y′,Z)\n",
    "end"
   ],
   "metadata": {},
   "execution_count": 3
  },
  {
   "cell_type": "markdown",
   "source": [
    "Exercise: draw the Hasse diagrams for these preorders by hand."
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "# Composition is transitivity\n",
    "expressions in the presentation are paths in the Hasse Diagram"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "compose (generic function with 75 methods)"
     },
     "metadata": {},
     "execution_count": 4
    }
   ],
   "cell_type": "code",
   "source": [
    "function compose(P::Presentation, vs::Vector{Symbol})\n",
    "  compose(collect(generator(P, v) for v in vs))\n",
    "end"
   ],
   "metadata": {},
   "execution_count": 4
  },
  {
   "cell_type": "markdown",
   "source": [
    "expressions are represented at expression trees"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "f⋅g: X → Z",
      "text/latex": "$f \\cdot g : X \\to Z$"
     },
     "metadata": {},
     "execution_count": 5
    }
   ],
   "cell_type": "code",
   "source": [
    "ex = compose(P, [:f, :g])"
   ],
   "metadata": {},
   "execution_count": 5
  },
  {
   "cell_type": "markdown",
   "source": [
    "the head of an expression is the root of the expression tree"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": ":compose"
     },
     "metadata": {},
     "execution_count": 6
    }
   ],
   "cell_type": "code",
   "source": [
    "head(ex)"
   ],
   "metadata": {},
   "execution_count": 6
  },
  {
   "cell_type": "markdown",
   "source": [
    "the julia type of the expression"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "Catlab.Theories.FreeThinCategory.Hom{:compose}"
     },
     "metadata": {},
     "execution_count": 7
    }
   ],
   "cell_type": "code",
   "source": [
    "typeof(ex)"
   ],
   "metadata": {},
   "execution_count": 7
  },
  {
   "cell_type": "markdown",
   "source": [
    "the GAT type of the expression"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": ":Hom"
     },
     "metadata": {},
     "execution_count": 8
    }
   ],
   "cell_type": "code",
   "source": [
    "gat_typeof(ex)"
   ],
   "metadata": {},
   "execution_count": 8
  },
  {
   "cell_type": "markdown",
   "source": [
    "the parameters of the GAT Type"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "2-element Vector{GATExpr}:\n X\n Z"
     },
     "metadata": {},
     "execution_count": 9
    }
   ],
   "cell_type": "code",
   "source": [
    "gat_type_args(ex)"
   ],
   "metadata": {},
   "execution_count": 9
  },
  {
   "cell_type": "markdown",
   "source": [
    "in any thin category there is at most one morphism between any pair of objects.\n",
    "In symbols: ex₁::Hom(X,Y) ∧ ex₂::Hom(X,Y) ⟹ ex₁ == ex₂"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "\u001b[32m\u001b[1mTest Passed\u001b[22m\u001b[39m"
     },
     "metadata": {},
     "execution_count": 10
    }
   ],
   "cell_type": "code",
   "source": [
    "function thinequal(ex₁::FreeThinCategory.Hom, ex₂::FreeThinCategory.Hom)\n",
    "  dom(ex₁) == dom(ex₂) && codom(ex₁) == codom(ex₂)\n",
    "end\n",
    "\n",
    "@test thinequal(ex, compose(P, [:f,:g])⋅id(generator(P,:Z)))"
   ],
   "metadata": {},
   "execution_count": 10
  },
  {
   "cell_type": "markdown",
   "source": [
    "Thinking in terms of preorders, the composite f⋅g::Hom(X,Z) is a proof that X ≤ Z\n",
    "in logical notation you would say f::Hom(X,Y) and g::Hom(Y,Z) ⊢ f⋅g::Hom(X,Z)\n",
    "given a proof that X≤Y and a proof of Y≤Z then ⋅ will create a proof of X≤Z\n",
    "by composing the proofs sequentially like chaining inequalities in math\n",
    "a key aspect of category theory is that you want to work constructively\n",
    "you don't want to know that there exists a composite, you want to hold onto that composite.\n",
    "in programming, the way that you hold onto things is putting data into data structures.\n",
    "While computers can access things by offset or addresses, programmers want to use names\n",
    "so when we prove in P that X≤Z, we name that proof by adding it as a generator"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "f⋅g: X → Z",
      "text/latex": "$f \\cdot g : X \\to Z$"
     },
     "metadata": {},
     "execution_count": 11
    }
   ],
   "cell_type": "code",
   "source": [
    "@present P₂(FreeThinCategory) begin\n",
    "  (X,Y,Z)::Ob\n",
    "  f::Hom(X,Y)\n",
    "  g::Hom(Y,Z)\n",
    "  h::Hom(X,Z)\n",
    "end\n",
    "\n",
    "ex = compose(P₂, [:f, :g])"
   ],
   "metadata": {},
   "execution_count": 11
  },
  {
   "cell_type": "markdown",
   "source": [
    "Now that we have a name for h, we can see that thinequal knows that f⋅g == h because\n",
    "according to the definition of a thin category, any two morphisms with the same\n",
    "domain and codomain are equal."
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "\u001b[32m\u001b[1mTest Passed\u001b[22m\u001b[39m"
     },
     "metadata": {},
     "execution_count": 12
    }
   ],
   "cell_type": "code",
   "source": [
    "@test thinequal(ex, generator(P₂, :h))"
   ],
   "metadata": {},
   "execution_count": 12
  },
  {
   "cell_type": "markdown",
   "source": [
    "There is an imperative interface to manipulating presentations by mutating them for this purpose"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "6-element Vector{Any}:\n X\n Y\n Z\n f: X → Y\n g: Y → Z\n h: X → Z"
     },
     "metadata": {},
     "execution_count": 13
    }
   ],
   "cell_type": "code",
   "source": [
    "P₂′ = copy(P)\n",
    "add_generator!(P₂′, Hom(:h, P[:X], P[:Z]))\n",
    "generators(P₂′)"
   ],
   "metadata": {},
   "execution_count": 13
  },
  {
   "cell_type": "markdown",
   "source": [
    "We could avoid this naming the homs situation by giving all the homs the same name\n",
    "however, then when you tried to write down a morphism, you wouldn't be able to refer\n",
    "to a specific one by name, because they are all named ≤."
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "4-element Vector{Any}:\n x\n y\n z\n ≤: x → y"
     },
     "metadata": {},
     "execution_count": 14
    }
   ],
   "cell_type": "code",
   "source": [
    "@present R(FreeThinCategory) begin\n",
    "  (x,y,z)::Ob\n",
    "  (≤)::Hom(x,y)\n",
    "end\n",
    "generators(R)"
   ],
   "metadata": {},
   "execution_count": 14
  },
  {
   "cell_type": "markdown",
   "source": [
    "Catlab won't let you make a presentation where the homs have the same exact name.\n",
    "So, this will error:\n",
    "\n",
    "```julia\n",
    "@present Q(FreeThinCategory) begin\n",
    "  (x,y,z)::Ob\n",
    "  (≤)::Hom(x,y)\n",
    "  (≤)::Hom(y,z)\n",
    "  (≤)::Hom(x,z)\n",
    "end\n",
    "```\n",
    "\n",
    "However, you can omit the names for homs with the following syntax, which is useful for thin categories.\n",
    "\n",
    "```julia\n",
    "@present Q(FreeThinCategory) begin\n",
    "  (x,y,z)::Ob\n",
    "  ::Hom(x,y)\n",
    "  ::Hom(y,z)\n",
    "  ::Hom(x,z)\n",
    "end\n",
    "```"
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "In a thin category, all the homs with the same domain and codomain are the same,\n",
    "so why don't we name them by their the domain and codomain and then use the property\n",
    "that any two homs with the same name are the same to encode the thinness. This is what\n",
    "the Hasse diagram representation does for us. The edges in the diagram are encoding the\n",
    "presentation data into a combinatorial object that we can visualize. There are many\n",
    "reasons to encode a logical structure into a combinatorial strucuture, one is that\n",
    "we generally have ways of drawing combinatorial objects that convey their saliant structure\n",
    "and enable visual reasoning. Another is algorithms, isomorphism between the combinatorial representations\n",
    "provide some of the isomorphisms between the logical structures. in this case, a graph homomorphism between Hasse Diagrams\n",
    "construct isomorphisms between the preorders they present. The converse is not true since there can be many Graphs\n",
    "that present the same preorder."
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "# Monotone Maps"
   ],
   "metadata": {}
  },
  {
   "cell_type": "markdown",
   "source": [
    "a generator is in the set of homs if it is in the list of generators"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "in_homs (generic function with 1 method)"
     },
     "metadata": {},
     "execution_count": 15
    }
   ],
   "cell_type": "code",
   "source": [
    "in_homs(f::FreeThinCategory.Hom{:generator}, C::FinCat) =\n",
    "  f in hom_generators(C)"
   ],
   "metadata": {},
   "execution_count": 15
  },
  {
   "cell_type": "markdown",
   "source": [
    "a composite hom is in the list set of homs if all of its components are."
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "in_homs (generic function with 2 methods)"
     },
     "metadata": {},
     "execution_count": 16
    }
   ],
   "cell_type": "code",
   "source": [
    "in_homs(f::FreeThinCategory.Hom{:compose}, C::FinCat) =\n",
    "  all(fᵢ->in_homs(fᵢ, C), args(f))"
   ],
   "metadata": {},
   "execution_count": 16
  },
  {
   "cell_type": "markdown",
   "source": [
    "we can check if a map is functorial, which is called monotone for preorders.\n",
    "1. make sure all the objects in the domain are sent to objects in the codomain\n",
    "2. make sure all the homs are sent to homs in the codomain\n",
    "3. check that the domains and codomainss of the homs match"
   ],
   "metadata": {}
  },
  {
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": "\u001b[32m\u001b[1mTest Passed\u001b[22m\u001b[39m"
     },
     "metadata": {},
     "execution_count": 17
    }
   ],
   "cell_type": "code",
   "source": [
    "function is_functorial(F::FinFunctor)\n",
    "  pₒ = map(ob_generators(dom(F))) do X\n",
    "    F(X) in ob_generators(codom(F))\n",
    "  end |> all\n",
    "\n",
    "  pₕ = map(hom_generators(dom(F))) do f\n",
    "    in_homs(F(f), codom(F))\n",
    "  end |> all\n",
    "\n",
    "  pᵩ = map(hom_generators(dom(F))) do f\n",
    "    FX = F(dom(f))\n",
    "    FY = F(codom(f))\n",
    "    Ff = F(f)\n",
    "    dom(Ff) == FX && codom(Ff) == FY\n",
    "  end |> all\n",
    "  return pₒ && pₕ && pᵩ\n",
    "end\n",
    "\n",
    "@present Q(FreeThinCategory) begin\n",
    "  (a,b,c,d)::Ob\n",
    "  ab::Hom(a,b)\n",
    "  bc::Hom(b,c)\n",
    "  cd::Hom(c,d)\n",
    "end\n",
    "generators(Q)\n",
    "\n",
    "Fₒ = Dict(:X=>:a, :Y=>:b, :Z=>:c)\n",
    "Fₕ = Dict(:f=>:ab, :g=>:bc)\n",
    "F = FinFunctor(Fₒ, Fₕ, P, Q)\n",
    "@test is_functorial(F)\n",
    "\n",
    "Fₒ = Dict(:X=>:a, :Y=>:b, :Z=>:d)\n",
    "Fₕ = Dict(:f=>:ab, :g=>[:bc, :cd])\n",
    "F = FinFunctor(Fₒ, Fₕ, P, Q)\n",
    "@test is_functorial(F)\n",
    "\n",
    "\n",
    "Fₒ = Dict(:X=>:a, :Y=>:b, :Z=>:c)\n",
    "Fₕ = Dict(:f=>:ab, :g=>[:bc, :cd])\n",
    "F = FinFunctor(Fₒ, Fₕ, P, Q)\n",
    "@test !is_functorial(F)"
   ],
   "metadata": {},
   "execution_count": 17
  },
  {
   "cell_type": "markdown",
   "source": [
    "Monotone maps are functors for thin categories. One of the benefits of\n",
    "category theory is that we find abstractions that work in multiple domains.\n",
    "The abstraction of preserving the domains and codomains of morphisms is\n",
    "a key abstraction that we can use to define many notions in mathematics."
   ],
   "metadata": {}
  }
 ],
 "nbformat_minor": 3,
 "metadata": {
  "language_info": {
   "file_extension": ".jl",
   "mimetype": "application/julia",
   "name": "julia",
   "version": "1.10.2"
  },
  "kernelspec": {
   "name": "julia-1.10",
   "display_name": "Julia 1.10.2",
   "language": "julia"
  }
 },
 "nbformat": 4
}