Lemma1.17.agda

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

open import Agda.Builtin.Equality

_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c}
    → (f : {x : A} (y : B x) → C y) (g : (x : A) → B x)
    → (x : A) → C (g x)
(f ∘ g) x = f (g x)

_⁻¹ : {A : Set} {x y : A} → x ≡ y → y ≡ x
refl ⁻¹ = refl

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

·⁻¹ : {A : Set} {x y : A} (e : x ≡ y) → (e ⁻¹) · e ≡ refl
·⁻¹ refl = refl

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

subst : {A : Set} (P : A → Set) {x y : A}
      → x ≡ y → P x → P y
subst P refl p = p

subst· : {A : Set} (P : A → Set) {x y z : A} (e₁ : x ≡ y) (e₂ : y ≡ z)
            → (p : P x) → subst P e₂ (subst P e₁ p) ≡ subst P (e₁ · e₂) p
subst· P refl refl p = refl

subst-cong : {A B : Set} (P : B → Set) (f : A → B) {x y : A} (e : x ≡ y)
           → (p : P (f x)) → subst (P ∘ f) e p ≡ subst P (cong f e) p
subst-cong P f refl p = refl

cong₂ : {A : Set} {B : A → Set} {C : Set} (f : (x : A) → B x → C)
      → {x₁ y₁ : A} (e₁ : x₁ ≡ y₁) {x₂ : B x₁} {y₂ : B y₁} (e₂ : subst B e₁ x₂ ≡ y₂)
      → f x₁ x₂ ≡ f y₁ y₂
cong₂ f refl refl = refl

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

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 _≃_

linv-is-rinv : {A B : Set} (f : A ≃ B) {y : B} → linv f y ≡ rinv f y
linv-is-rinv f {y = y} = (cong (linv f) (isRinv f y ⁻¹)) · isLinv f (rinv f y)