In addition to CT's application to commutative algebra, it's pretty nice for reasoning about programs and logic.

Programs: http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen..., https://blog.sumtypeofway.com/posts/introduction-to-recursio..., the Functor/Applicative/Monad hierarchy in Haskell et al

Logic: https://publish.uwo.ca/~jbell/catlogprime.pdf

CT as a bridge between programs and logic: https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...