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

[Chris Jeris]

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)))
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140129/d65d9f5a/attachment.htm