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

[Permjacov Evgeniy]

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...