[Agda] comlicated equivalence: need help to prove

[Permjacov Evgeniy]

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