[Agda] Confusion with levels in proof irrelevance

[Andreas Abel]

Hello Jan,

don't you need some form of functional extensionality?

E.g. when I write

   propEqFunctor {Cℓ₀} {Cℓ₁} {Dℓ₀} {Dℓ₁} {F₀ = F₀} {F₁ = F₁} {idF = idF} 
{idG} {distF} {distG} refl refl
     = let pi = proof-irrelevance idF idG in {!!}

I get some yellow, since there is a hidden argument to idF missing.  But 
I have no object in C to apply it to.

Cheers,
Andreas

On 17.06.2016 15:09, Jan Bracker wrote:
> Hello,
>
> I am trying to formalize some category theory in Agda. Using my
> definition of Category and Functor I wanted to show what it means for
> two functors to be propositionally equal. Attached is the module trying
> to achieve this.
>
> The problem is: When I try to use "proof-irrelevance" to prove that the
> laws are equal I get a confusing error about mismatching levels that I
> cannot explain:
>
>  > Minimal.agda:45,145-170
>  > (Set Dℓ₁) != (Set (Dℓ₁ ⊔ Cℓ₀))
>  > when checking that the expression (proof-irrelevance idF idG) has
>  > type (idF ≡ idG)
>
> I have tried specifying the implicit level argument of
> 'proof-irrelevance' to either of the mentioned levels with no progress.
>
> I have also tried to make the implicit arguments to the laws explicit
> together with using function extensionality, but again at some point I
> got stuck, because there were complaints about the mixture of implicit
> and explicit arguments.
>
> Can somebody help me with my definition?
>
> Best regards,
> Jan Bracker
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/