{-# OPTIONS --without-K #-}
module segal.preliminaries where

open import equality
open import hott.level
open import function.isomorphism
open import function.extensionality
open import function.fibration
open import level
open import sum

module _ {i} {A : Set i} where
  private
    Singleton : Set (lsuc i)
    Singleton = Σ (A → Set i) λ P → contr (Σ A P)

    f : A → Singleton
    f a = ((λ b → a ≡ b), singl-contr a)

    g : Singleton → A
    g (_ , (a , _) , _) = a

    α : (a : A) → g (f a) ≡ a
    α a = refl

    β : (s : Singleton) → f (g s) ≡ s
    β (P , (x , p) , h) = unapΣ (lem , h1⇒prop (hn-h1  _) _ _)
      where
        t-iso : singleton x ≅ Σ A P
        t-iso = contr-⊤-iso (singl-contr x)
              ·≅ sym≅ (contr-⊤-iso ((x , p), h))

        t-iso-β : (b : A)(p : x ≡ b) → proj₁ (apply≅ t-iso (b , p)) ≡ b
        t-iso-β .x refl = refl

        lem : (λ b → x ≡ b) ≡ P
        lem = funext λ b → ≅⇒≡ (family-eq-iso t-iso t-iso-β b)

  contr-predicate : Singleton ≅ A
  contr-predicate = iso g f β α

  contr-predicate-η : (a : A) → proj₁ (invert≅ contr-predicate a) ≡ (λ b → a ≡ b)
  contr-predicate-η a = refl

  add-contr : {B : A → Set i}
            → ((a : A) → contr (B a))
            → A ≅ Σ A B
  add-contr {B = B} hB = sym≅ (  Σ-ap-iso₂ (λ a → contr-⊤-iso (hB a))
                              ·≅ ×-right-unit)

module _ {i} {A B : Set i} where
  iso-adjunct : {a : A}{b : B}(φ : A ≅ B)
              → apply≅ φ a ≡ b
              → a ≡ invert≅ φ b
  iso-adjunct {a} φ p = sym (_≅_.iso₁ φ a) · ap (invert≅ φ) p