module Prelude.Equivalences where

-- Equivalences in Fam D

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam

open _Fam⇒_

{------ The type of equivalences -----------------------}

record _≃_ {D : Set1}(P Q : Fam D) : Set1 where
  field
    left  : P Fam⇒ Q
    right : Q Fam⇒ P
    leftright : left Fam∘ right ≡ FamId _
    rightleft : right Fam∘ left ≡ FamId _
    -- naive definition assuming all types are sets for now; these are
    -- logically equivalent to real equivalences anyway
open _≃_

{-------------------------------------------------------}

{------ ≃ is an equivalence relation -------------------}


IdEq : ∀ {D} {A : Fam D} -> A ≃ A
left IdEq = FamId _
right IdEq = FamId _
leftright IdEq = refl
rightleft IdEq = refl

symEq : ∀ {D} {A B : Fam D} -> A ≃ B -> B ≃ A
left (symEq p) = right p
right (symEq p) = left p
leftright (symEq p) = rightleft p
rightleft (symEq p) = leftright p

transEq : ∀ {D} {A B C : Fam D} -> A ≃ B -> B ≃ C -> A ≃ C
left (transEq p q) = left q Fam∘ left p
right (transEq p q) = right p Fam∘ right q
leftright (transEq p q)
  = comp-is-id-ext
     (left q Fam∘ left p)
     (right p Fam∘ right q)
     (λ x → trans (sym (happly (cong indmor (leftright q)) x))
                  (cong (indmor (left q))
                        (sym (happly (cong indmor (leftright p))
                                     (indmor (right q) x)))))
     (λ y → UIP _ _) -- TODO: this should be doable
rightleft (transEq p q)
  = comp-is-id-ext
     (right p Fam∘ right q)
     (left q Fam∘ left p)
     (λ x → trans (sym (happly (cong indmor (rightleft p)) x))
                  (cong (indmor (right p))
                        (sym (happly (cong indmor (rightleft q))
                                     (indmor (left p) x)))))
     (λ y → UIP _ _) -- TODO: this should be doable

{-------------------------------------------------------}

{----- Constructions closed under ≃ --------------------}

-- coproducts
+-≃ : ∀ {D}{A B A' B' : Fam D} -> A ≃ A' -> B ≃ B' ->
        (A Fam+ B) ≃ (A' Fam+ B')
left (+-≃ p q) = (⊎-map (indmor (left p)) ((indmor (left q))) ,
                  (λ { (inj₁ x) → indmor= (left p) x ;
                       (inj₂ y) → indmor= (left q) y }))
right (+-≃ p q) = (⊎-map (indmor (right p)) ((indmor (right q))) ,
                  (λ { (inj₁ x) → indmor= (right p) x ;
                       (inj₂ y) → indmor= (right q) y }))
leftright (+-≃ p q)
 = comp-is-id-ext
     (left (+-≃ p q))
     (right (+-≃ p q))
     (λ {(inj₁ x) → cong inj₁
                         (sym (happly (cong indmor (leftright p)) x)) ;
         (inj₂ y) → cong inj₂
                         (sym (happly (cong indmor (leftright q)) y)) })
                         (λ y → UIP _ _) -- TODO: again, shouldn't be hard
rightleft (+-≃ p q)
 = comp-is-id-ext
     (right (+-≃ p q))
     (left (+-≃ p q))
     (λ {(inj₁ x) → cong inj₁
                         (sym (happly (cong indmor (rightleft p)) x)) ;
         (inj₂ y) → cong inj₂
                         (sym (happly (cong indmor (rightleft q)) y)) })
                         (λ y → UIP _ _) -- TODO: again, shouldn't be hard

{-------------------------------------------------------}