Record types are a common feature in most paradigms.
Agda also allows defining records with the coinductive keyword.
Lastly there are the seemingly more exotic co(inductive)data types which are kind of the duals of inductive types, in the sense that they're defined by projections rather than constructors.
What are the differences between all of these? Is one more powerful than the rest?
By reading your question, I believe that you are not looking for a very technical answer, but general ideas instead. If you would like to dig deeper, you can search with the keyword 'polarity' and 'later modality'.
I would say in Agda, coinductive records is a technique of implementing codata types. There are others, such as the Coq CoInductive and the Agda's old musical notations, and I believe they're all different ways to express the so-called "codatatypes". There is a subtle difference between coinductive records and Coq CoInductive, which I do not want to explain here.
Records in Agda are by default non-recursive, say, you may think of them as a named version of sigma types (so they have η-rules, etc.), but coinductive records are totally different, either in the semantic sense or in the typing rules of type theory. They have a special termination checker (the "productivity checker") and allows negativity. So, I would say, the two features look similar is only because the information you provide to define a record & a coinductive type is similar -- parameters, the universe it lives in, and a list of types with names which are fields for records and projections/copatterns for coinductive records.
I think the similarity is also due to the fact that sigma types is positive and negative at the same time (there are equivalent ways to define it, one positive and one negative), but still coinductive records are more complicated than negative sigma types.
