# Isomorphisms of sets

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-08.

module foundation.isomorphisms-of-sets where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.sets
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.subtypes


## Idea

Since equality of elements in a set is a proposition, isomorphisms of sets are equivalent to equivalences of sets

module _
{l1 l2 : Level} (A : Set l1) (B : Set l2)
where

is-iso-Set : (f : hom-Set A B) → UU (l1 ⊔ l2)
is-iso-Set f = Σ (hom-Set B A) (λ g → ((f ∘ g) ＝ id) × ((g ∘ f) ＝ id))

iso-Set : UU (l1 ⊔ l2)
iso-Set = Σ (hom-Set A B) is-iso-Set

map-iso-Set : iso-Set → type-Set A → type-Set B
map-iso-Set = pr1

is-iso-map-iso-Set : (f : iso-Set) → is-iso-Set (map-iso-Set f)
is-iso-map-iso-Set = pr2

is-proof-irrelevant-is-iso-Set :
(f : hom-Set A B) → is-proof-irrelevant (is-iso-Set f)
pr1 (is-proof-irrelevant-is-iso-Set f H) = H
pr2 (is-proof-irrelevant-is-iso-Set f (g , p , q)) (g' , p' , q') =
eq-type-subtype
( λ h →
product-Prop
( Id-Prop (hom-set-Set B B) (f ∘ h) id)
( Id-Prop (hom-set-Set A A) (h ∘ f) id))
( ( ap (λ h → g ∘ h) (inv p')) ∙
( ap (λ h → h ∘ g') q))

is-prop-is-iso-Set : (f : hom-Set A B) → is-prop (is-iso-Set f)
is-prop-is-iso-Set f =
is-prop-is-proof-irrelevant (is-proof-irrelevant-is-iso-Set f)

is-iso-is-equiv-Set : {f : hom-Set A B} → is-equiv f → is-iso-Set f
pr1 (is-iso-is-equiv-Set H) = map-inv-is-equiv H
pr1 (pr2 (is-iso-is-equiv-Set H)) = eq-htpy (is-section-map-inv-is-equiv H)
pr2 (pr2 (is-iso-is-equiv-Set H)) = eq-htpy (is-retraction-map-inv-is-equiv H)

is-equiv-is-iso-Set : {f : hom-Set A B} → is-iso-Set f → is-equiv f
is-equiv-is-iso-Set H =
is-equiv-is-invertible
( pr1 H)
( htpy-eq (pr1 (pr2 H)))
( htpy-eq (pr2 (pr2 H)))

iso-equiv-Set : equiv-Set A B → iso-Set
pr1 (iso-equiv-Set e) = map-equiv e
pr2 (iso-equiv-Set e) = is-iso-is-equiv-Set (is-equiv-map-equiv e)

equiv-iso-Set : iso-Set → equiv-Set A B
pr1 (equiv-iso-Set f) = map-iso-Set f
pr2 (equiv-iso-Set f) = is-equiv-is-iso-Set (is-iso-map-iso-Set f)

equiv-iso-equiv-Set : equiv-Set A B ≃ iso-Set
equiv-iso-equiv-Set =
equiv-type-subtype
( is-property-is-equiv)
( is-prop-is-iso-Set)
( λ f → is-iso-is-equiv-Set)
( λ f → is-equiv-is-iso-Set)