```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)))
```