I am interested in coinduction since I see it crop up in various ways in the subject of higher category theory. But I don't even know where to begin learning about coinduction, particularly from the point of view of (higher) category theory. I checked the references of the related wikipedia page and found the book "Introduction to Bisimulation and Coinduction" by Davide Sangiorgi. But this book seems to have a focus on coinduction in computer science. Lack of any other recommendations, this is what I'll read through. But, I thought I'd ask for a reference request here to see what others recommend.
Let me explain my interest in coinduction and then my background. I got interested in coinduction due to my interest in higher category theory and the use of type theory to do higher category theory synthetically. I occasionally see coinductive definitions in this area. For example, the definition of equivalence on Eric Finster's website "opetopic.net" is coinductive. In a lecture by the same author, he points out that coinduction is important in making sense of opetopic categories and opetopic type theory. Additionally, the notion of $\infty$-isomorphism (or equivalence) is coinductive in the sense that two objects of an $\infty$-groupoid are isomorphic iff there exists back and forth maps such that the composites of these maps are isomorphic to the identity map. This is informally explained by Awodey in his paper "Univalence as a Principle of Logic".
These are the particular things that got me interested in coinduction: I want to be able to more rigorously understand these definitions. So, I would love a resource on coinduction that has some overlap in this area, though I know that may be hard to find.
As for my background: I have no background in computer science so CS oriented resources are not for me. I do have familiarity with type theory (mostly with HoTT) and inductive types in this context. The book does not mention coinduction, at least not in the index or any section that I have read. I have a fairly good understanding of category theory, though I wish I had a better understanding of how inductive types are given categorical semantics.
P.S. - though not directly related to higher category theory, I include in this tag in hopes that someone from this community familiar with coinduction has a good recommendation.