[HoTT] Agda formalization question

[HoTT] Agda formalization question

[Martín Hötzel Escardó]

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

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

-- 
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: 2304 bytes --]

[HoTT] Re: Agda formalization question

[Martín Hötzel Escardó]

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

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.

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

Re: [HoTT] Re: Agda formalization question

[Favonia]

[-- Attachment #1: Type: text/plain, Size: 2194 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 4322 bytes --]

Re: [HoTT] Re: Agda formalization question

[Martín Hötzel Escardó]

[-- 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 --]

Re: [HoTT] Re: Agda formalization question

[Favonia]

[-- Attachment #1: Type: text/plain, Size: 4067 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 7073 bytes --]