Thanks, Favonia. Meanwhile I solved this as in the following commit (file  source/UF-Subsingletons-FunExt.lagda), https://github.com/martinescardo/TypeTopology/commit/7433e08de497216cbe131727c4a367eaed85847e, which may be similar to what you are saying. However, the problem with such a solution is that it has to be specialized to each situation where we have inputs defined with some ex/implicit arguments which we want to apply to a function defined with some other ex/implicit arguments. In my view, a definition with implicit arguments should be considered to be the same as the definition with explicit arguments, as in real-life informal mathematics. Best, Martin  

On Tuesday, 26 June 2018 20:16:06 UTC+1, Favonia wrote:

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...@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.