Re: [HoTT] Re: Agda formalization question

["Martín Hötzel Escardó" <escardo.martin@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 3216 bytes --]

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 <javascript:>> 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 <javascript:>.
>> 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.

[-- Attachment #1.2: Type: text/html, Size: 5901 bytes --]