Require Import
  HoTT.Classes.interfaces.abstract_algebra.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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)))%type
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))%type
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))%type
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)))%type
-
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)))%type 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))%type 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))%type 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)))%type destruct (trichotomy _ b1 b2) as [?|[?|?]];auto.
Defined.

End contents.