{-# OPTIONS --safe #-}

module DepthComonads.Stable where

open import DepthComonads.Empty
open import DepthComonads.Level
open import DepthComonads.Path
open import DepthComonads.HLevels

Stable : Type a  Type a
Stable A = ¬ ¬ A  A

Stable≡→isSet :  {} {A : Type }  (st :  (a b : A)  Stable (a  b))  isSet A
Stable≡→isSet {A = A} st a b p q j i =
  let f : (x : A)  a  x  a  x
      f x p = st a x  h  h p)
      fIsConst : (x : A)  (p q : a  x)  f x p  f x q
      fIsConst = λ x p q i  st a x (isProp¬  h  h p)  h  h q) i)
      rem : (p : a  b)  PathP  i  a  p i) (f a refl) (f b p)
      rem p j = f (p j)  i  p (i  j))
  in hcomp  k  λ { (i = i0)  f a refl k
                    ; (i = i1)  fIsConst b p q j k
                    ; (j = i0)  rem p i k
                    ; (j = i1)  rem q i k }) a