I'm sympathetic, but I don't agree about the comparison to vector spaces because a cleaving is nothing like a basis. My evidence for this is that for fibrations of univalent categories, cleavings are always canonical; on the other hand, there is no foundational tweak that could make vector spaces have canonical bases.
I agree that from a univalent point of view all cleavages are equal. But from a univalent point of view all cleavages are even split! That is a bit too much for me (see Warning (1) on p.10 of my notes on fibered cats). But I do not want to take up old discussions! I really prefer to disagree. Instead I admit that all choices of cleavages are uniquely isomorphic which certainly is not teh case for bases. Thomas ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27