{A} (f : A -> V) : forall (x y : A), f x = f y <~> ker_bisim f x y. Proof. intros; apply bisimulation_equiv_id. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.