```open import Relation.Binary.PropositionalEquality

module Prelude.Isos
(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

open import Function.Equality hiding (id; _∘_; cong)
open import Function.Inverse renaming (id to ↔refl; _∘_ to ↔trans; sym to ↔sym)
open ≡-Reasoning

import Prelude
open Prelude C HomC idC _∘C_

-- Isos in FamC ---

record _↔C_ (X Y : C) : Set1 where
field
to : HomC X Y
from : HomC Y X
left-inverse-of : from ∘C to ≡ idC X
right-inverse-of : to ∘C from ≡ idC Y
open _↔C_ public

↔C-refl : {X : C} -> X ↔C X
↔C-refl = record
{ to = idC _
; from = idC _
; left-inverse-of = id-unit-left (idC _)
; right-inverse-of = id-unit-right (idC _) }

↔C-trans : {X Y Z : C} -> X ↔C Y -> Y ↔C Z -> X ↔C Z
↔C-trans p q = record
{ to = to q ∘C to p
; from = from p ∘C from q
; left-inverse-of
= begin
(from p ∘C from q) ∘C (to q ∘C to p)
≡⟨ trans (assocC _ _ _)
(cong (λ z → from p ∘C z) (sym (assocC _ _ _))) ⟩
from p ∘C ((from q ∘C to q) ∘C to p)
≡⟨ trans (cong (λ z → from p ∘C (z ∘C to p))
(left-inverse-of q))
(cong (λ z → from p ∘C z) (id-unit-left _)) ⟩
from p ∘C to p
≡⟨ left-inverse-of p ⟩
idC _
∎
; right-inverse-of
= begin
(to q ∘C to p) ∘C (from p ∘C from q)
≡⟨ trans (sym (assocC _ _ _))
(cong (λ z → z ∘C from q) (assocC _ _ _)) ⟩
(to q ∘C (to p ∘C from p)) ∘C from q
≡⟨ trans (cong (λ z → (to q ∘C z) ∘C from q)
(right-inverse-of p))
(cong (λ z → z ∘C from q) (id-unit-right _)) ⟩
to q ∘C from q
≡⟨ right-inverse-of q ⟩
idC _
∎
}

↔C-sym : {X Y : C} -> X ↔C Y -> Y ↔C X
↔C-sym p = record
{ to = from p
; from = to p
; left-inverse-of = right-inverse-of p
; right-inverse-of = left-inverse-of p }

record _↔FamC_ (A B : FamC) : Set1 where
open Inverse
open Function.Equality.Π

field
index↔ : index A   ↔ index B
fam↔ : (x : index A) -> fam A x ↔C fam B ((Inverse.to index↔) ⟨\$⟩ x)
open _↔FamC_ public

↔FamC-refl : {A : FamC} -> A ↔FamC A
↔FamC-refl = record { index↔ = ↔refl ; fam↔ = λ a → ↔C-refl }

↔FamC-trans : {A B C : FamC} -> A ↔FamC B -> B ↔FamC C -> A ↔FamC C
↔FamC-trans p q = record { index↔ = ↔trans (index↔ q) (index↔ p)
; fam↔ = λ a → ↔C-trans (fam↔ p a) (fam↔ q _) }

↔FamC-sym : {A B : FamC} -> A ↔FamC B -> B ↔FamC A
↔FamC-sym {A} {B} p
= record
{ index↔ = ↔sym (index↔ p)
; fam↔ = λ a → ↔C-sym (subst (λ z → fam A (Inverse.to (↔sym (index↔ p))
⟨\$⟩ a) ↔C Prelude.fam B z)
(Inverse.right-inverse-of (index↔ p) a)
(fam↔ p ((Inverse.from (index↔ p)) ⟨\$⟩ a)))
}
```