{-# OPTIONS --without-K #-}
module function.isomorphism.core where

open import level using (_⊔_)
open import equality.core
open import equality.groupoid
open import equality.reasoning
open import function.core
open import sum
open import function.extensionality.core

-- isomorphisms
record _≅_ {i j}(X : Set i)(Y : Set j) : Set (i ⊔ j) where
  constructor iso
  field
    to : X → Y
    from : Y → X
    iso₁ : (x : X) → from (to x) ≡ x
    iso₂ : (y : Y) → to (from y) ≡ y

refl≅ : ∀ {i}{X : Set i} → X ≅ X
refl≅ = iso id id (λ _ → refl) (λ _ → refl)

≡⇒≅ : ∀ {i}{X Y : Set i} → X ≡ Y → X ≅ Y
≡⇒≅ refl = refl≅

sym≅ : ∀ {i j}{X : Set i}{Y : Set j} → X ≅ Y → Y ≅ X
sym≅ (iso f g H K) = iso g f K H

trans≅ : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
       → X ≅ Y → Y ≅ Z → X ≅ Z
trans≅ (iso f g H K) (iso f' g' H' K') = record
  { to = f' ∘ f
  ; from = g ∘ g'
  ; iso₁ = λ x → cong g (H' (f x)) ⊚ H x
  ; iso₂ = λ y → cong f' (K (g' y)) ⊚ K' y }

module ≅-Reasoning where
  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≅⟨_⟩_
  infixr 2 _≡⟨_⟩_
  infix  1 begin_

  data _IsRelatedTo_ {i j}(x : Set i)(y : Set j) : Set (i ⊔ j) where
    relTo : x ≅ y → x IsRelatedTo y

  begin_ : ∀ {i j}{X : Set i}{Y : Set j} → X IsRelatedTo Y → X ≅ Y
  begin relTo p = p

  _≅⟨_⟩_ : ∀ {i j k} (X : Set i) {Y : Set j}{Z : Set k}
         → X ≅ Y → Y IsRelatedTo Z → X IsRelatedTo Z
  _ ≅⟨ p ⟩ relTo q = relTo (trans≅ p q)

  _≡⟨_⟩_ : ∀ {i j} (X : Set i) {Y : Set i} {Z : Set j}
         → X ≡ Y → Y IsRelatedTo Z → X IsRelatedTo Z
  _ ≡⟨ p ⟩ relTo q = relTo (trans≅ (≡⇒≅ p) q)

  _∎ : ∀ {i} (X : Set i) → X IsRelatedTo X
  _∎ _ = relTo refl≅

private
  module Dummy {i j}{X : Set i}{Y : Set j} where
      injective : (f : X → Y) → Set _
      injective f = (x x' : _) → f x ≡ f x' → x ≡ x'

      surjective : (f : X → Y) → Set _
      surjective f = (y : Y) → Σ X λ x → f x ≡ y

      open _≅_ public using ()
        renaming (to to apply ; from to invert)

      iso⇒inj : (iso : X ≅ Y) → injective (apply iso)
      iso⇒inj f x x' q = (iso₁ x) ⁻¹ ⊚ cong from q ⊚ iso₁ x'
        where
          open _≅_ f

      iso⇒surj : (iso : X ≅ Y) → surjective (apply iso)
      iso⇒surj f y = from y , iso₂ y
        where
          open _≅_ f

      inj+surj⇒iso : (f : X → Y) → injective f → surjective f → X ≅ Y
      inj+surj⇒iso f inj-f surj-f = iso f g H K
        where
          g : Y → X
          g y = proj₁ (surj-f y)

          H : (x : X) → g (f x) ≡ x
          H x = inj-f (g (f x)) x (proj₂ (surj-f (f x)))

          K : (y : Y) → f (g y) ≡ y
          K y = proj₂ (surj-f y)
open Dummy public

_↣_ : (A B : Set) → Set
A ↣ B = Σ (A → B) injective

_∘i_ : {A B C : Set} → (B ↣ C) → (A ↣ B) → (A ↣ C) -- composition of injections:
(g , p) ∘i (f , q) = g ∘ f , r
   where
     r : (x x' : _) → g (f x) ≡ g (f x') → x ≡ x'
     r x x' s = q x x' (p (f x) (f x') s)

_↠_ : (A B : Set) → Set
A ↠ B = Σ (A → B) surjective