📥 Auto-inserting .fib projections when the fib field is a record

[mmcqd]

Once #361 gets merged, I want to consider ways to auto-insert .fib projections even in the case where the fib field is a record. This becomes a problem as soon as you try formalize functors as a type family indexed by a signature of two categories. The resulting total space has a fib field that's a record, so any definition involving functors involves writing down a lot of .fib. I can see two simple ways to do this:

1. Add a special syntax for projecting the non-fib fields from a total space. I actually kind of like @ for this, but don't have strong feelings. Then we'd have

   e : total-space |- e @ lbl ~> e.lbl
   
   e : total-space |- e.lbl ~> e.fib.lbl
   
   e : sig (x : ...) (y : ...) |- e @ lbl ~> ERROR
   

   This avoids ambiguity but might be annoying to write down, having to remember what fields need @ and what fields need .

2. Check if the field being projected is in the structure the user is trying to project from, if it's not, then try eliminating a total space and try again. Then we'd have

   e : sig (lbl : ...) (fib : ...) |- e.lbl ~> e.lbl
   
   e : sig (x : ...) (fib : ...) |- e.lbl ~> e.fib.lbl
   
   e : sig (x : ...) (y : ...) | e.lbl ~> ERROR (as normal)
   

   This is convenient for the user, but makes the elaboration process less elegant and is potentially confusing when reading code (what fields does this thing actually have?).

I lean towards (2), but am open to either.