<div dir="ltr"><div>Disclaimer: X-posted on Stack Overflow: <a href="https://stackoverflow.com/questions/61877871/agda-constructing-a-recursive-record-value">https://stackoverflow.com/questions/61877871/agda-constructing-a-recursive-record-value</a></div><div><br></div><div>I'm wondering, is it possible to have records whose *values* depend on each other, without being recursively defined in terms of types?</div><div><br></div><div>Basically, I have a record type that looks like this:</div><div><br></div><div>record SomeRec (a : Set) : Set where</div><div>   method1 : a -> a -> Foo</div><div>   method2 : a -> a -> Bar</div><div>  ...</div><div>  method n : a -> a -> Baz</div><div><br></div><div>where n is large enough that I want to actually bundle all of these up as records, instead of just having a bunch of mutually recursive functions. (Also, I'm using SomeRec as an instance argument).</div><div><br></div><div>Notably, SomeRec is not recursive: none of its fields types refer to SomeRec.<br></div><div><br></div><div>Right now, I have a Description D, where FD : Set -> Set is the functor described by D. What I'm trying to show is the following:</div><div><br></div><div>  muRec : ( FRec : (a : Set) -> SomeRec a -> SomeRec (FD a) ) -> SomeRec (mu D)</div><div><br></div><div>That is, if I can take a (SomeRec a) to a (SomeRec (F a)), then I can tie the knot recursively and show the instance for the whole thing.</div><div><br></div><div>In principle this can be done: each recursive call to a field of SomeRec would happen with strictly smaller arguments. If I were to just have 10 mutually recursive methods, it would work. But if I try to build the record, I end up passing muRec to FRec *without its arguments decreasing*.<br></div><div><br></div><div>So, what I'm wondering is: is there a way to show that this is well-founded? Can induction or coinduction help, even though the record type is not inductive or coinductive?<br></div><div><br></div><div>My current approach is to make a size-indexed version of D, and build SomeRec for size n out of SomeRec for size < n. But this is dramatically increasing the complexity of what I'm doing, and I'm having to use Brouwer ordinals to get size bounds on what I'm doing. So I'm wondering if there's a better way.<br></div><div><br></div><div>Thanks!<br></div></div>