Alex Gryzlov

Ok I think I'm done with `Smallstep`, gonna start with `Types` next.

As a reminder, we should try replacing `rewrite`s with dependent pattern matching where appropriate.

Look for places where **match application** (http://docs.idris-lang.org/en/latest/reference/misc.html#match-application) could be introduced/used. Maybe we could fix some of the bigger `replace`s with it?

Looks reasonable except for the explicit `implementation`, I find it too verbose :)

So should we just replace it with `\subsection` everywhere or you still hope to find a proper solution?

Yeah, I could spend a bit more time to special-case it.

I'm not sure where are you using `Singleton`, but there's an interface for such things in `contrib`: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Interfaces/Proposition.idr

Blodwen is now deprecated so I removed it from the title

Issues encountered: * ~~`Basic.Functor.functorEq` doesn’t typecheck~~ (solved by explicitly using heterogenous equality) * `Idris.TypesAsCategory.typesAsCategory` insists on `compose` being (partially) eta-expanded, i.e. only `\a => compose a` and more verbose variants...

Pushed https://github.com/statebox/idris-ct/tree/idris2