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

open import equality
open import hott.equivalence
open import sum

open import segal.composition
open import segal.identities

module _ {i} (W : Wild₃ i) where
  open WildOps₃ W
  module _ (Wid : HasId₂ W|2) where
    open HasId₂ Wid

    LInv : {x y : obj 𝓒} → hom 𝓒 x y → Set i
    LInv {x}{y} f = Σ (hom 𝓒 y x) λ g → g ∘ f ≡ id x

    RInv : {x y : obj 𝓒} → hom 𝓒 x y → Set i
    RInv {x}{y} f = Σ (hom 𝓒 y x) λ g → f ∘ g ≡ id y

    IsIso : {x y : obj 𝓒} → hom 𝓒 x y → Set i
    IsIso f = LInv f × RInv f

    Iso : obj 𝓒 → obj 𝓒 → Set i
    Iso x y = Σ (hom 𝓒 x y) IsIso

    id-equiv : (x : obj 𝓒) → Iso x x
    id-equiv x = id x , (id x , id-λ _ _ (id x))
                      , (id x , id-λ _ _ (id x))

    id-to-iso : (x y : obj 𝓒)
              → (x ≡ y)
              → Iso x y
    id-to-iso x .x refl = id-equiv x

    IsUnivalent : Set i
    IsUnivalent = (x y : obj 𝓒) → weak-equiv (id-to-iso x y)