Related to @hejohns and I discussed in our meeting about operational logical relations, it would be nice to get a version of SET^D called POSET^D which would be displayed over Posets, where an object over a poset P would be either (1) a displayed poset or (2) a monotone function P^op -> Prop.
Related to @hejohns and I discussed in our meeting about operational logical relations, it would be nice to get a version of
SET^DcalledPOSET^Dwhich would be displayed over Posets, where an object over a posetPwould be either (1) a displayed poset or (2) a monotone functionP^op -> Prop.