{A : Type} (F : A -> pType) : pType := [forall (a : A), pointed_type (F a), ispointed_type o F].
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.