From 4f6689a0964a952be1b41be54e6400a4d1f51d90 Mon Sep 17 00:00:00 2001 From: Pouya Date: Tue, 4 Aug 2026 03:23:25 +0100 Subject: [PATCH] mino --- draft/draft.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index 29debd5..52579e2 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -483,7 +483,7 @@ We want to say that a natural order structure entails an order over a functor de \begin{proof} $(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$. - Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$. + Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\sappr)}s$. $(II)$ Basically, by definition of $\op$ and relation composition we have \begin{gather*}