[HoTT-reading-group] Agda, funext and implicits

[Jason Gross]

The problem is that Agda tries to automatically insert the remaining
implicit arguments for you.  So your x, y, and z have the wrong type to be
passed to ∙=∙'₁.  Note that if you replace the definition of ∙=∙'₂ with a
hole, the type is colored yellow, indicating that Agda couldn't figure out
all of the arguments for you, and the type is incomplete.  I don't know of
any good way to unimplicit a function, but manually eta expanding seems to
work fine:

  ∙=∙'₂ : (λ x y z → _∙_ {i = i} {A = A} {x = x} {y = y} {z = z}) == (λ x y
z → _∙'_ {i = i} {A = A} {x = x} {y = y} {z = z})
  ∙=∙'₂ = λ= (λ x → λ= (λ y → λ= (λ z → ∙=∙'₁ x y z)))


-Jason



On Wed, Jan 29, 2014 at 9:58 PM, Chris Jeris <cjeris at gmail.com> wrote:

> I was trying to work Exercise 2.1 in Agda and ran into some trouble
> applying functional extensionality in the presence of implicit arguments.
>  In the below code, if I redefine path composition to require the arguments
> x, y, z explicitly, the proof that the composition operators are equal (as
> dependent functions of x, y, z, p, q) goes through without trouble.  But
> with the standard (implicit in everything except the path arguments)
> definitions, I get the error indicated below, and I don't see why.
>  (Refining on holes doesn't work because the type checker will never guess
> I want to apply extensionality at an implicit argument.)
>
> The problem is not caused by the fact that the proofs live in a module
> with parameter A which is distinct from the module in PathGroupoid where
> composition is initially defined; I tried adding duplicate definitions into
> my own module and got the same problem.
>
> Can anyone help?
>
> thanks, C
>
> {-# OPTIONS --without-K #-}
> module Exercises.Exercises2 where
>
> open import HoTT public
>
> -- 2.1. Show that the three obvious proofs of Lemma 2.1.2 are pairwise
> equal.
>
> -- From PathGroupoid:
>
> -- _∙_ : {x y z : A}
> --   → (x == y → y == z → x == z)
> -- idp ∙ q = q
>
> -- _∙'_ : {x y z : A}
> --   → (x == y → y == z → x == z)
> -- q ∙' idp = q
>
> -- ∙=∙' : {x y z : A} (p : x == y) (q : y == z)
> --   → p ∙ q == p ∙' q
> -- ∙=∙' idp idp = idp
>
> module _ {i} {A : Type i} where
>
>   -- ! are the versions with explicit x y z arguments
>   ∙! : (x y z : A) → x == y → y == z → x == z
>   ∙! x .x z idp q = q
>
>   ∙′! : (x y z : A) → x == y → y == z → x == z
>   ∙′! x y .y p idp = p
>
>   -- The proof that any particular instances of the compositions are equal
> is a trivial path
>   -- induction, but to prove the operators themselves are equal we require
> extensionality.
>   ∙=∙'₁ : (x y z : A) → _∙_ {x = x} {y = y} {z = z} == _∙'_ {x = x} {y =
> y} {z = z}
>   ∙=∙'₁ x y z = λ= (λ p → λ= (λ q → ∙=∙' p q))
>
>   ∙=∙'₂ : _∙_ {i = i} {A = A} == _∙'_ {i = i} {A = A}
> *-- _x_75 == _y_76 != A of type Set i*
> *-- when checking that the expression*
> *-- λ= (λ x → λ= (λ y → λ= (λ z → ∙=∙'₁ x y z))) has type _∙_ == _∙'_*
>   ∙=∙'₂ = *λ= (λ x → λ= (λ y → λ= (λ z → ∙=∙'₁ x y z)))*
>
>   ∙!=∙′! : (x y z : A) (p : x == y) (q : y == z) → ∙! x y z p q == ∙′! x y
> z p q
>   ∙!=∙′! x .x .x idp idp = idp
>
>   ∙!=∙′!₁ : (x y z : A) → ∙! x y z == ∙′! x y z
>   ∙!=∙′!₁ x y z = λ= (λ p → λ= (λ q → ∙!=∙′! x y z p q))
>
>   ∙!=∙′!₂ : ∙! == ∙′!
>   ∙!=∙′!₂ = λ= (λ x → λ= (λ y → λ= (λ z → ∙!=∙′!₁ x y z)))
>
>
> _______________________________________________
> HoTT-reading-group mailing list
> HoTT-reading-group at mit.edu
> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140130/81c143ce/attachment-0001.htm