Definition Subposet_to_Subposet' {X:Poset} : Subposet X -> Subposet' X. Proof. intros S. use tpair. - exists (carrier_subset S). use tpair. + intros s t. exact (pr1 s ≤ pr1 t)%poset. + simpl. split. { split. { intros s t u. exact (istrans_posetRelation _ _ _ _). } { intros s. exact (isrefl_posetRelation _ _). } } { intros s t a b. apply subtypePath_prop. exact (isantisymm_posetRelation _ _ _ a b). } - simpl. use tpair. + exists (pr1carrier _). intros s t a. simpl in s,t. exact a. + simpl. apply isinclpr1carrier. Defined.