Unset Kernel Term Sharing.

Require Export UniMath.Algebra.BinaryOperations.
Require Import UniMath.Foundations.Propositions.

Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.DecidablePropositions.

Lemma isapropisirrefl {X : UU} (rel : hrel X) :
  isaprop (isirrefl rel).
Proof.
  apply impred_isaprop ; intro.
  now apply isapropneg.
Qed.
Lemma isapropissymm {X : UU} (rel : hrel X) :
  isaprop (issymm rel).
Proof.
  apply impred_isaprop ; intro x.
  apply impred_isaprop ; intro y.
  apply isapropimpl.
  now apply pr2.
Qed.
Lemma isapropiscotrans {X : UU} (rel : hrel X) :
  isaprop (iscotrans rel).
Proof.
  apply impred_isaprop ; intro x.
  apply impred_isaprop ; intro y.
  apply impred_isaprop ; intro z.
  apply isapropimpl.
  now apply pr2.
Qed.

Definition isaprel {X : UU} (ap : hrel X) :=
  isirrefl ap × issymm ap × iscotrans ap.

Lemma isaprop_isaprel {X : UU} (ap : hrel X) :
  isaprop (isaprel ap).
Proof.
  apply isapropdirprod.
  apply isapropisirrefl.
  apply isapropdirprod.
  apply isapropissymm.
  apply isapropiscotrans.
Qed.

Definition aprel (X : UU) := ∑ ap : hrel X, isaprel ap.
Definition aprel_pr1 {X : UU} (ap : aprel X) : hrel X := pr1 ap.
Coercion aprel_pr1 : aprel >-> hrel.

Definition apSet := ∑ X : hSet, aprel X.
Definition apSet_pr1 (X : apSet) : hSet := pr1 X.
Coercion apSet_pr1 : apSet >-> hSet.
Arguments apSet_pr1 X: simpl never.
Definition apSet_pr2 (X : apSet) : aprel X := pr2 X.
Notation "x # y" := (apSet_pr2 _ x y) : ap_scope.

Delimit Scope ap_scope with ap.
Local Open Scope ap_scope.

Lemma isirreflapSet {X : apSet} :
  ∏ x : X, ¬ (x # x).
Proof.
  exact (pr1 (pr2 (pr2 X))).
Qed.

Lemma issymmapSet {X : apSet} :
  ∏ x y : X, x # y → y # x.
Proof.
  exact (pr1 (pr2 (pr2 (pr2 X)))).
Qed.

Lemma iscotransapSet {X : apSet} :
  ∏ x y z : X, x # z → x # y ∨ y # z.
Proof.
  exact (pr2 (pr2 (pr2 (pr2 X)))).
Qed.
Close Scope ap_scope.

Definition istight {X : UU} (R : hrel X) :=
  ∏ x y : X, ¬ (R x y) → x = y.
Definition istightap {X : UU} (ap : hrel X) :=
  isaprel ap × istight ap.

Definition tightap (X : UU) := ∑ ap : hrel X, istightap ap.
Definition tightap_aprel {X : UU} (ap : tightap X) : aprel X := pr1 ap ,, (pr1 (pr2 ap)).
Coercion tightap_aprel : tightap >-> aprel.

Definition tightapSet := ∑ X : hSet, tightap X.
Definition tightapSet_apSet (X : tightapSet) : apSet := pr1 X ,, (tightap_aprel (pr2 X)).
Coercion tightapSet_apSet : tightapSet >-> apSet.

Definition tightapSet_rel (X : tightapSet) : hrel X := (pr1 (pr2 X)).
Notation "x ≠ y" := (tightapSet_rel _ x y) (at level 70, no associativity) : tap_scope.

Delimit Scope tap_scope with tap.
Local Open Scope tap_scope.

Lemma isirrefltightapSet {X : tightapSet} :
  ∏ x : X, ¬ (x ≠ x).
Proof.
  exact isirreflapSet.
Qed.

Lemma issymmtightapSet {X : tightapSet} :
  ∏ x y : X, x ≠ y → y ≠ x.
Proof.
  exact issymmapSet.
Qed.

Lemma iscotranstightapSet {X : tightapSet} :
  ∏ x y z : X, x ≠ z → x ≠ y ∨ y ≠ z.
Proof.

  exact iscotransapSet.
Qed.

Lemma istighttightapSet {X : tightapSet} :
  ∏ x y : X, ¬ (x ≠ y) → x = y.
Proof.
  exact (pr2 (pr2 (pr2 X))).
Qed.

Lemma istighttightapSet_rev {X : tightapSet} :
  ∏ x y : X, x = y → ¬ (x ≠ y).
Proof.
  intros x _ <-.
  now apply isirrefltightapSet.
Qed.

Lemma tightapSet_dec {X : tightapSet} :
  LEM → ∏ x y : X, (x != y ↔ x ≠ y).
Proof.
  intros Hdec x y.
  destruct (Hdec (x ≠ y)) as [ Hneq | Heq ].
  - split.
    + intros _ ; apply Hneq.
    + intros _ Heq.
      rewrite <- Heq in Hneq.
      revert Hneq.
      now apply isirrefltightapSet.
  - split.
    + intros Hneq.
      apply fromempty, Hneq.
      now apply istighttightapSet.
    + intros Hneq.
      exact (fromempty (Heq Hneq)).
Qed.

Definition isapunop {X : tightapSet} (op :unop X) :=
  ∏ x y : X, op x ≠ op y → x ≠ y.
Lemma isaprop_isapunop {X : tightapSet} (op :unop X) :
  isaprop (isapunop op).
Proof.
  intros ap.
  apply impred_isaprop ; intro x.
  apply impred_isaprop ; intro y.
  apply isapropimpl.
  now apply pr2.
Qed.

Definition islapbinop {X : tightapSet} (op : binop X) :=
  ∏ x, isapunop (λ y, op y x).
Definition israpbinop {X : tightapSet} (op : binop X) :=
  ∏ x, isapunop (λ y, op x y).
Definition isapbinop {X : tightapSet} (op : binop X) :=
  (islapbinop op) × (israpbinop op).
Lemma isaprop_islapbinop {X : tightapSet} (op : binop X) :
  isaprop (islapbinop op).
Proof.
  apply impred_isaprop ; intro x.
  now apply isaprop_isapunop.
Qed.
Lemma isaprop_israpbinop {X : tightapSet} (op : binop X) :
  isaprop (israpbinop op).
Proof.
  apply impred_isaprop ; intro x.
  now apply isaprop_isapunop.
Qed.
Lemma isaprop_isapbinop {X : tightapSet} (op :binop X) :
  isaprop (isapbinop op).
Proof.
  intros ap.
  apply isapropdirprod.
  now apply isaprop_islapbinop.
  now apply isaprop_israpbinop.
Qed.

Definition apbinop (X : tightapSet) := ∑ op : binop X, isapbinop op.
Definition apbinop_pr1 {X : tightapSet} (op : apbinop X) : binop X := pr1 op.
Coercion apbinop_pr1 : apbinop >-> binop.

Definition apsetwithbinop := ∑ X : tightapSet, apbinop X.
Definition apsetwithbinop_pr1 (X : apsetwithbinop) : tightapSet := pr1 X.
Coercion apsetwithbinop_pr1 : apsetwithbinop >-> tightapSet.
Definition apsetwithbinop_setwithbinop : apsetwithbinop → setwithbinop :=
  λ X : apsetwithbinop, (apSet_pr1 (apsetwithbinop_pr1 X)),, (pr1 (pr2 X)).
Definition op {X : apsetwithbinop} : binop X := op (X := apsetwithbinop_setwithbinop X).

Definition apsetwith2binop := ∑ X : tightapSet, apbinop X × apbinop X.
Definition apsetwith2binop_pr1 (X : apsetwith2binop) : tightapSet := pr1 X.
Coercion apsetwith2binop_pr1 : apsetwith2binop >-> tightapSet.
Definition apsetwith2binop_setwith2binop : apsetwith2binop → setwith2binop :=
  λ X : apsetwith2binop,
        apSet_pr1 (apsetwith2binop_pr1 X),, pr1 (pr1 (pr2 X)),, pr1 (pr2 (pr2 X)).
Definition op1 {X : apsetwith2binop} : binop X := op1 (X := apsetwith2binop_setwith2binop X).
Definition op2 {X : apsetwith2binop} : binop X := op2 (X := apsetwith2binop_setwith2binop X).

Section apsetwithbinop_pty.

Context {X : apsetwithbinop}.

Lemma islapbinop_op :
  ∏ x x' y : X, op x y ≠ op x' y → x ≠ x'.
Proof.
  intros x y y'.
  now apply (pr1 (pr2 (pr2 X))).
Qed.

Lemma israpbinop_op :
  ∏ x y y' : X, op x y ≠ op x y' → y ≠ y'.
Proof.
  intros x y y'.
  now apply (pr2 (pr2 (pr2 X))).
Qed.

Lemma isapbinop_op :
  ∏ x x' y y' : X, op x y ≠ op x' y' → x ≠ x' ∨ y ≠ y'.
Proof.
  intros x x' y y' Hop.
  apply (iscotranstightapSet _ (op x' y)) in Hop.
  revert Hop ; apply hinhfun ; intros [Hop | Hop].
  - left ; revert Hop.
    now apply islapbinop_op.
  - right ; revert Hop.
    now apply israpbinop_op.
Qed.

End apsetwithbinop_pty.

Section apsetwith2binop_pty.

Context {X : apsetwith2binop}.

Definition apsetwith2binop_apsetwithbinop1 : apsetwithbinop :=
  (pr1 X) ,, (pr1 (pr2 X)).
Definition apsetwith2binop_apsetwithbinop2 : apsetwithbinop :=
  (pr1 X) ,, (pr2 (pr2 X)).

Lemma islapbinop_op1 :
  ∏ x x' y : X, op1 x y ≠ op1 x' y → x ≠ x'.
Proof.
  exact (islapbinop_op (X := apsetwith2binop_apsetwithbinop1)).
Qed.

Lemma israpbinop_op1 :
  ∏ x y y' : X, op1 x y ≠ op1 x y' → y ≠ y'.
Proof.
  exact (israpbinop_op (X := apsetwith2binop_apsetwithbinop1)).
Qed.

Lemma isapbinop_op1 :
  ∏ x x' y y' : X, op1 x y ≠ op1 x' y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (isapbinop_op (X := apsetwith2binop_apsetwithbinop1)).
Qed.

Lemma islapbinop_op2 :
  ∏ x x' y : X, op2 x y ≠ op2 x' y → x ≠ x'.
Proof.
  exact (islapbinop_op (X := apsetwith2binop_apsetwithbinop2)).
Qed.

Lemma israpbinop_op2 :
  ∏ x y y' : X, op2 x y ≠ op2 x y' → y ≠ y'.
Proof.
  exact (israpbinop_op (X := apsetwith2binop_apsetwithbinop2)).
Qed.

Lemma isapbinop_op2 :
  ∏ x x' y y' : X, op2 x y ≠ op2 x' y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (isapbinop_op (X := apsetwith2binop_apsetwithbinop2)).
Qed.

End apsetwith2binop_pty.

Close Scope tap_scope.