Hi Martin,

I don't know your definition of is-prop, but how about this?

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

On Wed, Jun 20, 2018 at 3:46 PM Martín Hötzel Escardó <
escardo.martin@gmail.com> wrote:

> Bad copy and paste. Let me fix this.
>
>
> 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)
>
> Martin
>
>>
>> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.