Merge branch 'master' into lists

code/Decidability/DiscreteTypes.v

@@ -1,4 +1,7 @@
 Require Import init.imports.
+Require Import UniMath.Combinatorics.Lists.
+Require Import UniMath.Combinatorics.MoreLists.
+Require Import Inductive.Option.
 
 Section EqualityDeciders.
 
@@ -138,12 +141,4 @@ Section ClosureProperties.
         * exact inr.
   Qed.
 
-
-
-
-End ClosureProperties.
-
-
-Section ChoiceFunction.
-
-End ChoiceFunction.
+End ClosureProperties.

code/Inductive/Option.v

@@ -1,5 +1,5 @@
-(* Definition of an option as the coproduct of a type X with the unit type *)
 
+(* Definition of an option as the coproduct of a type X with the unit type *)
 Require Import init.imports. 
 
 Section Option.
@@ -10,3 +10,23 @@ Section Option.
   Definition none {X : UU} : @option X := (ii2 tt).
 
 End Option.
+
+Section PathProperties.
+
+  Lemma nopathssomenone {X : UU} (x : X) : ¬ ((some x) = none). 
+  Proof.
+    apply negpathsii1ii2.
+  Qed.
+
+  Lemma nopathsnonesome {X : UU} (x : X) : ¬ (none = (some x)).
+  Proof.
+    apply negpathsii2ii1.
+  Qed.
+
+  Lemma some_injectivity {X : UU} (x y : X) : (some x = some y) → x = y.
+  Proof.
+    apply ii1_injectivity.
+  Qed.
+
+
+End PathProperties.

code/_CoqProject

@@ -2,11 +2,13 @@ COQC = coqc
 COQDEP = coqdep
 -R . "sem"
 
+
 -arg "-w -notation-overridden -type-in-type -noinit"
 
 init/imports.v
 init/all.v
 
+
 Inductive/ListProperties.v
 Inductive/Option.v