Equality in a Cartesian Fibration

Let $p:\mathcal{E}\rightarrowtriangle\mathcal{B}$ be a Cartesian Fibration over a Cartesian Category. We say that $p$ has simple equality if

• For each $\Gamma,A:\mathcal{B}$ and $X:\mathcal{E}_{\Gamma\times A}$ there is a Cocartesian Lift

• These cocartesian lifts satisfy a Beck-Chevalley Condition; for each square \[

  \begin{tikzcd}

&& Y &&& {Eq(Z)}
X &&& Z
&& {(Γ × A) × A} &&& {(Δ × A) × A}
{Γ × A} &&& {Δ × A} \end{tikzcd} \]

If the two red maps are Cartesian, then the blue map is Cocartesian.

Note that we should not think of equality as an equality type, but rather a sort of wonky "unquantifier" that duplicates a variable. EG: when we form $\mathrm{Eq}(P)\rightarrowtriangle(\Gamma\times A)\times A$ from $P\rightarrowtriangle\Gamma\times A$, we should think of this as turning $\Gamma,x:A\vdash P(x)\;\mathrm{true}$ into $\Gamma,x:A,y:A\vdash x=y\land P(y)\;\mathrm{true}$; the cocartesian map $\mathrm{refl}$ then says that we can prove $\Gamma,x:A\mid P(x)\vdash x=x\land P(x)\;\mathrm{true}$

If $\mathcal{E}$ has Fibred Terminal Objects, then we can get a notion of equality on morphisms $u,v:{{A}\to{B}}$ by base changing $\mathrm{Eq}(1):\mathcal{E}_{(A\times B)\times B}$ to $E_{A}$ along $\langle\langle mathrm{id}{ifx..lse\par i},u\rangle,v\rangle$. What this essentially does is turn the predicate $a:A,b:B\vdash\top\;\mathrm{true}$ into $a:A,b_{1}:B,b_{2}:B\vdash b_{1}=b_{2}\land\top\;\mathrm{true}$, and then Substitute away the $b_{1}$ and $b_{2}$ to get $a:A\vdash u(a)=v(a)\land\top\;\mathrm{true}$.