From fa89a32cb7641275c20fe314f23ea1f50458a5ea Mon Sep 17 00:00:00 2001 From: lemastero Date: Thu, 5 Dec 2024 01:56:05 +0100 Subject: [PATCH] Fix broken links and drop non-existing resources --- AbstractAlgebra.md | 4 ++-- BasicAbstractions.md | 2 +- Bifunctors.md | 8 ++++---- CombinatoryBirds.md | 1 - Limits.md | 9 ++++----- README.md | 3 +-- Topos.md | 6 +++--- 7 files changed, 15 insertions(+), 18 deletions(-) diff --git a/AbstractAlgebra.md b/AbstractAlgebra.md index 50188e29..e868d671 100644 --- a/AbstractAlgebra.md +++ b/AbstractAlgebra.md @@ -64,7 +64,7 @@ def combineAllOption(as: TraversableOnce[A]): Option[A] * Examples how to define alternative Semigroup instances [for Option, Int with *](https://github.com/lemastero/learn_scala_cats/blob/master/src/main/scala/monoid/AlternativeMonoidInstances.scala) and [usage](https://github.com/lemastero/learn_scala_cats/blob/master/src/test/scala/monoid/AlternativeMonoidInstancesSpec.scala). Examples for usage of derived methods and combine [(src)](https://github.com/lemastero/learn_scala_cats/blob/master/src/test/scala/semigroup/SemigroupExamplesSpec.scala) -* Implementations: [Cats](https://github.com/typelevel/cats/blob/master/kernel/src/main/scala/cats/kernel/Semigroup.scala) [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Semigroup.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/semigroup.scala), [twitter/algebird](https://github.com/twitter/algebird/blob/master/algebird-core/src/main/scala/com/twitter/algebird/Semigroup.scala), [zio-prelude](https://github.com/zio/zio-prelude/blob/master/src/main/scala/zio/prelude/Associative.scala), [Haskell](http://hackage.haskell.org/package/base/docs/Data-Semigroup.html), [Racket algebraic](https://docs.racket-lang.org/algebraic/class_base.html#%28part._class~3abase~3asemigroup%29), [Java](http://www.functionaljava.org/javadoc/4.8.1/functionaljava/fj/Semigroup.html) +* Implementations: [Cats](https://github.com/typelevel/cats/blob/master/kernel/src/main/scala/cats/kernel/Semigroup.scala) [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Semigroup.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/semigroup.scala), [twitter/algebird](https://github.com/twitter/algebird/blob/master/algebird-core/src/main/scala/com/twitter/algebird/Semigroup.scala), [zio-prelude](https://github.com/zio/zio-prelude/blob/master/src/main/scala/zio/prelude/Associative.scala), [Haskell](http://hackage.haskell.org/package/base/docs/Data-Semigroup.html), [Racket algebraic](https://docs.racket-lang.org/algebraic/class_base.html#%28part._class~3abase~3asemigroup%29), [Java](https://github.com/functionaljava/functionaljava/blob/series/5.x/core/src/main/java/fj/Semigroup.java) * Resources: * herding cats - Semigroup [(blog post)](http://eed3si9n.com/herding-cats/Semigroup.html) @@ -115,7 +115,7 @@ in [monoid-subclasses in Haskell](https://hackage.haskell.org/package/monoid-sub * We can joint two monoids into tuple of monoids. -* Implementations: [Cats](https://github.com/typelevel/cats/blob/master/kernel/src/main/scala/cats/kernel/Monoid.scala), [Scalaz](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Monoid.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/monoid.scala), [Racket algebraic](https://docs.racket-lang.org/algebraic/class_base.html#%28part._class~3abase~3amonoid%29), [Java functionaljava](http://www.functionaljava.org/javadoc/4.8.1/functionaljava/fj/Monoid.html) [Java DataFixerUpper](https://github.com/Mojang/DataFixerUpper/blob/master/src/main/java/com/mojang/datafixers/kinds/Monoid.java) +* Implementations: [Cats](https://github.com/typelevel/cats/blob/master/kernel/src/main/scala/cats/kernel/Monoid.scala), [Scalaz](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Monoid.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/monoid.scala), [Racket algebraic](https://docs.racket-lang.org/algebraic/class_base.html#%28part._class~3abase~3amonoid%29), [Java functionaljava](https://github.com/functionaljava/functionaljava/blob/series/5.x/core/src/main/java/fj/Monoid.java) [Java DataFixerUpper](https://github.com/Mojang/DataFixerUpper/blob/master/src/main/java/com/mojang/datafixers/kinds/Monoid.java) * Resources: * FSiS 4 - Semigroup, Monoid, and Foldable type classes - Michael Pilquist [video 23:02](https://www.youtube.com/watch?v=ueo_E2BxMnA&t=1381) diff --git a/BasicAbstractions.md b/BasicAbstractions.md index 0f94a674..ba75ca7e 100644 --- a/BasicAbstractions.md +++ b/BasicAbstractions.md @@ -64,7 +64,7 @@ def widen[A, B >: A](fa: F[A]): F[B] * Functors can compose: Cats [ComposedFunctor](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Composed.scala#L20-L26) [compose](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Functor.scala#L147-L151), [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Functor.scala#L61-L66) -* An examples for [instances for built in types](https://github.com/lemastero/learn_scala_cats/blob/master/src/main/scala/functor/InstancesForBuiltInTypes.scala), +* An examples for [instances for built in types](https://github.com/lemastero/scala_typeclassopedia/blob/main/src/test/scala/bifunctor/BicovariantExamplesSpec.scala), [function1](https://www.youtube.com/watch?v=Dsd4pc99FSY&t=1075), and [custom Tree type](https://github.com/lemastero/learn_scala_cats/blob/master/src/main/scala/functor/TreeFunctor.scala). An examples for [usage of map, derived methods, compose](https://github.com/lemastero/learn_scala_cats/blob/master/src/test/scala/functor/FunctorExamplesSpec.scala). diff --git a/Bifunctors.md b/Bifunctors.md index 4fa31ad5..239a4925 100644 --- a/Bifunctors.md +++ b/Bifunctors.md @@ -91,7 +91,7 @@ def umap[A, B](faa: F[A, A])(f: A => B): F[B, B] def widen[A, B, C >: A, D >: B](fab: F[A, B]): F[C, D] ``` -* Implementations: [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Bifunctor.scala), [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Bifunctor.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/bifunctor.scala), [Haskell](https://hackage.haskell.org/package/base/docs/Data-Bifunctor.html), [Purescript](https://pursuit.purescript.org/packages/purescript-bifunctors/docs/Data.Bifunctor), [Idris](https://github.com/japesinator/Idris-Bifunctors/blob/master/src/Data/Bifunctor.idr), [Agda](https://github.com/agda/agda-categories/blob/master/Categories/Functor/Bifunctor.agda) +* Implementations: [Cats](https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/Bifunctor.scala), [Scalaz 7](https://github.com/scalaz/scalaz/blob/series/7.3.x/core/src/main/scala/scalaz/Bifunctor.scala), [Scalaz 8](https://github.com/scalaz/scalaz/blob/series/8.0.x/base/shared/src/main/scala/scalaz/tc/bifunctor.scala), [Haskell](https://hackage.haskell.org/package/base/docs/Data-Bifunctor.html), [Purescript](https://pursuit.purescript.org/packages/purescript-bifunctors/docs/Data.Bifunctor), [Idris](https://github.com/japesinator/Idris-Bifunctors/blob/master/src/Data/Bifunctor.idr), [Agda](https://github.com/agda/agda-categories/blob/master/src/Categories/Functor/Bifunctor.agda) * Instances [can be defined](https://github.com/lemastero/learn_scala_cats/blob/master/src/main/scala/functor/bifunctor/InstancesForForBuildInTypes.scala) for: Tuple2, Either, Validated. For Function1 not - functions are contravariant for input type. @@ -129,7 +129,7 @@ newtype WrappedBifunctor p a b = WrapBifunctor { unwrapBifunctor :: p a b } -- Bifunctor p => Functor (WrappedBifunctor p a) ``` -* Implementations [Haskell bifunctors/Data.Bifunctor.Wrapped](https://hackage.haskell.org/package/bifunctors/docs/Data-Bifunctor-Wrapped.html) [purescript-bifunctors/Data.Bifunctor.Wrap](https://pursuit.purescript.org/packages/purescript-bifunctors/docs/Data.Bifunctor.Wrap) +* Implementations [Haskell bifunctors/Data.Bifunctor.Wrapped](https://hackage.haskell.org/package/bifunctors/docs/Data-Bifunctor-Wrapped.html) [purescript-bifunctors/Data.Bifunctor.Wrap](https://pursuit.purescript.org/packages/purescript-bifunctors/4.0.0/docs/Data.Bifunctor.Wrap) ### Bifunctor Flip @@ -142,7 +142,7 @@ newtype Flip p a b = Flip { runFlip :: p b a } -- Bifunctor p => Bifunctor (Flip p) ``` -* Implementations [Haskell bifunctors/Data.Bifunctor.Flip](https://hackage.haskell.org/package/bifunctors/docs/Data-Bifunctor-Flip.html) [purescript-bifunctors/Data.Bifunctor.Flip](https://pursuit.purescript.org/packages/purescript-bifunctors/docs/Data.Bifunctor.Flip) +* Implementations [Haskell bifunctors/Data.Bifunctor.Flip](https://hackage.haskell.org/package/bifunctors/docs/Data-Bifunctor-Flip.html) [purescript-bifunctors/Data.Bifunctor.Flip](https://pursuit.purescript.org/packages/purescript-bifunctors/4.0.0/docs/Data.Bifunctor.Flip) ### Bifunctor Joker @@ -190,7 +190,7 @@ data Product f g a b = Pair (f a b) (g a b) -- (Bifunctor f, Bifunctor g) => Bifunctor (Product f g) ``` -* Implementations [Haskell bifunctors/Data.Bifunctor.Product](https://hackage.haskell.org/package/bifunctors/docs/Data-Bifunctor-Product.html) [purescript-bifunctors/Data.Bifunctor.Product](https://pursuit.purescript.org/packages/purescript-bifunctors/docs/Data.Bifunctor.Product) +* Implementations [Haskell bifunctors/Data.Bifunctor.Product](https://hackage.haskell.org/package/bifunctors/docs/Data-Bifunctor-Product.html) [purescript-bifunctors/Data.Bifunctor.Product](https://pursuit.purescript.org/packages/purescript-bifunctors/4.0.0/docs/Data.Bifunctor.Product) ### Bifunctor Sum diff --git a/CombinatoryBirds.md b/CombinatoryBirds.md index b72e6c64..77247512 100644 --- a/CombinatoryBirds.md +++ b/CombinatoryBirds.md @@ -19,7 +19,6 @@ * [Combinator Birds - Chris Rathman](http://www.angelfire.com/tx4/cus/combinator/birds.html) Reference of Birds expressed as Combinatory Logic (SKI calculus) * [functions from Functor, Applicative, Monad, Comond as combinators](http://hackage.haskell.org/package/data-aviary/docs/Data-Aviary-Functional.html) * [Haskell Wiki Combinatory logic](https://wiki.haskell.org/Combinatory_logic) - * [Combinatory Logic Tutorial - Chris Barker](http://www.nyu.edu/projects/barker/Lambda/ski.html) * The Thrush combinator in Scala - Debasish Ghosh [(blog post)](http://debasishg.blogspot.com/2009/09/thrush-combinator-in-scala.html) * (Haskell) Combinators in Haskell - geophf [(blog post)](http://logicaltypes.blogspot.com/2008/08/combinators-in-haskell.html) * (Haskell) Combinatory Birds as Types - geophf [(blog post)](http://logicaltypes.blogspot.com/2008/08/combinatory-birds-as-types.html) \ No newline at end of file diff --git a/Limits.md b/Limits.md index e56493b4..e611941e 100644 --- a/Limits.md +++ b/Limits.md @@ -4,13 +4,12 @@ * [Haskell wiki ADT](https://wiki.haskell.org/Algebraic_data_type) * Simple Algebraic Data Types - Bartosz Milewski [blog post](https://bartoszmilewski.com/2015/01/13/simple-algebraic-data-types/) * Category Theory 5.2: Algebraic data types - Bartosz Milewski [video](https://www.youtube.com/watch?v=w1WMykh7AxA) - * Counting type inhabitants - Alexander Konovalov [blog post](https://alexknvl.com/posts/counting-type-inhabitants.html) ### Unit Type that has only one element -* Implementations [scala.Unit](https://www.scala-lang.org/api/2.11.12/#scala.Unit) [purescript-prelude/Data.Unit](https://pursuit.purescript.org/packages/purescript-prelude/docs/Data.Unit), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/limits/terminal.v), [nLab](https://ncatlab.org/nlab/show/terminal+object) +* Implementations [scala.Unit](https://www.scala-lang.org/api/2.11.12/#scala.Unit) [purescript-prelude/Data.Unit](https://pursuit.purescript.org/packages/purescript-prelude/docs/Data.Unit), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Limits/Terminal.v), [nLab](https://ncatlab.org/nlab/show/terminal+object) * Resources * Category Theory 4.1: Terminal and initial objects [video](https://www.youtube.com/watch?v=zer1aFgj4aU&feature=youtu.be&t=615) [Scala translation](https://github.com/typelevel/CT_from_Programmers.scala/blob/master/src/main/tut/2.2-limits-and-colimits.md) @@ -21,7 +20,7 @@ Type that has only one element Type that has no elements. In Category Theory - Initial Object -* Implementations [scala.Nothing](https://www.scala-lang.org/api/2.11.12/#scala.Nothing) [purescript-prelude/Data.Void](https://pursuit.purescript.org/packages/purescript-prelude/docs/Data.Void) [Idris prelude/Prelude/Uninhabited](https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Uninhabited.idr), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/limits/initial.v), [nLab](https://ncatlab.org/nlab/show/initial+object) +* Implementations [scala.Nothing](https://www.scala-lang.org/api/2.11.12/#scala.Nothing) [purescript-prelude/Data.Void](https://pursuit.purescript.org/packages/purescript-prelude/docs/Data.Void) [Idris prelude/Prelude/Uninhabited](https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Uninhabited.idr), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Limits/Initial.v), [nLab](https://ncatlab.org/nlab/show/initial+object) * Resources * Category Theory 4.1: Terminal and initial objects [video](https://www.youtube.com/watch?v=zer1aFgj4aU&feature=youtu.be&t=615) [Scala translation](https://github.com/typelevel/CT_from_Programmers.scala/blob/master/src/main/tut/2.2-limits-and-colimits.md) @@ -32,14 +31,14 @@ In Category Theory - Initial Object Type represents either one or another element. In set theory: disjoint union in Category theory: coproduct (sum). -* Implementations [scala.util.Either](https://www.scala-lang.org/api/2.11.12/index.html#scala.util.Either) [purescript-either/Data.Either](https://pursuit.purescript.org/packages/purescript-either/docs/Data.Either), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/limits/coproducts.v), [nLab](https://ncatlab.org/nlab/show/coproduct) +* Implementations [scala.util.Either](https://www.scala-lang.org/api/2.11.12/index.html#scala.util.Either) [purescript-either/Data.Either](https://pursuit.purescript.org/packages/purescript-either/docs/Data.Either), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Limits/Coproducts.v), [nLab](https://ncatlab.org/nlab/show/coproduct) ## Product Type represents combination of two types. In Set theory cartesian product, in Category Theory product. -* Implementations [scala.Product2](https://www.scala-lang.org/api/2.11.12/index.html#scala.Product2) [scala.Tuple2](https://www.scala-lang.org/api/2.11.12/#scala.Tuple2) [purescript-tuples/Data.Tuple](https://pursuit.purescript.org/packages/purescript-tuples/docs/Data.Tuple), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/limits/products.v), [nLab](https://ncatlab.org/nlab/show/cartesian+product) +* Implementations [scala.Product2](https://www.scala-lang.org/api/2.11.12/index.html#scala.Product2) [scala.Tuple2](https://www.scala-lang.org/api/2.11.12/#scala.Tuple2) [purescript-tuples/Data.Tuple](https://pursuit.purescript.org/packages/purescript-tuples/docs/Data.Tuple), [UniMath](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/Limits/Products.v), [nLab](https://ncatlab.org/nlab/show/cartesian+product) ### These diff --git a/README.md b/README.md index af27727f..2dc1a88a 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ [![Scala CI](https://github.com/lemastero/scala_typeclassopedia/actions/workflows/scala.yml/badge.svg?branch=main)](https://github.com/lemastero/scala_typeclassopedia/actions/workflows/scala.yml?query=branch%3Amain) -[![Scala Steward badge](https://img.shields.io/badge/Scala_Steward-helping-brightgreen.svg?style=flat&logo=data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAA4AAAAQCAMAAAARSr4IAAAAVFBMVEUAAACHjojlOy5NWlrKzcYRKjGFjIbp293YycuLa3pYY2LSqql4f3pCUFTgSjNodYRmcXUsPD/NTTbjRS+2jomhgnzNc223cGvZS0HaSD0XLjbaSjElhIr+AAAAAXRSTlMAQObYZgAAAHlJREFUCNdNyosOwyAIhWHAQS1Vt7a77/3fcxxdmv0xwmckutAR1nkm4ggbyEcg/wWmlGLDAA3oL50xi6fk5ffZ3E2E3QfZDCcCN2YtbEWZt+Drc6u6rlqv7Uk0LdKqqr5rk2UCRXOk0vmQKGfc94nOJyQjouF9H/wCc9gECEYfONoAAAAASUVORK5CYII=)](https://scala-steward.org) +[![Scala Steward badge](https://img.shields.io/badge/Scala_Steward-helping-brightgreen.svg?style=flat&logo=data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAA4AAAAQCAMAAAARSr4IAAAAVFBMVEUAAACHjojlOy5NWlrKzcYRKjGFjIbp293YycuLa3pYY2LSqql4f3pCUFTgSjNodYRmcXUsPD/NTTbjRS+2jomhgnzNc223cGvZS0HaSD0XLjbaSjElhIr+AAAAAXRSTlMAQObYZgAAAHlJREFUCNdNyosOwyAIhWHAQS1Vt7a77/3fcxxdmv0xwmckutAR1nkm4ggbyEcg/wWmlGLDAA3oL50xi6fk5ffZ3E2E3QfZDCcCN2YtbEWZt+Drc6u6rlqv7Uk0LdKqqr5rk2UCRXOk0vmQKGfc94nOJyQjouF9H/wCc9gECEYfONoAAAAASUVORK5CYII=)](https://github.com/scala-steward-org/scala-steward) # Scala typeclassopedia @@ -284,7 +284,6 @@ classDiagram * (Haskell) Haskell libraries containing abstractions from category theory written by Edward Kmett: [Profunctors](https://hackage.haskell.org/package/profunctors/docs/Data-Profunctor.html), [Bifunctors](https://hackage.haskell.org/package/bifunctors), [Comonad](https://hackage.haskell.org/package/comonad), [free](https://hackage.haskell.org/package/free), [adjunctions](https://hackage.haskell.org/package/adjunctions), [Kan extensions](https://hackage.haskell.org/package/kan-extensions), [invariant](https://hackage.haskell.org/package/invariant), [distributive](https://hackage.haskell.org/package/distributive), [transformers](https://hackage.haskell.org/package/transformers), [semigroupoids](https://hackage.haskell.org/package/semigroupoids). This is how all of this was started :) Some of them were already moved into Haskell standard library e.g. [Data.Functor.Contravariant](https://hackage.haskell.org/package/base/docs/Data-Functor-Contravariant.html) * [zio-prelude](https://github.com/zio/zio-prelude) modern look at abstractions from category theory, more modular and expressive -* (Kotlin) [Patterns from Category Theory in Kotlin](https://arrow-kt.io/docs/) * (Idris) [statebox/idris-ct](https://github.com/statebox/idris-ct) encoding of abstractions & formal verification in Idris 2 * Functional Structures in Scala - Michael Pilquist [(video playlist)](https://www.youtube.com/watch?v=Dsd4pc99FSY&list=PLFrwDVdSrYE6dy14XCmUtRAJuhCxuzJp0): workshop on [implementating FP constructions](https://github.com/mpilquist/Structures) with usage examples and great insights about Scala and FP. * Applied functional type theory - Sergei Winitzki [(video playlist)](https://www.youtube.com/watch?v=0Ld79Lnzx_o&list=PLcoadSpY7rHXJWbUkjQ3P9MXBbXxLP8kV) diff --git a/Topos.md b/Topos.md index 6627dc13..e1d600d9 100644 --- a/Topos.md +++ b/Topos.md @@ -14,11 +14,11 @@ Elementary topos is a category that: Resources: * vpatryshev/Categories [Topos](https://github.com/vpatryshev/Categories/blob/master/scala2/src/main/scala/math/cat/topos/Topos.scala) [Grothendieck Topos, Subobject Classifier](https://github.com/vpatryshev/Categories/blob/master/scala2/src/main/scala/math/cat/topos/GrothendieckTopos.scala), [Topology](https://github.com/vpatryshev/Categories/blob/master/scala2/src/main/scala/math/cat/topos/Topology.scala), [Lawvere-Tierney topology](https://github.com/vpatryshev/Categories/blob/master/scala2/src/main/scala/math/cat/topos/LawvereTopology.scala) - * (Agda) agda/agda-categories [Topos](https://github.com/agda/agda-categories/blob/master/Categories/Category/Topos.agda) [Subobject Classifier](https://github.com/agda/agda-categories/blob/master/Categories/Diagram/SubobjectClassifier.agda) - * (Coq) UniMath/UniMath [Grothendieck Topos](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/GrothendieckTopos.v) [Subobject Classifier](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/SubobjectClassifier.v) + * (Agda) agda/agda-categories [Topos](https://github.com/agda/agda-categories/blob/master/src/Categories/Category/Topos.agda) [Subobject Classifier](https://github.com/agda/agda-categories/blob/master/src/Categories/Diagram/SubobjectClassifier.agda) + * (Coq) UniMath/UniMath [Grothendieck Topos](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/GrothendieckToposes/Toposes.v) [Subobject Classifier](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/SubobjectClassifier/SubobjectClassifier.v) * (Haskell) [brunjlar/protop](https://github.com/brunjlar/protop) * Category Theory for Computing Science - Michael Barr Charles Wells [(pdf)](http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf) Chapter 15 Toposes - * 7Sketches Chapter 7 Logic of behavior: Sheaves, toposes, and internal languages [(pdf)](http://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf), [(video 1)](https://www.youtube.com/watch?v=Cf3tsAeGhBg), [(video 2)](https://www.youtube.com/watch?v=wF-khda2i4c) + * 7Sketches Chapter 7 Logic of behavior: Sheaves, toposes, and internal languages [(arxiv)](https://arxiv.org/abs/1803.05316), [(video 1)](https://www.youtube.com/watch?v=Cf3tsAeGhBg), [(video 2)](https://www.youtube.com/watch?v=wF-khda2i4c) * (Category Theory, Haskell) Topoi - Bartosz Milewski [(blog post)](https://bartoszmilewski.com/2017/07/22/topoi/) * Category Theory: Toposes - MathProofsable [(video playlist)](https://www.youtube.com/watch?v=gKYpvyQPhZo&list=PL4FD0wu2mjWM3ZSxXBj4LRNsNKWZYaT7k) * Computational Quadrinitarianism (Curious Correspondences go Cubical) - Gershom Bazerman [(blog post)](http://comonad.com/reader/2018/computational-quadrinitarianism-curious-correspondences-go-cubical/)