[Agda] Re: comlicated equivalence: need help to prove: errh, addres of repository

[Daniel Peebles]

I think you may have forgotten to add Category.Functor.Isomorphism to your
repository? I don't see it in
https://github.com/permeakra/agda-learning/tree/master/Category/Functor

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.

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:

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
  refl : {g : Category.Hom C A B} → (f≡g : Category._≡_ C f g) → [ C ] f ∼ g

(please excuse the coding style!)

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 http://coq.inria.fr/V8.2pl1/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.Hom_Equality.html
and translated it.

You can see more at
https://github.com/pumpkin/categories/blob/master/Category/Functor.agda.


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.

Hope this helps,

-Dan

On Thu, Feb 24, 2011 at 8:21 AM, Permjacov Evgeniy <permeakra at gmail.com>wrote:

> repository is here: https://github.com/permeakra/agda-learning
>
> On 02/24/2011 04:17 PM, Permjacov Evgeniy wrote:
> > Hello! I'm currently learning category theory with Abstract And Concrete
> > Categories: Joy of Cats (freely available online) and tries to formalise
> > some categorical concepts. Yesterday I came up to functor as Isomorphism
> > and was not able to prove transitivity on such isomorphisms as relations.
> >
> > I made a GitHub repository and uploaded work I have done. The current
> > goal is two holes in Category.Functor.Isomorphism
> >
> > In general, what is currently done.
> >  -- Level and Function modules are taken from standart library. Function
> > module is slightly modified
> >  -- Relation.Binary is stripped-down varian of Relation.Binary.Core from
> > standard library It contains Relation type and several types, encoding
> > relation properties
> >  -- Relation.Binary.Equivalence defines record for equivalence laws and
> > nothing more
> >  -- Relation.Binary.Equivalence.Setoid defines setoid type, intensional
> > equiality (stealed from Standart library) and several setoids and
> > several operations using intensional equality.
> >  -- Category defines category record
> >  -- Category.Morhpism.Properties defines isomorphism that is morphism on
> > objects of given category and its properies (reflexivity, transitivity,
> > symmetricity)
> >  -- Category.Functor defines functor type, i.e. mapping from category to
> > category
> >  -- Category.Functor.Composition defines composition of two functors.
> >  -- Category.Functor.Isomorphism is current work-in-progress and contains
> >   -- property of functor to be full
> >   -- property of functor to be faithfull
> >   -- isomorphism, i.e. collection of two opposite morphisms
> >   -- properties of isomorphism
> > What I currently have problem with is proving transitivity of
> > isomorphism on categories. It includes type-casting
> >  (application of cast : \all {A B} -> A \== B -> A -> B) in type
> > signature and I cannot understand how to build term needed.
> >
> > The code is freely available for any use and any constructive criticism
> > is welcomed.
> >
> > BTW, Category.Functor.Isomorphism and Category.Functor.Composition
> > (re)loads painfully slow. May be there is a way to speed-up Agda on such
> > files...
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110224/0bf027fc/attachment.html