module Preliminaries where

infix  _≡_
data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

open _≡_ public

data ⊥ : Set where

infixr  _+_
data _+_ (A : Set) (B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

open _+_ public

record ⊤ : Set where
  constructor tt

open ⊤ public

infixr  _,_

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

open Σ public

infix  _≅_
record _≅_ (A B : Set) : Set where
  field
    fun : A → B
    inv : B → A
    inv-fun : (a : A) → inv (fun a) ≡ a
    fun-inv : (b : B) → fun (inv b) ≡ b

open _≅_ public

postulate
  funext : {A : Set} {B : A → Set} {f g : (a : A) → B a} → ((a : A) → f a ≡ g a) → f ≡ g

infixr  _•_
_•_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
refl • refl = refl

symm : {A : Set} {a b : A} → a ≡ b → b ≡ a
symm refl = refl

ap : {A B : Set} {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
ap f refl = refl

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

-- To avoid parentheses in long function applications.
infixr  _$_
_$_ : {A : Set} {B : A → Set} (f : (a : A) → B a) (a : A) → B a
f $ a = f a

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
(g ∘ f) a = g (f a)

infixr  _∘ₑ_
_∘ₑ_ : {A B C : Set} → B ≅ C → A ≅ B → A ≅ C
(g ∘ₑ f) .fun a = g .fun (f .fun a)
(g ∘ₑ f) .inv c = f .inv (g .inv c)
(g ∘ₑ f) .inv-fun a = ap (f .inv) (g .inv-fun _) • f .inv-fun _
(g ∘ₑ f) .fun-inv c = ap (g .fun) (f .fun-inv _) • g .fun-inv _

+-ind : {A B : Set} {P : A + B → Set} → ((a : A) → P (inl a)) → ((b : B) → P (inr b)) →
        (x : A + B) → P x
+-ind pa pb (inl a) = pa a
+-ind pa pb (inr b) = pb b

+-rec : {A B C : Set} → (A → C) → (B → C) → A + B → C
+-rec = +-ind

+-symm : {A B : Set} → A + B ≅ B + A
+-symm .fun = +-rec inr inl
+-symm .inv = +-rec inr inl
+-symm .inv-fun = +-ind (λ a → refl) (λ b → refl)
+-symm .fun-inv = +-ind (λ b → refl) (λ a → refl)

+-assoc : {A B C : Set} → A + B + C ≅ (A + B) + C
+-assoc .fun = +-rec (inl ∘ inl) (+-rec (inl ∘ inr) inr)
+-assoc .inv = +-rec (+-rec inl (inr ∘ inl)) (inr ∘ inr)
+-assoc .inv-fun = +-ind (λ a → refl) (+-ind (λ b → refl) λ c → refl)
+-assoc .fun-inv = +-ind (+-ind (λ a → refl) (λ b → refl)) λ c → refl

+-map : {A B X Y : Set} → (A → X) → (B → Y) → A + B → X + Y
+-map f g = +-rec (inl ∘ f) (inr ∘ g)

+-congr : {A B X Y : Set} → A ≅ X → B ≅ Y → A + B ≅ X + Y
+-congr f g .fun = +-map (f .fun) (g .fun)
+-congr f g .inv = +-map (f .inv) (g .inv)
+-congr f g .inv-fun = +-ind (λ a → ap inl (f .inv-fun a)) (λ b → ap inr (g .inv-fun b))
+-congr f g .fun-inv = +-ind (λ a → ap inl (f .fun-inv a)) (λ b → ap inr (g .fun-inv b))

id-iso : {A : Set} → A ≅ A
id-iso .fun a = a
id-iso .inv a = a
id-iso .inv-fun a = refl
id-iso .fun-inv a = refl

inv-iso : {A B : Set} → A ≅ B → B ≅ A
inv-iso f .fun = f .inv
inv-iso f .inv = f .fun
inv-iso f .inv-fun = f .fun-inv
inv-iso f .fun-inv = f .inv-fun

symm-iso : {A : Set} {x y : A} → x ≡ y ≅ y ≡ x
symm-iso .fun = symm
symm-iso .inv = symm
symm-iso .inv-fun refl = refl
symm-iso .fun-inv refl = refl

transport-iso : {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x ≅ P y
transport-iso _ refl = id-iso

eq-congr : {A : Set} {a b x y : A} → a ≡ x → b ≡ y → a ≡ b ≅ x ≡ y
eq-congr refl refl = id-iso

eq-congr-refl : {A : Set} {a x : A} (p : a ≡ x) → eq-congr p p .fun refl ≡ refl
eq-congr-refl refl = refl

fib : {A B : Set} (f : A → B) → B → Set
fib {A = A} f b = Σ A (λ a → f a ≡ b)

isContr : Set → Set
isContr A = Σ A (λ a → (b : A) → a ≡ b)

refl-comp : {A : Set} {a b : A} (p : a ≡ b) → refl • p ≡ p
refl-comp refl = refl

comp-refl : {A : Set} {a b : A} (p : a ≡ b) → p • refl ≡ p
comp-refl refl = refl

ap-nat : {A B : Set} {f g : A → B} (h : (a : A) → f a ≡ g a) {a b : A} (p : a ≡ b) →
         ap f p • h b ≡ h a • ap g p
ap-nat h refl = refl-comp _ • symm (comp-refl _)

eq-symm-comp-of-comp-eq : {A : Set} {a b c : A}
                         (ab : a ≡ b) (bc : b ≡ c) (ac : a ≡ c) →
                         ab • bc ≡ ac → bc ≡ symm ab • ac
eq-symm-comp-of-comp-eq  refl refl p h = h • symm (refl-comp _)

ap-id : {A : Set} {a b : A} (p : a ≡ b) → ap (λ x → x) p ≡ p
ap-id refl = refl

ap-circ : {A B C : Set} {f : A → B} {g : B → C} {a b : A} (p : a ≡ b) → ap g (ap f p) ≡ ap (g ∘ f) p
ap-circ refl = refl

comp-congr : {A : Set} {a b c : A} {p p' : a ≡ b} {q q' : b ≡ c} → p ≡ p' → q ≡ q' → p • q ≡ p' • q'
comp-congr refl refl = refl

postcomp-inj : {A : Set} {a b c : A} {p p' : a ≡ b} (q : b ≡ c) →
               p • q ≡ p' • q → p ≡ p'
postcomp-inj refl h = symm (comp-refl _ ) • h • comp-refl _

endo-comm : {A : Set} {f : A → A} (h : (a : A) → f a ≡ a) (a : A) →
            h (f a) ≡ ap f (h a)
endo-comm h a = postcomp-inj (h a) (symm (ap-nat h (h a) • comp-congr refl (ap-id _)))

isProp : Set → Set
isProp A = (a b : A) → a ≡ b

isProp-of-isContr : {A : Set} → isContr A → isProp A
isProp-of-isContr A-contr a b = symm (A-contr .snd _) • A-contr .snd _

contr-of-prop : {A : Set} → isProp A → A → isContr A
contr-of-prop A-prop a = (a , A-prop a)

transport-refl : {A : Set} {P : A → Set} {a : A} {q : a ≡ a} {p : P a} →
                 q ≡ refl → transport P p q ≡ p
transport-refl refl = refl

module _ {A : Set} (A-contr : isContr A) (P : A → Set) (p : P (A-contr .fst)) where
  abstract
    contr-ind : (a : A) → P a
    contr-ind a = transport P p (isProp-of-isContr A-contr _ _)

    contr-ind-centre : contr-ind (A-contr .fst) ≡ p
    contr-ind-centre = transport-refl {p = p} (symm (eq-symm-comp-of-comp-eq _ _ _ (comp-refl _)))

congrFun : {A : Set} {B : A → Set} {f g : (a : A) → B a} → f ≡ g → (a : A) → f a ≡ g a
congrFun refl _ = refl

Σ-congr-snd : {A : Set} {X Y : A → Set} (e : (a : A) → X a ≅ Y a) → Σ A X ≅ Σ A Y
Σ-congr-snd e .fun t = t .fst , e (t .fst) .fun (t .snd)
Σ-congr-snd e .inv t = t .fst , e (t .fst) .inv (t .snd)
Σ-congr-snd e .inv-fun t = ap (t .fst ,_) (e (t .fst) .inv-fun (t .snd))
Σ-congr-snd e .fun-inv t = ap (t .fst ,_) (e (t .fst) .fun-inv (t .snd))

uncurry : {A : Set} {B : A → Set} {C : Σ A B → Set} → (c : (a : A) → (b : B a) → C (a , b)) →
          (t : Σ A B) → C t
uncurry c t = c (t .fst) (t .snd)

⊥-prop : isProp ⊥
⊥-prop ()

⊤-prop : isProp ⊤
⊤-prop tt tt = refl

exfalso : {A : Set} → ⊥ → A
exfalso ()

+-prop : {A B : Set} → isProp A → isProp B → (A → B → ⊥) → isProp (A + B)
+-prop A-prop B-prop disj (inl a) (inl a') = ap inl (A-prop _ _)
+-prop A-prop B-prop disj (inl a) (inr b') = exfalso (disj a b')
+-prop A-prop B-prop disj (inr b) (inl a') = exfalso (disj a' b)
+-prop A-prop B-prop disj (inr b) (inr b') = ap inr (B-prop _ _)

prop-iso : {A B : Set} → isProp A → isProp B → (A → B) → (B → A) → A ≅ B
prop-iso A-prop B-prop f g .fun = f
prop-iso A-prop B-prop f g .inv = g
prop-iso A-prop B-prop f g .inv-fun a = A-prop _ _
prop-iso A-prop B-prop f g .fun-inv b = B-prop _ _

+-distrib : {A : Set} {X Y : A → Set} → (Σ A X) + (Σ A Y) ≅ Σ A (λ a → X a + Y a)
+-distrib .fun (inl t) = t .fst , inl (t .snd)
+-distrib .fun (inr t) = t .fst , inr (t .snd)
+-distrib .inv (a , inl x) = inl (a , x)
+-distrib .inv (a , inr y) = inr (a , y)
+-distrib .inv-fun (inl t) = refl
+-distrib .inv-fun (inr t) = refl
+-distrib .fun-inv (a , inl x) = refl
+-distrib .fun-inv (a , inr y) = refl

ap-inr-iso : {A B : Set} {x y : B} → x ≡ y ≅ inr {A = A} x ≡ inr y
ap-inr-iso .fun = ap inr
ap-inr-iso .inv refl = refl
ap-inr-iso .inv-fun refl = refl
ap-inr-iso .fun-inv refl = refl 

Σ-contr : {A : Set} {X : A → Set} → ((a : A) → isContr (X a)) →
          Σ A X ≅ A
Σ-contr X-contr .fun = fst
Σ-contr X-contr .inv a = a , X-contr a .fst 
Σ-contr X-contr .inv-fun = uncurry λ a → contr-ind (X-contr a) _ refl
Σ-contr X-contr .fun-inv a = refl

×-symm : {A B : Set} → Σ A (λ _ → B) ≅ Σ B (λ _ → A)
×-symm .fun p = p .snd , p .fst
×-symm .inv p = p .snd , p .fst
×-symm .inv-fun p = refl
×-symm .fun-inv p = refl

contr-singleton : {A : Set} (a : A) → isContr (Σ A (λ a' → a' ≡ a))
contr-singleton a .fst = (a , refl)
contr-singleton a .snd (_ , refl) = refl

contr-congr : {A B : Set} (f : A ≅ B) → isContr A → isContr B
contr-congr f A-contr = contr-of-prop
  (λ b b' → symm (f .fun-inv b) •
    ap (f .fun) (isProp-of-isContr A-contr _ _) • f .fun-inv b')
    (f .fun (A-contr .fst))