From 8ff9089d3d8584f0551ea5097d15b20a0f07cd20 Mon Sep 17 00:00:00 2001
From: Niels <nmvdw@ip-145-116-140-226.wlan-int.ru.nl>
Date: Mon, 31 Jul 2017 14:52:41 +0200
Subject: [PATCH] Added disjunction.

---
 FiniteSets/_CoqProject   |  1 +
 FiniteSets/disjunction.v | 69 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 70 insertions(+)
 create mode 100644 FiniteSets/disjunction.v

diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index fb31360..9990301 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -1,6 +1,7 @@
 -R . "" COQC = hoqc COQDEP = hoqdep
 -R ../prelude ""
 definition.v
+disjunction.v
 operations.v
 Ext.v
 properties.v
diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v
new file mode 100644
index 0000000..5775d8f
--- /dev/null
+++ b/FiniteSets/disjunction.v
@@ -0,0 +1,69 @@
+Require Import HoTT.
+
+Definition lor (X Y : hProp) : hProp := BuildhProp (Trunc (-1) (sum X Y)).
+
+Infix "\/" := lor.
+
+Section lor_props.
+  Variable X Y Z : hProp.
+  Context `{Univalence}.
+
+  Theorem lor_assoc : (X \/ (Y \/ Z)) = ((X \/ Y) \/ Z).
+  Proof.
+    apply path_iff_hprop ; cbn.
+    * simple refine (Trunc_ind _ _).
+      intros [x | yz] ; cbn.
+      + apply (tr (inl (tr (inl x)))).
+      + simple refine (Trunc_ind _ _ yz).
+        intros [y | z].
+        ++ apply (tr (inl (tr (inr y)))). 
+        ++ apply (tr (inr z)).
+    * simple refine (Trunc_ind _ _).
+      intros [xy | z] ; cbn.
+      + simple refine (Trunc_ind _ _ xy).
+        intros [x | y].
+        ++ apply (tr (inl x)). 
+        ++ apply (tr (inr (tr (inl y)))).
+      + apply (tr (inr (tr (inr z)))).
+  Defined.
+
+  Theorem lor_comm : (X \/ Y) = (Y \/ X).
+  Proof.
+    apply path_iff_hprop ; cbn.
+    * simple refine (Trunc_ind _ _).
+      intros [x | y].
+      + apply (tr (inr x)).
+      + apply (tr (inl y)).
+    * simple refine (Trunc_ind _ _).
+      intros [y | x].
+      + apply (tr (inr y)).
+      + apply (tr (inl x)).
+  Defined.
+
+  Theorem lor_nl : (False_hp \/ X) = X.
+  Proof.
+    apply path_iff_hprop ; cbn.
+    * simple refine (Trunc_ind _ _).
+      intros [ | x].
+      + apply Empty_rec.
+      + apply x.
+    * apply (fun x => tr (inr x)).
+  Defined.
+
+  Theorem lor_nr : (X \/ False_hp) = X.
+  Proof.
+    apply path_iff_hprop ; cbn.
+    * simple refine (Trunc_ind _ _).
+      intros [x | ].
+      + apply x.
+      + apply Empty_rec.
+    * apply (fun x => tr (inl x)).
+  Defined.
+
+  Theorem lor_idem : (X \/ X) = X.
+  Proof.
+    apply path_iff_hprop ; cbn.
+    - simple refine (Trunc_ind _ _).
+      intros [x | x] ; apply x.
+    - apply (fun x => tr (inl x)).
+  Defined.
\ No newline at end of file