Require ImportRequire Import
  HoTT.Classes.interfaces.abstract_algebra.

Generalizable Variables A B.

Instance Empty_lt : Lt@{Set Set} Empty.
Lt Empty
Proof.
Lt Empty intros []. Defined.

Instance Unit_lt : Lt@{Set Set} Unit := fun _ _ => Empty.

Instance empty_tricho : Trichotomy@{Set Set Set} (_:Lt Empty).
Trichotomy (Empty_lt : Lt Empty)
Proof.
Trichotomy (Empty_lt : Lt Empty)
intros [].
Qed.

Instance unit_tricho : Trichotomy@{Set Set Set} (_:Lt Unit).
Trichotomy (Unit_lt : Lt Unit)
Proof.
Trichotomy (Unit_lt : Lt Unit)
intros [] [];auto.
Defined.

Section contents.

Context `{Alt : Lt@{Set Set} A} `{Blt : Lt@{Set Set} B}.

#[export] Instance sum_lt : Lt@{Set Set} (A |_| B) | 2
  := fun s1 s2 =>
  match s1, s2 with
  | inl a1, inl a2 => a1 < a2
  | inr b1, inr b2 => b1 < b2
  | inl _, inr _ => Unit
  | inr _, inl _ => Empty
  end.

#[export] Instance sum_tricho `{!Trichotomy@{Set Set Set} Alt} `{!Trichotomy@{Set Set Set} Blt}
  : Trichotomy@{Set Set Set} sum_lt.
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
Trichotomy sum_lt
Proof.
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
Trichotomy sum_lt
hnf.
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
forall x y : A + B, sum_lt x y + ((x = y) + sum_lt y x) intros [a1|b1] [a2|b2];simpl.
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
a1, a2: A
(a1 < a2) + ((inl a1 = inl a2) + (a2 < a1))
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
a1: A
b2: B
Unit + ((inl a1 = inr b2) + Empty)
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
b1: B
a2: A
Empty + ((inr b1 = inl a2) + Unit)
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
b1, b2: B
(b1 < b2) + ((inr b1 = inr b2) + (b2 < b1))
-
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
a1, a2: A
(a1 < a2) + ((inl a1 = inl a2) + (a2 < a1)) destruct (trichotomy _ a1 a2) as [?|[?|?]];auto.
-
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
a1: A
b2: B
Unit + ((inl a1 = inr b2) + Empty) auto.
-
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
b1: B
a2: A
Empty + ((inr b1 = inl a2) + Unit) auto.
-
A: Type0
Alt: Lt A
B: Type0
Blt: Lt B
Trichotomy0: Trichotomy Alt
Trichotomy1: Trichotomy Blt
b1, b2: B
(b1 < b2) + ((inr b1 = inr b2) + (b2 < b1)) destruct (trichotomy _ b1 b2) as [?|[?|?]];auto.
Defined.

End contents.