(S : Type) : pType := [S + Unit, inr tt]. Global Instance is0functor_pointify : Is0Functor . Proof. apply Build_Is0Functor. intros A B f. srapply Build_pMap. 1: exact (functor_sum f idmap). reflexivity. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.