foo.agda

module Foo where

{-

https://arxiv.org/pdf/1912.10642.pdf

I'd like to learn categroy theory finally.
To this end I'm going to show it.

Ultimately I'd like to reconcile it with homotopy and make use
of it in describing databases and connectiveness or geometry.

Categories encompass graphs, graphs encompass trees, trees
encompass lists, lists encompass naturals. Understanding
categories will result in insights to the rest.

ps subjects:
What is a string diagram?

bib links:

This
https://arxiv.org/pdf/1912.10642.pdf

Category Theory in Context
http://www.math.jhu.edu/~eriehl/context.pdf 

Categorical homotopy theory
http://www.math.jhu.edu/~eriehl/cathtpy.pdf

An invitation to applied category theory: seven sketches
in compositionality
https://arxiv.org/pdf/1803.05316.pdf



-}

open import Relation.Binary.PropositionalEquality

record Category (_⇝_ : Set → Set → Set) : Set₁ where
  infixr 8 _⇝_
  field
    id : ∀ {x} → x ⇝ x
    _∘_ : ∀ {a b c : Set} → (b ⇝ c) → (a ⇝ b) → (a ⇝ c)
  
    unitalityˡ : ∀ {X Y} {f : X ⇝ Y} → id ∘ f ≡ f
    unitalityʳ : ∀ {X Y} {f : X ⇝ Y} → f ∘ id ≡ f

    associativity : ∀ {X Y Z W} {f : X ⇝ Y} {g : Y ⇝ Z} {h : Z ⇝ W}
                  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
    
{-

/agdaproj/cat/src/Foo.agda:42,12-15
The following names are not declared in the same scope as their
syntax or fixity declaration (i.e., either not in scope at all,
imported from another module, or declared in a super module): _⇝_
when scope checking the declaration
  record Category _⇝_ where
    infixr 8 _⇝_
    field
      id : ∀ {x} → x ⇝ x
      _∘_ : {a b c : Set} → (b ⇝ c) → (a ⇝ b) → (a ⇝ c)
      unitalityˡ : ∀ {X} {Y} {f : X ⇝ Y} → id ∘ f ≡ f
      unitalityʳ : ∀ {X} {Y} {f : X ⇝ Y} → f ∘ id ≡ f
      associativity :
        ∀ {X} {Y} {Z} {W} {f : X ⇝ Y} {g : Y ⇝ Z} {h : Z ⇝ W} →
        h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f

-}