Library UniMath.Foundations.Tests

Require Export UniMath.Foundations.PartD.

Goal ∑ (_:nat) (_:nat) (_:nat) (_:nat), nat. exact (2,,3,,4,,5,,6). Defined.
Goal ∏ i j k, i+j+k = (i+j)+k. intros. apply idpath. Defined.
Goal ∏ n, 1+n = S n. intros. apply idpath. Defined.
Goal ∏ i j k, i×j×k = (i×j)*k. intros. apply idpath. Defined.
Goal ∏ n, 0×n = 0. intros. apply idpath. Defined.
Goal ∏ n, 0+n = n. intros. apply idpath. Defined.
Goal ∏ n, 0×n = 0. intros. apply idpath. Defined.
Goal ∏ n m, S n × m = n×m + m. intros. apply idpath. Defined.
Goal ∏ n, 1×n = n. intros. apply idpath. Defined.
Goal ∏ n, 4×n = n+n+n+n. intros. apply idpath. Defined.
Goal ∏ X x, idweq X x = x. intros. apply idpath. Defined.

Section Test_isweq_iso.
  Let f := idfun nat.
  Let w : nat ≃ nat := weq_iso f f (λ _, idpath _) (λ _, idpath _).
  Goal homotinvweqweq w 3 = idpath _. apply idpath. Defined.
  Goal homotweqinvweq w 3 = idpath _. apply idpath. Defined.
  Goal homotweqinvweqweq w 3 = idpath _. apply idpath. Defined.

  Definition v : bool ≃ bool.
    simple refine (weq_iso negb negb _ _); intro x; induction x; apply idpath. Defined.
  Goal homotinvweqweq v true = idpath _. apply idpath. Defined.
  Goal homotweqinvweq v true = idpath _. apply idpath. Defined.
  Goal homotweqinvweqweq v true = idpath _. apply idpath. Defined.
End Test_isweq_iso.

Goal ∏ X x, invweq (idweq X) x = x. intros. apply idpath. Defined.

Section Test_weqtotal2overcoprod.
  Let P (t : bool ⨿ bool) := nat.
  Goal weqtotal2overcoprod P (ii1 true,,3) = ii1 (true,,3). apply idpath. Defined.
  Goal weqtotal2overcoprod P (ii2 false,,3) = ii2 (false,,3). apply idpath. Defined.
  Goal invmap (weqtotal2overcoprod P) (ii1 (true,,3)) = ii1 true,,3. apply idpath. Defined.
  Goal invmap (weqtotal2overcoprod P) (ii2 (false,,3)) = ii2 false,,3. apply idpath. Defined.
End Test_weqtotal2overcoprod.

Goal weqcoprodf (idweq nat) (idweq nat) (ii1 3) = ii1 3. apply idpath. Defined.
Goal weqcoprodf (idweq nat) (idweq nat) (ii2 3) = ii2 3. apply idpath. Defined.
Goal invmap (weqcoprodf (idweq nat) (idweq nat)) (ii1 3) = ii1 3. apply idpath. Defined.
Goal invmap (weqcoprodf (idweq nat) (idweq nat)) (ii2 3) = ii2 3. apply idpath. Defined.

Goal bool_to_type true = unit . apply idpath. Defined.
Goal bool_to_type false = empty. apply idpath. Defined.

Goal @weqfibtototal bool _ _ (λ _, idweq bool) (true,,true) = (true,,true).
  apply idpath. Defined.
Goal invmap (@weqfibtototal bool _ _ (λ _, idweq bool)) (true,,true) = (true,,true).
  apply idpath. Defined.

Goal @weqfp_map nat nat (idweq _) (λ _,nat) (3,,4) = (3,,4). apply idpath. Defined.
Goal @weqfp_map _ _ boolascoprod (λ _,nat) (ii1 tt,,4) = (true,,4). apply idpath. Defined.

Goal @weqfp_invmap nat nat (idweq _) (λ _,nat) (3,,4) = (3,,4). apply idpath. Defined.
Goal @weqfp_invmap _ _ boolascoprod (λ _,nat) (true,,4) = (ii1 tt,,4). apply idpath. Defined.

Goal weqfp (idweq nat) (λ _,nat) (3,,4) = (3,,4). apply idpath. Defined.
Goal invmap (weqfp (idweq nat) (λ _,nat)) (3,,4) = (3,,4). apply idpath. Defined.

Goal weqtotal2overunit (λ _,nat) (tt,,3) = 3. apply idpath. Defined.
Goal invmap (weqtotal2overunit (λ _,nat)) 3 = (tt,,3). apply idpath. Defined.

Goal iscontr = isofhlevel 0. apply idpath. Defined.
Goal isaset = isofhlevel 2. apply idpath. Defined.

Require UniMath.Foundations.Sets.

Module Test_sets.

  Import UniMath.Foundations.Sets.

  Goal ∏ Y (is:isaset Y) (F:Y→UU) (e :∏ y y', F y → F y' → y=y')
         y (f:F y), squash_pairs_to_set F is e (hinhpr (y,,f)) = y.
  Proof.
    intros. apply idpath.
  Qed.

  Goal ∏ X Y (is:isaset Y) (f:X→Y) (e:∏ x x', f x = f x'),
         f = funcomp hinhpr (squash_to_set is f e).
  Proof.
    intros. apply idpath.
  Qed.

End Test_sets.