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

{-------------------------------------------------------}
```