Definition bi-invertibility

BiInverse.agda

{-# OPTIONS --without-K #-}

-- BiInverse definition
-- f : A ≃ B
-- HoTT book
-- 4.3 Bi-invertible maps

module BiInverse where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

record _≃_ (A B : Set) : Set where
  field
    apply  : A → B
    linv   : B → A
    rinv   : B → A
    isLinv : (x : A) → linv (apply x) ≡ x
    isRinv : (y : B) → apply (rinv y) ≡ y

open _≃_

-- Lemma 1.17
linv-is-rinv : {A B : Set} (f : A ≃ B) (y : B) → linv f y ≡ rinv f y
linv-is-rinv f y = sym (trans (sym (isLinv f (rinv f y))) (cong (linv f) (isRinv f y)))