Proposition prod_dcpo_basis_laws : dcpo_basis_laws (X × Y) prod_dcpo_basis_data. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal.