open import Agda.Primitive
_* : ∀ U → Set (lsuc U)
U * = Set U
data _≡_ {U} {X : U *} (x : X) : X → U * where
refl : x ≡ x
is-prop : ∀ {U} → U * → U *
is-prop X = (x y : X) → x ≡ y
is-set : ∀ {U} → U * → U *
is-set X = {x y : X} → is-prop (x ≡ y)
is-set' : ∀ {U} → U * → U *
is-set' X = (x y : X) → is-prop (x ≡ y)
is-set'-is-set : ∀ {U} {X : U *} → is-set' X → is-set X
is-set'-is-set s {x} {y} = s x y
is-set-is-set' : ∀ {U} {X : U *} → is-set X → is-set' X
is-set-is-set' s x y = s {x} {y}
funext : ∀ U0 U1 → lsuc (U0 ⊔ U1) *
funext U0 U1 = {X : U0 *} {Y : X → U1 *} (f g : (x : X) → Y x) → (∀ x → f x ≡ g x) → f ≡ g
postulate
is-prop-is-set' : ∀ {U} {X : U *} → funext U U → is-prop (is-set' X)
ap : ∀ {U0 U1} {X : U0 *} {Y : U1 *} (f : X → Y) {x y : X} → x ≡ y → f x ≡ f y
ap f refl = refl
is-prop-is-set : ∀ {U} {X : U *} → funext U U → is-prop (is-set X)
is-prop-is-set fe isset0 isset1 =
ap is-set'-is-set (is-prop-is-set' fe (is-set-is-set' isset0) (is-set-is-set' isset1))
Best,
Favonia