Definition θ_subset {B C:category} {F : [B, C]} {X : [B, [C^op, HSET]]} (t u : F ⟹ X) : pr1 t = pr1 u -> t = u. Proof. apply subtypePath. intros x. apply impred; intro b;apply impred; intro b'; apply impred; intro f. apply setproperty. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.RepresentableFunctors.Precategories. Require Import UniMath.MoreFoundations.Tactics.