open import Relation.Binary.PropositionalEquality

module Uniform.Category
  (C : Set1)(HomC : C -> C -> Set)
  (idC : (c : C) -> HomC c c)
  (_∘C_ : {a b c : C} -> HomC b c -> HomC a b -> HomC a c)
  (id-unit-left : {a b : C} -> (f : HomC a b) -> (idC b) ∘C f ≡ f)
  (id-unit-right : {a b : C} -> (f : HomC a b) -> f ∘C (idC a) ≡ f)
  (assocC : {a b c d : C} -> (f : HomC c d) -> (g : HomC b c) -> (h : HomC a b) -> (f ∘C g) ∘C h ≡ f ∘C (g ∘C h)) where

import Prelude
open Prelude C HomC idC _∘C_
import Uniform.posIR
open Uniform.posIR C HomC idC _∘C_


open import Data.Empty
open import Data.Unit
open import Data.Product
open import Function


module _ (ext : ∀ {a b} -> {A : Set a}{B : A -> Set b}{f g : (x : A) -> B x} -> ((x : A) -> f x ≡ g x) -> f ≡ g) where

  id-left : {Γ Δ : Ctxt}{e : Env Γ}{e' : Env Δ} ->
            {γ : IR' Γ}{γ' : IR' Δ} ->
            (f : Hom' e e' γ γ') -> idIR' γ' ∘IR' f ≡ f
  id-left (ι→ι f) = cong ι→ι (id-unit-left f)
  id-left (σ→σ h γ) = cong (λ z → σ→σ h z) (ext (λ a → id-left (γ a)) )
  id-left (δ→δ g γ) = cong (λ z → δ→δ g z) (ext (λ k → id-left (γ k)))

  id-right : {Γ Δ : Ctxt}{e : Env Γ}{e' : Env Δ} ->
             {γ : IR' Γ}{γ' : IR' Δ} ->
             (f : Hom' e e' γ γ') -> f ∘IR' idIR' γ ≡ f
  id-right (ι→ι f) = cong ι→ι (id-unit-right f)
  id-right (σ→σ h γ) = cong (λ z → σ→σ h z) (ext (λ a → id-right (γ a)) )
  id-right (δ→δ g γ) = cong (λ z → δ→δ g z) (ext (λ k → id-right (γ k)))


  assoc : {Γ Γ' Γ'' Γ''' : Ctxt} ->
          {e : Env Γ}{e' : Env Γ'}{e'' : Env Γ''}{e''' : Env Γ'''} ->
          {γ : IR' Γ}{γ' : IR' Γ'}{γ'' : IR' Γ''}{γ''' : IR' Γ'''} ->
          (f : Hom' e'' e''' γ'' γ''')(g : Hom' e' e'' γ' γ'')
          (h : Hom' e e' γ γ') ->
          (f ∘IR' g) ∘IR' h ≡ f ∘IR' (g ∘IR' h)
  assoc (ι→ι f)   (ι→ι g)   (ι→ι h) = cong ι→ι (assocC f g h)
  assoc (σ→σ h γ) (σ→σ g φ) (σ→σ k ψ)
    = cong (σ→σ _) (ext (λ a → assoc (γ (g (k a))) (φ (k a)) (ψ a)))
  assoc (δ→δ h γ) (δ→δ g φ) (δ→δ k ψ)
    = cong (δ→δ _) (ext (λ l → assoc (γ (l ∘ k ∘ g)) (φ (l ∘ k)) (ψ l)))