<div dir="ltr">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:<div>
<br></div><div><div> ∙=∙'₂ : (λ 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})</div><div> ∙=∙'₂ = λ= (λ x → λ= (λ y → λ= (λ z → ∙=∙'₁ x y z)))</div>
</div><div><br></div><div><br></div><div>-Jason</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jan 29, 2014 at 9:58 PM, Chris Jeris <span dir="ltr"><<a href="mailto:cjeris@gmail.com" target="_blank">cjeris@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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.)<div>
<br></div><div>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.</div>
<div><br></div><div>Can anyone help?</div><div><br></div><div>thanks, C<br><div><br></div><div><div><font face="courier new, monospace">{-# OPTIONS --without-K #-}</font></div><div><font face="courier new, monospace">module Exercises.Exercises2 where</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">open import HoTT public</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- 2.1. Show that the three obvious proofs of Lemma 2.1.2 are pairwise equal.</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- From PathGroupoid:</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- _∙_ : {x y z : A}</font></div>
<div><font face="courier new, monospace">-- → (x == y → y == z → x == z)</font></div><div><font face="courier new, monospace">-- idp ∙ q = q</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- _∙'_ : {x y z : A}</font></div>
<div><font face="courier new, monospace">-- → (x == y → y == z → x == z)</font></div><div><font face="courier new, monospace">-- q ∙' idp = q</font></div><div><font face="courier new, monospace"><br></font></div><div>
<font face="courier new, monospace">-- ∙=∙' : {x y z : A} (p : x == y) (q : y == z)</font></div><div><font face="courier new, monospace">-- → p ∙ q == p ∙' q</font></div><div><font face="courier new, monospace">-- ∙=∙' idp idp = idp</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">module _ {i} {A : Type i} where</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> -- ! are the versions with explicit x y z arguments</font></div>
<div><font face="courier new, monospace"> ∙! : (x y z : A) → x == y → y == z → x == z</font></div><div><font face="courier new, monospace"> ∙! x .x z idp q = q</font></div><div><font face="courier new, monospace"><br></font></div>
<div><font face="courier new, monospace"> ∙′! : (x y z : A) → x == y → y == z → x == z</font></div><div><font face="courier new, monospace"> ∙′! x y .y p idp = p</font></div><div><font face="courier new, monospace"><br>
</font></div><div><span style="font-family:'courier new',monospace"> -- The proof that any particular instances of the compositions are equal is a trivial path</span><br></div><div><font face="courier new, monospace"> -- induction, but to prove the operators themselves are equal we require extensionality.</font></div>
<div><font face="courier new, monospace"> ∙=∙'₁ : (x y z : A) → _∙_ {x = x} {y = y} {z = z} == _∙'_ {x = x} {y = y} {z = z}</font></div><div><font face="courier new, monospace"> ∙=∙'₁ x y z = λ= (λ p → λ= (λ q → ∙=∙' p q))</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> ∙=∙'₂ : _∙_ {i = i} {A = A} == _∙'_ {i = i} {A = A}</font></div><div><font face="courier new, monospace"><b>-- _x_75 == _y_76 != A of type Set i</b></font></div>
<div><font face="courier new, monospace"><b>-- when checking that the expression</b></font></div><div><font face="courier new, monospace"><b>-- λ= (λ x → λ= (λ y → λ= (λ z → ∙=∙'₁ x y z))) has type _∙_ == _∙'_</b></font></div>
<div><font face="courier new, monospace"> ∙=∙'₂ = <b>λ= (λ x → λ= (λ y → λ= (λ z → ∙=∙'₁ x y z)))</b></font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> ∙!=∙′! : (x y z : A) (p : x == y) (q : y == z) → ∙! x y z p q == ∙′! x y z p q</font></div>
<div><font face="courier new, monospace"> ∙!=∙′! x .x .x idp idp = idp</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> ∙!=∙′!₁ : (x y z : A) → ∙! x y z == ∙′! x y z</font></div>
<div><font face="courier new, monospace"> ∙!=∙′!₁ x y z = λ= (λ p → λ= (λ q → ∙!=∙′! x y z p q))</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> ∙!=∙′!₂ : ∙! == ∙′!</font></div>
<div><font face="courier new, monospace"> ∙!=∙′!₂ = λ= (λ x → λ= (λ y → λ= (λ z → ∙!=∙′!₁ x y z)))</font></div><div><br></div></div></div></div>
<br>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu">HoTT-reading-group@mit.edu</a><br>
<a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
<br></blockquote></div><br></div>