{A B C : pType} (f : A <~>* B) (g : B <~>* C) : A <~>* C := g $oE f. Global Instance pequiv_transitive : Transitive pEquiv. Proof. intros ? ? ?; apply . Defined.
Require Import Basics. Require Import Types. Require Import WildCat. Require Import Pointed.Core.