module Prelude where

open import Level
open import Function using (id; _∘_)
open import Data.Unit using (⊤; tt)
open import Data.Product using (Σ; _,_; proj₁; proj₂; _×_) renaming (map to _**_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂; trans)


--------
-- unit type is terminal

! : ∀ {a} {A : Set a} → A → ⊤
! _ = tt


--------
-- uniqueness of identity proofs

UIP : ∀ {a} {A : Set a} {x y : A} {eq eq' : x ≡ y} → eq ≡ eq'
UIP {eq = refl} {refl} = refl


--------
-- sigma types

cong-proj₂ : ∀ {a b} {A : Set a} {B : A → Set b} {x : A} {y y' : B x} → (_,_ {B = B} x y) ≡ (x , y') → y ≡ y'
cong-proj₂ refl = refl

--------
-- isomorphisms

record Iso (A : Set) (B : Set) : Set where
  field
    to   : A → B
    from : B → A
    to-from-inverse : ∀ {y} → to (from y) ≡ y
    from-to-inverse : ∀ {x} → from (to x) ≡ x

idIso : ∀ {A} → Iso A A
idIso = record { to   = id
               ; from = id
               ; to-from-inverse = refl
               ; from-to-inverse = refl }

symIso : ∀ {A B} → Iso A B → Iso B A
symIso ab =
  record { to   = Iso.from ab
         ; from = Iso.to ab
         ; to-from-inverse = Iso.from-to-inverse ab
         ; from-to-inverse = Iso.to-from-inverse ab }

transIso : ∀ {A B C} → Iso A B → Iso B C → Iso A C
transIso ab bc =
  record { to   = Iso.to bc ∘ Iso.to ab
         ; from = Iso.from ab ∘ Iso.from bc
         ; to-from-inverse = trans (cong (Iso.to bc) (Iso.to-from-inverse ab)) (Iso.to-from-inverse bc)
         ; from-to-inverse = trans (cong (Iso.from ab) (Iso.from-to-inverse bc)) (Iso.from-to-inverse ab) }

prodIso : ∀ {A B C D} → Iso A B → Iso C D → Iso (A × C) (B × D)
prodIso ab cd =
  record { to   = Iso.to ab ** Iso.to cd
         ; from = Iso.from ab ** Iso.from cd
         ; to-from-inverse = cong₂ _,_ (Iso.to-from-inverse ab) (Iso.to-from-inverse cd)
         ; from-to-inverse = cong₂ _,_ (Iso.from-to-inverse ab) (Iso.from-to-inverse cd) }

toIso : ∀ {A B} → (f : A → B) → (∀ x x' → f x ≡ f x' → x ≡ x') → (g : (y : B) → Σ[ x ∶ A ] f x ≡ y) → Iso A B
toIso f f-inj g =
  record { to   = f
         ; from = proj₁ ∘ g
         ; to-from-inverse = λ {y} → proj₂ (g y)
         ; from-to-inverse = λ {x} → f-inj (proj₁ (g (f x))) x (proj₂ (g (f x))) }


--------
-- inverse images

data _⁻¹_ {A B : Set} (f : A → B) : B → Set where
  ok : (x : A) → f ⁻¹ (f x)

und : ∀ {A B} {f : A → B} {y} → f ⁻¹ y → A
und (ok x) = x

from≡ : ∀ {A B} {f : A → B} {x y} → f x ≡ y → f ⁻¹ y
from≡ {x = x} refl = ok x

to≡ : ∀ {A B} {f : A → B} {y} → (x : f ⁻¹ y) → f (und x) ≡ y
to≡ (ok x) = refl


--------
-- pullbacks

data _⋈_ {A B C : Set} (f : A → C) (g : B → C) : Set where
  _,_ : {c : C} → f ⁻¹ c → g ⁻¹ c → f ⋈ g

infixr  _,_

pull : {A B C : Set} {f : A → C} {g : B → C} → f ⋈ g → C
pull (_,_ {c} _ _) = c

π₁ : {A B C : Set} {f : A → C} {g : B → C} → f ⋈ g → A
π₁ (a , _) = und a

π₂ : {A B C : Set} {f : A → C} {g : B → C} → f ⋈ g → B
π₂ (_ , b) = und b