{- Defining the product in the category of directed multigraphs -}
import Level
open Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Structures
open import Data.Product
open import Function hiding (id)

variable v e : Level

record Graph : Set (Level.suc (v Level.⊔ e)) where
  field
    V : Set v
    E : Set e
    s t : E → V

record Hom (G₁ G₂ : Graph {v} {e}) : Set (v Level.⊔ e) where
  module G₁ = Graph G₁
  module G₂ = Graph G₂
  field
    fᵥ : G₁.V → G₂.V
    fₑ : G₁.E → G₂.E
    comm-s : G₂.s ∘ fₑ ≗ fᵥ ∘ G₁.s
    comm-t : G₂.t ∘ fₑ ≗ fᵥ ∘ G₁.t
open Hom
    
variable o m p : Level

record Category : Set (Level.suc (o Level.⊔ m Level.⊔ p)) where
  field
    O : Set o
    hom[_,_] : (A B : O) → Set m
    _≈_ : {A B : O} → (f g : hom[ A , B ]) → Set p
    ≈-equiv : {A B : O} → IsEquivalence (_≈_ {A} {B})
    id : (A : O) → hom[ A , A ]
    _⊗_ : {A B C : O} → hom[ B , C ] → hom[ A , B ] → hom[ A , C ]

    assoc : {A B C D : O} → (f : hom[ A , B ]) → (g : hom[ B , C ]) → (h : hom[ C , D ]) → (h ⊗ (g ⊗ f)) ≈ ((h ⊗ g) ⊗ f)
    idₗ : {A B : O} → (f : hom[ A , B ]) → (id B ⊗ f) ≈ f
    idᵣ : {A B : O} → (f : hom[ A , B ]) → (f ⊗ id A) ≈ f
open Category

module _ where
  variable ℓ : Level
  variable A B : Set ℓ
  variable f g h : A → B

  ≗-refl : f ≗ f
  ≗-refl x = refl

  ≗-sym : f ≗ g → g ≗ f
  ≗-sym p x = sym (p x)

  ≗-trans : f ≗ g → g ≗ h → f ≗ h
  ≗-trans p q x = trans (p x) (q x)

Graphs : Category {Level.suc (v Level.⊔ e)} {v Level.⊔ e} {v Level.⊔ e}
Graphs {v} {e} .O = Graph {v} {e}
Graphs .hom[_,_] G₁ G₂ = Hom G₁ G₂
Graphs ._≈_ f g = f .fᵥ ≗ g .Hom.fᵥ × f .Hom.fₑ ≗ g .Hom.fₑ
Graphs .≈-equiv .IsEquivalence.refl = ≗-refl , ≗-refl
Graphs .≈-equiv .IsEquivalence.sym = map ≗-sym ≗-sym
Graphs .≈-equiv .IsEquivalence.trans (p , q) (h , j) = (≗-trans p h) , ≗-trans q j
Graphs .id A .fᵥ x = x
Graphs .id A .fₑ x = x
Graphs .id A .comm-s _ = refl
Graphs .id A .comm-t _ = refl
(Graphs ⊗ f) g .fᵥ = f .fᵥ ∘ g .fᵥ
(Graphs ⊗ f) g .fₑ = f .fₑ ∘ g .fₑ
(Graphs ⊗ f) g .comm-s x = trans (f .comm-s (g .fₑ x)) (cong (f .fᵥ) (g .comm-s x))
(Graphs ⊗ f) g .comm-t x = trans (f .comm-t (g .fₑ x)) (cong (f .fᵥ) (g .comm-t x))
Graphs .assoc f g h = (λ x → refl) , (λ x → refl)
Graphs .idₗ f = (λ x → refl) , (λ x → refl)
Graphs .idᵣ = λ f → (λ x → refl) , (λ x → refl)

module _ (𝓒 : Category {o} {m} {p}) where
  module 𝓒 = Category 𝓒
  record Product (A B : 𝓒.O) : Set (o Level.⊔ m Level.⊔ p) where
    field
      P : 𝓒.O
      π₁ : 𝓒.hom[ P , A ]
      π₂ : 𝓒.hom[ P , B ]
      universal : ∀ {C : 𝓒.O} (f : 𝓒.hom[ C , A ]) (g : 𝓒.hom[ C , B ]) → ∃! 𝓒._≈_ λ h → (π₁ 𝓒.⊗ h) 𝓒.≈ f × (π₂ 𝓒.⊗ h) 𝓒.≈ g

open Product

Graph-Product : (A B : Graph {v} {e}) → Product (Graphs {v} {e}) A B
Graph-Product A B .P .Graph.V = A .Graph.V × B .Graph.V
Graph-Product A B .P .Graph.E = A .Graph.E × B .Graph.E
Graph-Product A B .P .Graph.s (a , b) = (A .Graph.s a) , B .Graph.s b
Graph-Product A B .P .Graph.t (a , b) = (A .Graph.t a) , B .Graph.t b
Graph-Product A B .π₁ .fᵥ = proj₁
Graph-Product A B .π₁ .fₑ = proj₁
Graph-Product A B .π₁ .comm-s _ = refl
Graph-Product A B .π₁ .comm-t _ = refl
Graph-Product A B .π₂ .fᵥ = proj₂
Graph-Product A B .π₂ .fₑ = proj₂
Graph-Product A B .π₂ .comm-s _ = refl
Graph-Product A B .π₂ .comm-t _ = refl
Graph-Product A B .universal f g .proj₁ .fᵥ = λ x → (f .fᵥ x) , (g .fᵥ x)
Graph-Product A B .universal f g .proj₁ .fₑ = λ x → (f .fₑ x) , (g .fₑ x)
Graph-Product A B .universal f g .proj₁ .comm-s x = cong₂ _,_ (f .comm-s x) (g .comm-s x)
Graph-Product A B .universal f g .proj₁ .comm-t x = cong₂ _,_ (f .comm-t x) (g .comm-t x)
Graph-Product A B .universal f g .proj₂ .proj₁ = ((λ x → refl) , (λ x → refl)) , ((λ x → refl) , (λ x → refl))
Graph-Product A B .universal f g .proj₂ .proj₂ ((p , q) , (h , j)) = (λ x → (cong₂ _,_ (sym (p x)) (sym (h x)))) , λ x → cong₂ _,_ (sym (q x)) (sym (j x))