This is really an Agda question, but because it involves HoTT concepts, and because there are several Agda formalizers here, I prefer to ask it here rather than in the Agda mailing list.
Forgive me is the question has a simple answer.
Consider the following constructions:
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}
is-prop-is-set' : ∀ {U} {X : U ̇} → funext U U → is-prop (is-set' X)
is-prop-is-set' fe = is-prop-exponential-ideal fe
(λ x → is-prop-exponential-ideal fe
(λ y → is-prop-is-prop fe))
Now I am not able to prove that
is-prop-is-set : ∀ {U} {X : U ̇} → funext U U → is-prop (is-set X)
The reason is that funext has explicit parameters, and I don't seem to be able to get funext with implicit parameters from funext with explicit parameters. Am I missing something obvious?
(I am tempted to make is-set' the official version and ditch is-set, but this will involve major rewriting of the Agda code.)
Martin