namespace http://mathhub.info/MitM/core/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚

/T MiKo: a first-order approximation of a view from POSet to PowerSet
   eventually, we want to push filter and co out over this to get the 
   usual applications of filters ❚

theory ASet : base:?Logic =
   include ?PowerSet ❙
   include ?BasicLemmata ❙
   A : type ❙
 ❚

theory PowersetPOSet : base:?Logic =
	include ?POSet ❙

	view PowersetIsPOSet : ?POSet/poset_theory -> ?ASet =
    	universe = set A ❙
    	ord = [S,T] subset A S T ❙
    	axiom_reflexive = lemma_subsetReflexive ❙
    	axiom_transitive = lemma_subsetTransitive ❙
    	axiom_antisymmetric = lemma_subsetAntisymmetric ❙
    ❚
❚