fact: Definition nat_equiv (x y : F ⟾ G) : Prop := match x with | Build_Natural _ _ _ _ transport0 _ => match y with | Build_Natural _ _ _ _ transport1 _ => forall {X}, transport0 X = transport1 X end end.
imports: Category