[HoTT] Agda formalization question

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

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