I see. FYI: with Univalence, we solve this issue in HoTT-Agda by
establishing an equivalence like this:
https://github.com/HoTT/HoTT-Agda/blob/e48a16bcd719e2fcb409d79e3f7df6c6b81223bb/core/lib/types/Pi.agda#L24-L29

As we all know, univalence is a general principle to internalize these
identifications. Perhaps special cases can be done in other ways.

Best,
Favonia

On Tue, Jun 26, 2018 at 4:00 PM Martín Hötzel Escardó <
escardo.martin@gmail.com> wrote:

> Thanks, Favonia. Meanwhile I solved this as in the following commit (file
> source/UF-Subsingletons-FunExt.lagda
> <https://github.com/martinescardo/TypeTopology/commit/7433e08de497216cbe131727c4a367eaed85847e#diff-562e7978f09d797d06b9bc40fc2e0c0e>
> ),
> 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.
>>>
>> --
> 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.