Lemma
Associating left and then right is like doing nothing.
assocLR : (x : (a * b) * c) -> assocR (assocL x) === x assocLR ((xa && xb) && xc) = Refl
Lemma
Associating left and then right is like doing nothing.
assocRL : (x : a * (b * c)) -> assocL (assocR x) === x assocRL (xa && (xb && xc)) = Refl
Lemma
Associativity of product forms an isomorphism.
assocIso : (a * (b * c)) ≅ ((a * b) * c) assocIso = MkIso assocR assocL assocLR assocRL