I think you may have forgotten to add Category.Functor.Isomorphism to your repository? I don't see it in <a href="https://github.com/permeakra/agda-learning/tree/master/Category/Functor">https://github.com/permeakra/agda-learning/tree/master/Category/Functor</a><div>
<br></div><div>I'm not sure that cast operation is what you really want if you aren't using Agda's propositional equality, but without seeing the rest of it it's hard to say.</div><div><br></div><div>Strangely enough, I recently started work on a similar project and had some difficulty with functor equivalence as well. After a brief attempt using natural isomorphism as equivalence between functors (which was exceedingly easy to work with, but rather loose), I went with a weird heterogeneous equality-like beast that relies on the underlying category's morphism equivalence relation:</div>
<div><br></div><div><meta charset="utf-8"><span class="Apple-style-span" style="font-family: helvetica, arial, freesans, clean, sans-serif; font-size: 11px; line-height: 14px; "><pre style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; padding-top: 0px; padding-right: 0px; padding-bottom: 0px; padding-left: 0px; font: normal normal normal 12px/normal Monaco, 'Courier New', 'DejaVu Sans Mono', 'Bitstream Vera Sans Mono', monospace; line-height: 1.4em; font-family: 'Bitstream Vera Sans Mono', Courier, monospace; font-size: 12px; ">
<div class="line" id="LC11" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; padding-top: 0px; padding-right: 0px; padding-bottom: 0px; padding-left: 1em; line-height: 1.4em; ">data [_]_∼_ {o ℓ e} (C : Category o ℓ e) {A B} (f : Category.Hom C A B) : ∀ {X Y} → Category.Hom C X Y → Set (ℓ ⊔ e) where</div>
<div class="line" id="LC12" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; padding-top: 0px; padding-right: 0px; padding-bottom: 0px; padding-left: 1em; line-height: 1.4em; "> refl : {g : Category.Hom C A B} → (f≡g : Category._≡_ C f g) → [ C ] f ∼ g</div>
<div><br></div><div>(please excuse the coding style!)</div><div><br></div><div>This allows you to talk about the equality of things that are not superficially equal (like F A -> F B and G A -> G B). I found the idea on <a href="http://coq.inria.fr/V8.2pl1/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.Hom_Equality.html">http://coq.inria.fr/V8.2pl1/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.Hom_Equality.html</a> and translated it.</div>
<div><br></div></pre></span></div><div>You can see more at <a href="https://github.com/pumpkin/categories/blob/master/Category/Functor.agda">https://github.com/pumpkin/categories/blob/master/Category/Functor.agda</a>.</div>
<div><br></div><div><br></div><div>If you're wondering why the name includes the underlying category, so am I. It's very puzzling, but if I don't include the C parameter (by making it implicit) even in the type of refl, it'll turn yellow. I could understand it having trouble if C were an index to the type, but as a parameter, the unsolved metas make no sense to me.</div>
<div><br></div><div>Hope this helps,</div><div><br></div><div>-Dan<br><br><div class="gmail_quote">On Thu, Feb 24, 2011 at 8:21 AM, Permjacov Evgeniy <span dir="ltr"><<a href="mailto:permeakra@gmail.com">permeakra@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">repository is here: <a href="https://github.com/permeakra/agda-learning" target="_blank">https://github.com/permeakra/agda-learning</a><br>
<br>
On 02/24/2011 04:17 PM, Permjacov Evgeniy wrote:<br>
> Hello! I'm currently learning category theory with Abstract And Concrete<br>
> Categories: Joy of Cats (freely available online) and tries to formalise<br>
> some categorical concepts. Yesterday I came up to functor as Isomorphism<br>
> and was not able to prove transitivity on such isomorphisms as relations.<br>
><br>
> I made a GitHub repository and uploaded work I have done. The current<br>
> goal is two holes in Category.Functor.Isomorphism<br>
><br>
> In general, what is currently done.<br>
> -- Level and Function modules are taken from standart library. Function<br>
> module is slightly modified<br>
> -- Relation.Binary is stripped-down varian of Relation.Binary.Core from<br>
> standard library It contains Relation type and several types, encoding<br>
> relation properties<br>
> -- Relation.Binary.Equivalence defines record for equivalence laws and<br>
> nothing more<br>
> -- Relation.Binary.Equivalence.Setoid defines setoid type, intensional<br>
> equiality (stealed from Standart library) and several setoids and<br>
> several operations using intensional equality.<br>
> -- Category defines category record<br>
> -- Category.Morhpism.Properties defines isomorphism that is morphism on<br>
> objects of given category and its properies (reflexivity, transitivity,<br>
> symmetricity)<br>
> -- Category.Functor defines functor type, i.e. mapping from category to<br>
> category<br>
> -- Category.Functor.Composition defines composition of two functors.<br>
> -- Category.Functor.Isomorphism is current work-in-progress and contains<br>
> -- property of functor to be full<br>
> -- property of functor to be faithfull<br>
> -- isomorphism, i.e. collection of two opposite morphisms<br>
> -- properties of isomorphism<br>
> What I currently have problem with is proving transitivity of<br>
> isomorphism on categories. It includes type-casting<br>
> (application of cast : \all {A B} -> A \== B -> A -> B) in type<br>
> signature and I cannot understand how to build term needed.<br>
><br>
> The code is freely available for any use and any constructive criticism<br>
> is welcomed.<br>
><br>
> BTW, Category.Functor.Isomorphism and Category.Functor.Composition<br>
> (re)loads painfully slow. May be there is a way to speed-up Agda on such<br>
> files...<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>