Idr.agda

module Idr where

open import Function.Equality
open import Function.Inverse
open import Level
open import Relation.Binary.PropositionalEquality
  renaming (cong to cong-f)

record _≃_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor iso
  field
    to   : A → B
    from : B → A

    id₁ : ∀ x → to (from x) ≡ x
    id₂ : ∀ x → from (to x) ≡ x

there : ∀ {a b} (A : Set a) (B : Set b) →
        A ≃ B →
        A ↔ B
there A B (iso f g p q) = record
  { to = record
    { _⟨$⟩_ = f
    ; cong = cong-f f
    }
  ; from = record
    { _⟨$⟩_ = g
    ; cong = cong-f g
    }
  ; inverse-of = record
    { left-inverse-of = q
    ; right-inverse-of = p
    }
  }

back : ∀ {a b} (A : Set a) (B : Set b) →
       A ↔ B →
       A ≃ B
back A B eq = record
  { to   = Π._⟨$⟩_ (Inverse.to eq)
  ; from = Π._⟨$⟩_ (Inverse.from eq)
  ; id₁ = _InverseOf_.right-inverse-of (Inverse.inverse-of eq)
  ; id₂ = _InverseOf_.left-inverse-of (Inverse.inverse-of eq)
  }