?? 2' : 1' :: grothendieck topology : lawvere-tierney topology ... ???

?? "lawvere-tierney topology" =?= "sub-canonical (????) grothendieck topology on grothendieck topos" ????.... ??? meaning of "sub-canonical" here as perhaps not so hard to remember now ... "geometric" meaning ... ?? ...

???compatibility between co-yoneda morphism and formula, vs between co-yoneda morphism and model, vs between formula and model ... ???? ..... ????? .....

formula as presheaf, model as co-presheaf ... tensoring gives "realization of formula in model" ... ???so a stretch to consider as "compatibility" ... unless you're into "categorify truth-value into set" ...??? .... ???...

??well, might actually be some funny but semi-plausible way to actually get truth-value here .... ???? ......

??? "generic model" ... as identity functor of formula category ... ???

???"tensoring" co-yoneda morphism with model-candidate co-presheaf ...compatible = "results in isomorphism" ... ??? .... ??? relationship to "implication" ... ??in topos case, but then more generally ??? ..... ???? ....

??? "auxiliary types" .... ???? ..... ???? ....

?? in "lawvere-tierney" situation, can use ordinary morphism realization of co-yoneda morphism, instead of co-yoneda morphism .... ????_is_ that ess what actual lawvere-tierney idea is using ??? ....

??various examples of theories ... old stand-bys ..."walking epi" ... "walking co-category" ... ???...

???presheaf on _finset_ that's finite-valued but not finitely presented ??? ... ?