open import Relation.Binary.PropositionalEquality

module 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

-- We prove that IR+ is a category, i.e. that idIR+ really is an
-- identity and that _∘IR+_ is associative (assuming C is a category)

open import Function

import posIR
open posIR C HomC idC _∘C_

module _ (ext : ∀ {c d} → Extensionality c d) where

  id-left : {a b : IR+} -> (f : Hom a b) -> 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 : {a b : IR+} -> (f : Hom a b) -> 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 : {a b c d : IR+} -> (f : Hom c d) ->
                             (g : Hom b c) ->
                             (h : Hom a b) ->
                             (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)))