proposition: Proposition prod_dcpo_basis_laws : dcpo_basis_laws (X × Y) prod_dcpo_basis_data.
proof: Proof. intros xy. split. - split. + assert (H := directed_set_el (directed_set_from_basis BX (pr1 xy))). revert H. use factor_through_squash. { apply propproperty. } intros a. induction a as [ a p ]. assert (H := directed_set_el (directed_set_from_basis BY (pr2 xy))). revert H. use factor_through_squash. { apply propproperty. } intros b. induction b as [ b q ]. refine (hinhpr ((a ,, b) ,, _)). use to_way_below_prod. * exact p. * exact q. + intros ij₁ ij₂. assert (H := directed_set_top (directed_set_from_basis BX (pr1 xy)) (pr11 ij₁ ,, way_below_prod_pr1 (pr2 ij₁)) (pr11 ij₂ ,, way_below_prod_pr1 (pr2 ij₂))). revert H. use factor_through_squash. { apply propproperty. } intros k. induction k as [ k [ p₁ p₂ ]]. assert (H := directed_set_top (directed_set_from_basis BY (pr2 xy)) (pr21 ij₁ ,, way_below_prod_pr2 (pr2 ij₁)) (pr21 ij₂ ,, way_below_prod_pr2 (pr2 ij₂))). revert H. use factor_through_squash. { apply propproperty. } intros l. induction l as [ l [ q₁ q₂ ]]. simple refine (hinhpr (((_ ,, _) ,, _) ,, (_ ,, _) ,, (_ ,, _))). * exact (pr1 k). * exact (pr1 l). * use to_way_below_prod. ** exact (pr2 k). ** exact (pr2 l). * exact p₁. * exact q₁. * exact p₂. * exact q₂. - use is_least_upperbound_pair. + split. * intros a. refine (is_least_upperbound_is_upperbound (is_least_upperbound_basis BX (pr1 xy)) (pr11 a ,, _)). apply (way_below_prod_pr1 (pr2 a)). * intros a Ha. apply (is_least_upperbound_is_least (is_least_upperbound_basis BX (pr1 xy))). intros b. assert (H := basis_nullary_interpolation BY (pr2 xy)). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ c p ]. simple refine (Ha ((pr1 b ,, c) ,, _)). use to_way_below_prod. ** exact (pr2 b). ** exact p. + split. * intros a. refine (is_least_upperbound_is_upperbound (is_least_upperbound_basis BY (pr2 xy)) (pr21 a ,, _)). apply (way_below_prod_pr2 (pr2 a)). * intros a Ha. apply (is_least_upperbound_is_least (is_least_upperbound_basis BY (pr2 xy))). intros b. assert (H := basis_nullary_interpolation BX (pr1 xy)). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ c p ]. simple refine (Ha ((c ,, pr1 b) ,, _)). use to_way_below_prod. ** exact p. ** exact (pr2 b). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Elements.Maximal