diff --git a/Adjunction.md b/Adjunction.md
index e8fc4f5..9e02fb5 100644
--- a/Adjunction.md
+++ b/Adjunction.md
@@ -10,7 +10,7 @@ trait Representable[F[_], Rep] {
 }
 ```
 
-* Implementations: [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Representable.scala), [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Representable.scala), [Haskell](https://hackage.haskell.org/package/adjunctions/docs/Data-Functor-Rep.html), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Functor/Representable.agda), [UniMath](https://github.com/UniMath/UniMath/tree/master/UniMath/CategoryTheory/RepresentableFunctors), [nLab](https://ncatlab.org/nlab/show/representable+functor)
+* Implementations: [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Representable.scala), [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Representable.scala), [Haskell](https://hackage.haskell.org/package/adjunctions/docs/Data-Functor-Rep.html), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Functor/Representable.agda), [UniMath](https://github.com/UniMath/UniMath/tree/master/UniMath/CategoryTheory/RepresentableFunctors), [nLab](https://ncatlab.org/nlab/show/representable+functor)
 
 * Resources:
   * (Haskell) Representing Applicatives - Gershom Bazerman [(blog post)](http://comonad.com/reader/2013/representing-applicatives/)
diff --git a/BasicAbstractions.md b/BasicAbstractions.md
index b9b1f2c..fdd3361 100644
--- a/BasicAbstractions.md
+++ b/BasicAbstractions.md
@@ -25,7 +25,7 @@ trait Functor[F[_]] {
 * Functor Implementations:  
   Scala: [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Functor.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/functor.scala), [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Functor.scala), [zio-prelude](https://github.com/zio/zio-prelude/blob/series/2.x/core/shared/src/main/scala/zio/prelude/Covariant.scala),  
   [Idris](https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Functor.idr), [Purescript](https://github.com/purescript/purescript-prelude/blob/master/src/Data/Functor.purs), [Haskell base](http://hackage.haskell.org/package/base/docs/Data-Functor.html), [Haskell data-category](http://hackage.haskell.org/package/data-category/docs/Data-Category-Functor.html#g:2), [Racket algebraic](https://docs.racket-lang.org/algebraic/class_base.html#%28part._class~3abase~3afunctor%29), [Racket functional](https://docs.racket-lang.org/functional/interfaces.html#%28part._functors%29), [nLab](https://ncatlab.org/nlab/show/functor), [Java Mojang/DataFixerUpper](https://github.com/Mojang/DataFixerUpper/blob/master/src/main/java/com/mojang/datafixers/kinds/Functor.java)
-* Encoding close to mathematics: [vpatryshev/Categories](https://github.com/vpatryshev/Categories/blob/master/src/main/scala/math/cat/Functor.scala)
+* Encoding close to mathematics: [vpatryshev/Categories](https://github.com/vpatryshev/Categories/blob/master/scala2/src/main/scala/math/cat/Functor.scala)
 * Formalization in proof assistants: [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/master/src/Basic/Functor.lidr), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Core/Functors.v), [HoTT Book](https://github.com/HoTT/HoTT/blob/master/theories/Categories/Functor/Core.v), [cubicaltt](https://github.com/mortberg/cubicaltt/blob/master/examples/category.ctt)
 
 * Functor Laws ([Cats](https://github.com/typelevel/cats/blob/master/laws/src/main/scala/cats/laws/FunctorLaws.scala), [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Functor.scala#L98-L107) [Haskell](http://hackage.haskell.org/package/base/docs/Data-Functor.html#t:Functor)):
@@ -314,7 +314,7 @@ trait Monad[F[_]] extends Apply[F] {
   [Cats FlatMap](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/FlatMap.scala), [Scalaz 7 Bind](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Bind.scala), [Scalaz 8 Bind](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/bind.scala)  
   Monad: [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Monad.scala), [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Monad.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/monad.scala),  
   [Haskell](https://hackage.haskell.org/package/base-4.16.0.0/docs/Control-Monad.html#t:Monad), [Idris](https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Monad.idr), [Purescript](https://pursuit.purescript.org/packages/purescript-prelude/docs/Control.Monad), [Racket algebraic](https://docs.racket-lang.org/algebraic/class_base.html#%28part._class~3abase~3amonad%29), [Racket functional](https://docs.racket-lang.org/functional/interfaces.html#%28part._monads%29)
-* Formalizations: [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Monad.agda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Monads/Monads.v), [nLab](https://ncatlab.org/nlab/show/monad)
+* Formalizations: [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Monad.agda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Monads/Monads.v), [nLab](https://ncatlab.org/nlab/show/monad)
 
 * Monad Laws ([Cats](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Monad.scala#L76-L85), [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Monad.scala#L76-L85), [Haskell Wiki](https://wiki.haskell.org/Monad_laws)):
     1. flatmap associativity: `fa.flatMap(f).flatMap(g) == fa.flatMap(a => f(a).flatMap(b => g(b))`
@@ -543,7 +543,7 @@ trait StateMonad[F[_],S] extends Monad[F] {
     * gist by xuwei-k (https://gist.github.com/xuwei-k/19c9bb8c3afd08175762957880c57500)
     * Continuation monad in Scala - Tony Morris [(blog post)](http://blog.tmorris.net/posts/continuation-monad-in-scala/index.html)
     * (Haskell) School of Haskell - The Mother of all Monads - Dan Piponi [(blog post)](https://www.schoolofhaskell.com/school/to-infinity-and-beyond/pick-of-the-week/the-mother-of-all-monads)
-    * (Haskell) Haskell for all - The Continuation Monad - Gabriel Gonzalez [(blog post)](http://www.haskellforall.com/2012/12/the-continuation-monad.html)
+    * (Haskell) Haskell for all - The Continuation Monad - Gabriella Gonzalez [(blog post)](http://www.haskellforall.com/2012/12/the-continuation-monad.html)
 
 ### Reverse State Monad
 
@@ -814,7 +814,7 @@ def distinct[A](fa: F[A])(implicit A: Order[A]): IList[A]
     * A tutorial on the universality and expressiveness of fold - Graham Hutton [(paper)](http://www.cs.nott.ac.uk/~pszgmh/fold.pdf)
     * (Haskell) Conquering Folds - Edward Kmett [blog post](https://www.schoolofhaskell.com/user/edwardk/conquering-folds)
     * (Haskell) Monoidal Sorting - Chris Penner [(blog post)](https://chrispenner.ca/posts/monoid-sort) (`Monoids` and `foldMap` used for sorting)
-    * Beautiful folds are practical, too - Gabriel Gonzalez [(video)](https://www.youtube.com/watch?v=6a5Ti0r8Q2s) [slides repo](https://github.com/Gabriel439/slides/blob/master/munihac/foldmap.md) [Hacker News](https://news.ycombinator.com/item?id=16478744)
+    * Beautiful folds are practical, too - Gabriella Gonzalez [(video)](https://www.youtube.com/watch?v=6a5Ti0r8Q2s) [slides repo](https://github.com/Gabriel439/slides/blob/master/munihac/foldmap.md) [Hacker News](https://news.ycombinator.com/item?id=16478744)
     * Beautiful folds in Scala - Adam Warski [(blog post)](https://softwaremill.com/beautiful-folds-in-scala/)
 
 ### Traverse
diff --git a/Comonads.md b/Comonads.md
index b4a2783..d3955dc 100644
--- a/Comonads.md
+++ b/Comonads.md
@@ -21,7 +21,7 @@ trait Comonad[C[_]] extends CoflatMap[C] {
 * Implementations:  
   CoflatMap/Cobind: [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/CoflatMap.scala),  [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Cobind.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/cobind.scala)    
   Comonad: [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Comonad.scala), [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Comonad.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/comonad.scala), [Haskell](https://hackage.haskell.org/package/comonad/docs/Control-Comonad.html), [Purescript](https://pursuit.purescript.org/packages/purescript-control/docs/Control.Comonad)
-* Verified implementations: [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/master/src/Comonad/Comonad.lidr), [agda-categories](https://github.com/agda/agda-categories/blob/master/Categories/Comonad.agda)
+* Verified implementations: [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/master/src/Comonad/Comonad.lidr), [agda-categories](https://github.com/agda/agda-categories/blob/master/src/Categories/Comonad.agda)
 
  
 If we define extract and extend:
diff --git a/Free.md b/Free.md
index be9c480..8ee4ed5 100644
--- a/Free.md
+++ b/Free.md
@@ -76,7 +76,7 @@ def freeMonad[F[_]](implicit FF: Functor[F]): Monad[FreeMonad[F, *]] = new Monad
 * Implementations: [Haskell transformers-free](http://hackage.haskell.org/package/transformers-free/docs/Control-Monad-Trans-Free.html) [Haskell free](http://hackage.haskell.org/package/free/docs/Control-Monad-Trans-Free.html) [Purescript](https://pursuit.purescript.org/packages/purescript-freet/)
 
 * Resources
-  * Free monad transformers - Gabriel Gonzalez [(blog post)](http://www.haskellforall.com/2012/07/free-monad-transformers.html)
+  * Free monad transformers - Gabriella Gonzalez [(blog post)](http://www.haskellforall.com/2012/07/free-monad-transformers.html)
 
 ### Cofree
 
diff --git a/HigherKinded.md b/HigherKinded.md
index 2b91a8c..4a0bf67 100644
--- a/HigherKinded.md
+++ b/HigherKinded.md
@@ -33,8 +33,8 @@ val headOption: List ~> Option = new ~>[List,Option] {
 Every polymorphic function (that do the same thing - do not change behavior for a specific type of X) have some nice properties. More in paper by [Philip Wadler - Theorems for free](http://homepages.inf.ed.ac.uk/wadler/topics/blame.html#parablame).
 
 * Implementations: [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/NaturalTransformation.scala), [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/arrow/FunctionK.scala), [Haskell](http://hackage.haskell.org/package/natural-transformation/docs/Control-Natural.html)
-* Encoding close to mathematics: [vpatryshev/Categories](https://github.com/vpatryshev/Categories/blob/master/src/main/scala/math/cat/NaturalTransformation.scala)
-* Formalization in proof assistants: [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/master/src/Basic/NaturalTransformation.lidr), [agda-categories](https://github.com/agda/agda-categories/blob/master/Categories/NaturalTransformation/Core.agda) [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Core/NaturalTransformations.v), [CubicalTT](https://github.com/mortberg/cubicaltt/blob/master/examples/univprop.ctt)
+* Encoding close to mathematics: [vpatryshev/Categories](https://github.com/vpatryshev/Categories/blob/master/scala2/src/main/scala/math/cat/NaturalTransformation.scala)
+* Formalization in proof assistants: [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/master/src/Basic/NaturalTransformation.lidr), [agda-categories](https://github.com/agda/agda-categories/blob/master/src/Categories/NaturalTransformation/Core.agda) [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Core/NaturalTransformations.v), [CubicalTT](https://github.com/mortberg/cubicaltt/blob/master/examples/univprop.ctt)
 * Definition in Category Theory: [nLab](https://ncatlab.org/nlab/show/natural+transformation)
 
 * Resources
@@ -73,8 +73,8 @@ trait FFunctor[FF[_]] {
   * (Haskell) Q: What is not an MFunctor? [reddit](https://www.reddit.com/r/haskell/comments/2c87m8/q_what_is_not_an_mfunctor/)
   * (Haskell) [MMonad](https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html#t:MMonad)
   * (Haskell) [Github issue with code with MCoyoneda](https://github.com/Gabriel439/Haskell-MMorph-Library/issues/33)
-  * (Haskell) [Tutorial - Gabriel Gonzalez](http://hackage.haskell.org/package/mmorp-1.1.2/docs/Control-Monad-Morph.html#g:3)
-  * (Haskell) mmorph-1.0.0: Monad morphisms - Gabriel Gonzalez [blog post](http://www.haskellforall.com/2013/03/mmorph-100-monad-morphisms.html)
+  * (Haskell) [Tutorial - Gabriella Gonzalez](https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html#g:3)
+  * (Haskell) mmorph-1.0.0: Monad morphisms - Gabriella Gonzalez [blog post](http://www.haskellforall.com/2013/03/mmorph-100-monad-morphisms.html)
 
 ### higher kinded category theory
   * [hask](https://github.com/ekmett/hask)
@@ -144,7 +144,7 @@ trait MonoidalCategoryLaws[M[_, _], I] extends MonoidalCategory[M,I] {
 }
 ```
 
-* Implementations: [Haskell](https://hackage.haskell.org/package/categories/docs/Control-Category-Monoidal.html#t:Monoidal), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Category/Monoidal.agda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Monoidal/MonoidalCategories.v), [nlab](https://ncatlab.org/nlab/show/monoidal+category)
+* Implementations: [Haskell](https://hackage.haskell.org/package/categories/docs/Control-Category-Monoidal.html#t:Monoidal), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Monoidal/Core.agda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Monoidal/Categories.v), [nlab](https://ncatlab.org/nlab/show/monoidal+category)
 
 We can create monoidal category where product (Tuple) is a bifunctor or an coproduct (Either).
 
@@ -164,15 +164,15 @@ In category of Profunctors with Profunctor Product as Bifunctor the Monoid Objec
  
 ### Braided Monoidal Category
 
-* Implementations: [Haskell](https://hackage.haskell.org/package/categories/docs/Control-Category-Braided.html#t:Braided), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Category/Monoidal/Braided.agda)
+* Implementations: [Haskell](https://hackage.haskell.org/package/categories/docs/Control-Category-Braided.html#t:Braided), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Monoidal/Braided.agda)
 
 ### Symmetric Monoidal Category
 
-* Implementations [Haskell](https://hackage.haskell.org/package/categories/docs/Control-Category-Braided.html#t:Symmetric), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Category/Monoidal/Symmetric.agda)
+* Implementations [Haskell](https://hackage.haskell.org/package/categories/docs/Control-Category-Braided.html#t:Symmetric), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Monoidal/Symmetric.agda)
 
 ### Cartesian Closed Category
 
-* Implementations [Haskell](https://hackage.haskell.org/package/category-extras-0.53.0/docs/Control-Category-Cartesian-Closed.html), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Category/CartesianClosed.agda)
+* Implementations [Haskell](https://hackage.haskell.org/package/category-extras-0.53.0/docs/Control-Category-Cartesian-Closed.html), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Category/CartesianClosed.agda)
 
 * Resources
   * [TomasMikula/LambdaCart](https://github.com/TomasMikula/LambdaCart) (CCC is used to define EDSL in Scala)
diff --git a/KanExtensions.md b/KanExtensions.md
index 9b8b0a6..2023a18 100644
--- a/KanExtensions.md
+++ b/KanExtensions.md
@@ -120,7 +120,7 @@ def yonedaFunctor[F[_]]: Functor[Yoneda[F, *]] =
 
 * Yoneda efficiently stack computations.
 
-* Implementations scalaz [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Yoneda.scala), [Purescript](https://pursuit.purescript.org/packages/purescript-free/docs/Data.Yoneda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/covyoneda.v), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Yoneda.agda), [HoTT](https://github.com/HoTT/HoTT/blob/master/theories/Categories/Yoneda.v), [nlab](https://ncatlab.org/nlab/show/Yoneda+lemma)
+* Implementations scalaz [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Yoneda.scala), [Purescript](https://pursuit.purescript.org/packages/purescript-free/docs/Data.Yoneda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/covyoneda.v), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Yoneda.agda), [HoTT](https://github.com/HoTT/HoTT/blob/master/theories/Categories/Yoneda.v), [nlab](https://ncatlab.org/nlab/show/Yoneda+lemma)
 
 * Resources
   * https://vimeo.com/122708005
@@ -201,7 +201,7 @@ trait Ran[G[_], H[_], A] {
 }
 ```
 
-* Implementations: [Scalaz](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Kan.scala), [Haskell](http://hackage.haskell.org/package/kan-extensions/docs/Data-Functor-Kan-Ran.html), [Purescript](https://github.com/freebroccolo/purescript-kan-extensions/blob/master/src/Data/Functor/Kan/Ran.purs), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Kan.agda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/RightKanExtension.v), [nLab](https://ncatlab.org/nlab/show/Kan+extension)
+* Implementations: [Scalaz](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Kan.scala), [Haskell](http://hackage.haskell.org/package/kan-extensions/docs/Data-Functor-Kan-Ran.html), [Purescript](https://github.com/freebroccolo/purescript-kan-extensions/blob/master/src/Data/Functor/Kan/Ran.purs), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Kan.agda), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/RightKanExtension.v), [nLab](https://ncatlab.org/nlab/show/Kan+extension)
 
 * We can create functor for Ran, without any requirements on G, H
 ```scala
@@ -252,7 +252,7 @@ trait Lan[F[_], H[_], A] {
 }
 ```
 
-[Scalaz](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Kan.scala), [Haskell](http://hackage.haskell.org/package/kan-extensions/docs/Data-Functor-Kan-Lan.html), [Purescript](https://github.com/freebroccolo/purescript-kan-extensions/blob/master/src/Data/Functor/Kan/Lan.purs), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Kan.agda), [nLab](https://ncatlab.org/nlab/show/Kan+extension)
+[Scalaz](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Kan.scala), [Haskell](http://hackage.haskell.org/package/kan-extensions/docs/Data-Functor-Kan-Lan.html), [Purescript](https://github.com/freebroccolo/purescript-kan-extensions/blob/master/src/Data/Functor/Kan/Lan.purs), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Kan.agda), [nLab](https://ncatlab.org/nlab/show/Kan+extension)
 
 * we can define Functor for it
 ```scala
diff --git a/Profunctors.md b/Profunctors.md
index 7f62539..950da7f 100644
--- a/Profunctors.md
+++ b/Profunctors.md
@@ -85,7 +85,7 @@ trait Profunctor[F[_, _]] {
 ```
 
 * Implementations: [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Profunctor.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/profunctor.scala), [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/arrow/Profunctor.scala), [Haskell](hackage.haskell.org/package/profunctors/docs/Data-Profunctor.html), [Purescript](https://github.com/purescript/purescript-profunctor/blob/master/src/Data/Profunctor.purs), [Java](https://github.com/Mojang/DataFixerUpper/blob/master/src/main/java/com/mojang/datafixers/optics/profunctors/Profunctor.java)
-* Verified implementations: [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Functor/Profunctor.agda),[UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Profunctors/Core.v), [idris-ct Profunctors](https://github.com/statebox/idris-ct/blob/master/src/Profunctors/Profunctor.lidr)
+* Verified implementations: [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Functor/Profunctor.agda),[UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Profunctors/Core.v), [idris-ct Profunctors](https://github.com/statebox/idris-ct/blob/master/src/Profunctors/Profunctor.lidr)
 * Definition in Category Theory: [nLab](https://ncatlab.org/nlab/show/profunctor)
 
 * Alternatively we can define functor using:
@@ -542,8 +542,8 @@ that satisfy certain conditions.
 * Implementations:  
   [Cats Compose](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/arrow/Compose.scala), [Scalaz 8 Semicategory](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/semicategory.scala), [zio-prelude AssociativeCompose](https://github.com/zio/zio-prelude/blob/series/2.x/core/shared/src/main/scala/zio/prelude/AssociativeCompose.scala) 
   Category: [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/arrow/Category.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/category.scala), [Haskell](https://hackage.haskell.org/package/base/docs/Control-Category.html), [nlab](https://ncatlab.org/nlab/show/category)
-* Encoding close to mathematics: [vpatryshev/Categories](https://github.com/vpatryshev/Categories/blob/master/src/main/scala/math/cat/Category.scala)
-* Formalization in proof assistants: [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/master/src/Basic/Category.lidr), [agda-categories](https://github.com/agda/agda-categories/blob/master/Categories/Category/Core.agda), [cubicaltt](https://github.com/mortberg/cubicaltt/blob/master/examples/category.ctt)
+* Encoding close to mathematics: [vpatryshev/Categories](https://github.com/vpatryshev/Categories/blob/master/scala2/src/main/scala/math/cat/Category.scala)
+* Formalization in proof assistants: [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/master/src/Basic/Category.lidr), [agda-categories](https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Core.agda), [cubicaltt](https://github.com/mortberg/cubicaltt/blob/master/examples/category.ctt)
 
 * Category laws [Cats Category laws](https://github.com/typelevel/cats/blob/master/laws/src/main/scala/cats/laws/CategoryLaws.scala), [Cats Compose laws](https://github.com/typelevel/cats/blob/master/laws/src/main/scala/cats/laws/ComposeLaws.scala):
 
@@ -653,7 +653,7 @@ Implementation in [statebox/idris-ct](https://github.com/statebox/idris-ct/blob/
 
 * Resources
   * Cats [src](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/arrow/ArrowChoice.scala)
-  * [channingwalton/typeclassopedia ArrowChoice](https://github.com/channingwalton/typeclassopedia/blob/master/src/main/scala/org/typeclassopedia/ArrowChoice.scala)
+  * [channingwalton/typeclassopedia ArrowChoice](https://github.com/channingwalton/typeclassopedia/blob/scala-2/src/main/scala/org/typeclassopedia/ArrowChoice.scala)
   * (Haskell) [Typeclassopedia ArrowChoice](https://wiki.haskell.org/Typeclassopedia#ArrowChoice)
 
 ### Arrow Apply, Arrow Monad
@@ -732,7 +732,7 @@ trait DinaturalTransformation[P[_,_],Q[_,_]]{
 * Resources
    * [Scalaz src](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/NaturalTransformation.scala#L87-L89)
    * [nlab/Extranatural Transformation](https://ncatlab.org/nlab/show/extranatural+transformation)
-   * [Agda](https://github.com/agda/agda-categories/blob/master/Categories/NaturalTransformation/Dinatural.agda)
+   * [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/NaturalTransformation/Dinatural.agda)
 
 ### Ends & Coends
 
diff --git a/notes/Hitchhiker's Guide to the Quadrinitarianism.MD b/notes/Hitchhiker's Guide to the Quadrinitarianism.MD
index 00a0ee7..27bdf13 100644
--- a/notes/Hitchhiker's Guide to the Quadrinitarianism.MD	
+++ b/notes/Hitchhiker's Guide to the Quadrinitarianism.MD	
@@ -83,7 +83,7 @@ trait Category[F[_, _]] {
 Implementations in libraries:  
 *  Compose/Semicategory [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/arrow/Compose.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/semicategory.scala)  
   Category: [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/arrow/Category.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/category.scala), [Haskell](https://hackage.haskell.org/package/base/docs/Control-Category.html)
-* Implementations in proof assistants: [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Category/Core.agda), [CubicalTT](https://github.com/mortberg/cubicaltt/blob/master/examples/category.ctt)
+* Implementations in proof assistants: [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Core.agda), [CubicalTT](https://github.com/mortberg/cubicaltt/blob/master/examples/category.ctt)
 
 [Cats Category laws](https://github.com/typelevel/cats/blob/master/laws/src/main/scala/cats/laws/CategoryLaws.scala), [Cats Compose laws](https://github.com/typelevel/cats/blob/master/laws/src/main/scala/cats/laws/ComposeLaws.scala):
  * associativity `f.compose(g.compose(h)) == f.compose(g).compose(h)`