(A : Type) : O_functor O2 (to O1 A) o to O2 A == to O2 (O1 A) o to O1 A := to_O_natural O2 (to O1 A).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.