Add a very rough draft of the idris catemorphisms article I found lying around

content/blog/idris_catamorphisms.md

@@ -0,0 +1,47 @@
+---
+title: "Induction Principles from Base Functors"
+date: 2022-04-22T12:19:22-07:00
+tags: ["Idris"]
+draft: true
+---
+In the [Haskell catamorphisms article]({{< relref "haskell_catamorphisms" >}}), we looked
+at how base functors and functions of the type `F a -> a` can be used to
+derive "fold" functions on inductive data types. This formulation allows for
+one more interesting trick, one that I found to be extremely interesting and
+worth covering. However, this trick requires a more powerful type system
+than Haskell provides us; it requires depdendent types.
+
+This article assumes a working knowledge of dependent types. I will not
+spend time explaining dependent types, nor the syntax for them in Idris,
+which is the language I'll use in this article. Below are a few resources
+that should help you get up to speed.
+
+{{< todo >}}List resources{{< /todo >}}
+
+We've seen that, given a function `F a -> a`, we can define a function
+`B -> a`, if `F` is a base functor of the type `B`. However, what if
+the goal is to define a function in which the return type `a` depends
+on the value of `B`? In other words, what if we want to define a function
+with type:
+```Idris
+someFunction : (b : B) -> P b
+```
+How might we achieve such a thing? Unlike the generic type `a`, we can't
+simply place `P` into the base functor `F`; the following is completely
+invalid.
+```Idris
+-- Completely bogus
+argType : Type
+argType = F P -> P
+```
+In our case, `P` is a type family, rather than a type; in order to use it as
+a parameter to the base functor, we need to feed it an argument (of type `B`).
+Well, we've already seen one way to get a value `b` of type `B` at the type
+level: we can use a dependent function. This too is not correct, but it does get us a little bit closer to the goal.
+```Idris
+-- Still bogus
+argType : Type
+argType = (b : B) -> F (P b) -> P b
+```
+Recall that the base functor `F` effectively denotes a single layer of a data
+structure, with recursive