Contr.agda

module Contr where

open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality

is-contr : ∀ {a} (A : Set a) → Set _
is-contr A = Σ A λ a → ∀ x → a ≡ x

infix  5 _~_

_~_ : ∀ {a b} {A : Set a} {B : A → Set b}
  (f g : ∀ a → B a) → Set _
f ~ g = ∀ x → f x ≡ g x

is-equiv : ∀ {a b} {A : Set a} {B : Set b}
  (f : A → B) → Set _
is-equiv {A = A} {B = B} f
  = (Σ (B → A) λ g → f ∘ g ~ id)
  × (Σ (B → A) λ h → h ∘ f ~ id)

_≃_ : ∀ {a b} (A : Set a) (B : Set b) → Set _
A ≃ B = Σ (A → B) is-equiv

contr-≃⊤ : ∀ {a} {A : Set a} → is-contr A → A ≃ ⊤
contr-≃⊤ (a , p)
  = (λ _ → _)
  , ((λ _ → a) , (λ _ → refl))
  , ((λ _ → a) , p)

iso : ∀ {a b} (A : Set a) (B : Set b) → Set _
iso A B
  = Σ (A → B) λ f
  → Σ (B → A) λ g
  → f ∘ g ~ id × g ∘ f ~ id

iso→≃ : ∀ {a b} {A : Set a} {B : Set b} →
  iso A B → A ≃ B
iso→≃ (f , g , α , β) = f , (g , α) , (g , β)

≃→iso : ∀ {a b} {A : Set a} {B : Set b} →
  A ≃ B → iso A B
≃→iso (f , (g , α) , (h , β))
  = f
  , h ∘ f ∘ g
  , (λ x → trans (cong f (β (g x))) (α x))
  , (λ x → trans (cong h (α (f x))) (β x))