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