feat(hott): more cleanup of HoTT library

remove funext class, remove a couple of sorry's, add characterization of equality in trunctypes, use Jeremy's format for headers everywhere in the HoTT library, continue working on Yoneda embedding
2015-02-26 13:19:54 -05:00 · 2015-02-26 13:19:54 -05:00 · f513538631
commit f513538631
parent c091acc55b
43 changed files with 488 additions and 413 deletions
--- a/hott/algebra/category/basic.hlean
+++ b/hott/algebra/category/basic.hlean
@ -1,33 +1,45 @@
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
+/-
+Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.

-import ..precategory.basic ..precategory.morphism ..precategory.iso
+Module: algebra.category.basic
+Author: Jakob von Raumer
+-/

-open precategory morphism is_equiv eq is_trunc nat sigma sigma.ops
+import algebra.precategory.iso

-- A category is a precategory extended by a witness,
-- that the function assigning to each isomorphism a path,
+open morphism is_equiv eq is_trunc
+
+-- A category is a precategory extended by a witness
+-- that the function from paths to isomorphisms,
 -- is an equivalecnce.
-structure category [class] (ob : Type) extends (precategory ob) :=
-  (iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
-
-attribute category [multiple-instances]
-
 namespace category
-  variables {ob : Type} {C : category ob} {a b : ob}
+
+  structure category [class] (ob : Type) extends parent : precategory ob :=
+    (iso_of_path_equiv : Π (a b : ob), is_equiv (@iso_of_path ob parent a b))
+
+  attribute category [multiple-instances]
+
+  abbreviation iso_of_path_equiv := @category.iso_of_path_equiv
+
+  definition category.mk' [reducible] (ob : Type) (C : precategory ob)
+    (H : Π (a b : ob), is_equiv (@iso_of_path ob C a b)) : category ob :=
+  precategory.rec_on C category.mk H
+
+  section basic
+  variables {ob : Type} [C : category ob]
  include C

  -- Make iso_of_path_equiv a class instance
  -- TODO: Unsafe class instance?
  attribute iso_of_path_equiv [instance]

-  definition path_of_iso {a b : ob} : a ≅ b → a = b :=
+  definition path_of_iso (a b : ob) : a ≅ b → a = b :=
  iso_of_path⁻¹

  set_option apply.class_instance false -- disable class instance resolution in the apply tactic

-  definition ob_1_type : is_trunc (succ nat.zero) ob :=
+  definition ob_1_type : is_trunc 1 ob :=
  begin
    apply is_trunc_succ_intro, intros (a, b),
    fapply is_trunc_is_equiv_closed,
@ -35,25 +47,27 @@ namespace category
        apply is_equiv_inv,
    apply is_hset_iso,
  end
+  end basic
+
+  -- Bundled version of categories
+  -- we don't use Category.carrier explicitly, but rather use Precategory.carrier (to_Precategory C)
+  structure Category : Type :=
+    (carrier : Type)
+    (struct : category carrier)
+
+  attribute Category.struct [instance] [coercion]
+  -- definition objects [reducible] := Category.objects
+  -- definition category_instance [instance] [coercion] [reducible] := Category.category_instance
+
+  definition Category.to_Precategory [coercion] [reducible] (C : Category) : Precategory :=
+  Precategory.mk (Category.carrier C) C
+
+  definition category.Mk [reducible] := Category.mk
+  definition category.MK [reducible] (C : Precategory)
+    (H : Π (a b : C), is_equiv (@iso_of_path C C a b)) : Category :=
+  Category.mk C (category.mk' C C H)
+
+  definition Category.eta (C : Category) : Category.mk C C = C :=
+  Category.rec (λob c, idp) C

 end category
-
-- Bundled version of categories
-
-structure Category : Type :=
-  (objects : Type)
-  (category_instance : category objects)
-
-namespace category
-  definition Mk {ob} (C) : Category := Category.mk ob C
-  --definition MK (a b c d e f g h i) : Category := Category.mk a (category.mk b c d e f g h i)
-
-  definition objects [coercion] [reducible] := Category.objects
-  definition category_instance [instance] [coercion] [reducible] := Category.category_instance
-
-end category
-
-open category
-
-protected definition Category.eta (C : Category) : Category.mk C C = C :=
-Category.rec (λob c, idp) C
--- a/hott/algebra/category/constructions.hlean
+++ b/hott/algebra/category/constructions.hlean
@ -0,0 +1,33 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.category.constructions
+Authors: Floris van Doorn
+-/
+
+import .basic algebra.precategory.constructions
+
+open eq prod eq eq.ops equiv is_trunc funext pi category.ops morphism category
+
+namespace category
+
+  section hset
+  definition is_category_hset (a b : Precategory_hset) : is_equiv (@iso_of_path _ _ a b) :=
+  sorry
+
+  definition category_hset [reducible] [instance] : category hset :=
+  category.mk' hset precategory_hset is_category_hset
+
+  definition Category_hset [reducible] : Category :=
+  Category.mk hset category_hset
+
+  --RENAME AND CLEANUP
+  definition set_category_equiv_iso (a b : Category_hset) : (a ≅ b) = (a ≃ b) := sorry
+
+  end hset
+  namespace ops
+    abbreviation set := Category_hset
+  end ops
+
+end category
--- a/hott/algebra/category/set.hlean
+++ b/hott/algebra/category/set.hlean
@ -1,70 +0,0 @@
-- Copyright (c) 2015 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Jakob von Raumer
-- Category of sets
-
-import .basic types.pi types.trunc
-
-open is_trunc sigma sigma.ops pi function eq morphism precategory
-open equiv
-
-namespace precategory
-
-  universe variable l
-
-  definition set_precategory : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A) :=
-  begin
-    fapply precategory.mk.{l+1 l},
-                  intros (a, a_1), apply (a.1 → a_1.1),
-                intros, apply is_trunc_pi, intros, apply b.2,
-              intros, intro x, exact (a_1 (a_2 x)),
-            intros, exact (λ (x : a.1), x),
-          intros, apply eq_of_homotopy, intro x, apply idp,
-        intros, apply eq_of_homotopy, intro x, apply idp,
-      intros, apply eq_of_homotopy, intro x, apply idp,
-  end
-
-end precategory
-
-namespace category
-
-  universe variable l
-  local attribute precategory.set_precategory.{l+1 l} [instance]
-
-  definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A))
-    : (a ≅ b) = (a.1 ≃ b.1) :=
-  /-begin
-    apply ua, fapply equiv.mk,
-      intro H,
-        apply (isomorphic.rec_on H), intros (H1, H2),
-        apply (is_iso.rec_on H2), intros (H3, H4, H5),
-        fapply equiv.mk,
-        apply (isomorphic.rec_on H), intros (H1, H2),
-        exact H1,
-      fapply is_equiv.adjointify, exact H3,
-          exact sorry,
-        exact sorry,
-  end-/ sorry
-
-  definition set_category : category.{l+1 l} (Σ (A : Type.{l}), is_hset A) :=
-  /-begin
-    assert (C : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A)),
-      apply precategory.set_precategory,
-    apply category.mk,
-    assert (p : (λ A B p, (set_category_equiv_iso A B) ▹ iso_of_path p) = (λ A B p, @equiv_of_eq A.1 B.1 p)),
-    apply is_equiv.adjointify,
-        intros,
-        apply (isomorphic.rec_on a_1), intros (iso', is_iso'),
-        apply (is_iso.rec_on is_iso'), intros (f', f'sect, f'retr),
-        fapply sigma_eq,
-          apply ua, fapply equiv.mk, exact iso',
-          fapply is_equiv.adjointify,
-              exact f',
-            intros, apply (f'retr ▹ _),
-          intros, apply (f'sect ▹ _),
-        apply (@is_hprop.elim),
-        apply is_hprop_is_trunc,
-      intros,
-  end -/ sorry
-
-end category
--- a/hott/algebra/groupoid.hlean
+++ b/hott/algebra/groupoid.hlean
@ -1,26 +1,32 @@
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
-import .precategory.basic .precategory.morphism .group types.pi
+/-
+Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.

-open eq function prod sigma pi is_trunc morphism nat path_algebra unit prod sigma.ops
+Module: algebra.groupoid
+Author: Jakob von Raumer

-structure foo (A : Type) := (bsp : A)
+Ported from Coq HoTT
+-/

-structure groupoid [class] (ob : Type) extends parent : precategory ob :=
-(all_iso : Π ⦃a b : ob⦄ (f : hom a b),
-  @is_iso ob parent a b f)
+import .precategory.morphism .group

-namespace groupoid
+open eq is_trunc morphism category path_algebra nat unit

-attribute all_iso [instance]
+namespace category

-universe variable l
-open precategory
-definition groupoid_of_1_type (A : Type.{l})
-    (H : is_trunc (nat.zero .+1) A) : groupoid.{l l} A :=
-groupoid.mk
+  structure groupoid [class] (ob : Type) extends parent : precategory ob :=
+   (all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f)
+
+  abbreviation all_iso := @groupoid.all_iso
+  attribute groupoid.all_iso [instance]
+
+  definition groupoid.mk' [reducible] (ob : Type) (C : precategory ob)
+    (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob :=
+  precategory.rec_on C groupoid.mk H
+
+  definition groupoid_of_1_type.{l} (A : Type.{l})
+      [H : is_trunc (succ zero) A] : groupoid.{l l} A :=
+  groupoid.mk
    (λ (a b : A), a = b)
    (λ (a b : A), have ish : is_hset (a = b), from is_trunc_eq nat.zero a b, ish)
    (λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p)
@ -31,10 +37,10 @@ groupoid.mk
    (λ (a b : A) (p : a = b), @is_iso.mk A _ a b p (p⁻¹)
      !con.left_inv !con.right_inv)

-- A groupoid with a contractible carrier is a group
-definition group_of_is_contr_groupoid {ob : Type} (H : is_contr ob)
-  (G : groupoid ob) : group (hom (center ob) (center ob)) :=
-begin
+  -- A groupoid with a contractible carrier is a group
+  definition group_of_is_contr_groupoid {ob : Type} [H : is_contr ob]
+    [G : groupoid ob] : group (hom (center ob) (center ob)) :=
+  begin
    fapply group.mk,
      intros (f, g), apply (comp f g),
      apply homH,
@ -44,10 +50,10 @@ begin
      intro f, apply id_right,
      intro f, exact (morphism.inverse f),
      intro f, exact (morphism.inverse_compose f),
-end
+  end

-definition group_of_unit_groupoid (G : groupoid unit) : group (hom ⋆ ⋆) :=
-begin
+  definition group_of_unit_groupoid [G : groupoid unit] : group (hom ⋆ ⋆) :=
+  begin
    fapply group.mk,
      intros (f, g), apply (comp f g),
      apply homH,
@ -57,11 +63,11 @@ begin
      intro f, apply id_right,
      intro f, exact (morphism.inverse f),
      intro f, exact (morphism.inverse_compose f),
-end
+  end

-- Conversely we can turn each group into a groupoid on the unit type
-definition of_group (A : Type.{l}) [G : group A] : groupoid.{l l} unit :=
-begin
+  -- Conversely we can turn each group into a groupoid on the unit type
+  definition of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{l l} unit :=
+  begin
    fapply groupoid.mk,
      intros, exact A,
      intros, apply (@group.carrier_hset A G),
@ -73,11 +79,11 @@ begin
      intros, apply is_iso.mk,
        apply mul_left_inv,
        apply mul_right_inv,
-end
+  end

-protected definition hom_group {A : Type} [G : groupoid A] (a : A) :
+  protected definition hom_group {A : Type} [G : groupoid A] (a : A) :
    group (hom a a) :=
-begin
+  begin
    fapply group.mk,
      intros (f, g), apply (comp f g),
      apply homH,
@ -87,6 +93,27 @@ begin
      intro f, apply id_right,
      intro f, exact (morphism.inverse f),
      intro f, exact (morphism.inverse_compose f),
-end
+  end

-end groupoid
+  -- Bundled version of categories
+  -- we don't use Groupoid.carrier explicitly, but rather use Groupoid.carrier (to_Precategory C)
+  structure Groupoid : Type :=
+    (carrier : Type)
+    (struct : groupoid carrier)
+
+  attribute Groupoid.struct [instance] [coercion]
+  -- definition objects [reducible] := Category.objects
+  -- definition category_instance [instance] [coercion] [reducible] := Category.category_instance
+
+  definition Groupoid.to_Precategory [coercion] [reducible] (C : Groupoid) : Precategory :=
+  Precategory.mk (Groupoid.carrier C) C
+
+  definition groupoid.Mk [reducible] := Groupoid.mk
+  definition category.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f)
+    : Groupoid :=
+  Groupoid.mk C (groupoid.mk' C C H)
+
+  definition Groupoid.eta (C : Groupoid) : Groupoid.mk C C = C :=
+  Groupoid.rec (λob c, idp) C
+
+end category
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@ -1,12 +1,18 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.precategory.basic
+Authors: Floris van Doorn
+-/

 open eq is_trunc

-structure precategory [class] (ob : Type) : Type :=
+namespace category
+
+  structure precategory [class] (ob : Type) : Type :=
    (hom : ob → ob → Type)
-  (homH : Π {a b : ob}, is_hset (hom a b))
+    (homH : Π(a b : ob), is_hset (hom a b))
    (comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
    (ID : Π (a : ob), hom a a)
    (assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b),
@ -14,33 +20,38 @@ structure precategory [class] (ob : Type) : Type :=
    (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
    (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)

-attribute precategory [multiple-instances]
+  attribute precategory [multiple-instances]
+  attribute precategory.homH [instance]

-namespace precategory
-  variables {ob : Type} [C : precategory ob]
-  variables {a b c d : ob}
-  include C
-  attribute homH [instance]
-
-  definition compose [reducible] := comp
-
-  definition id [reducible] {a : ob} : hom a a := ID a
-
-  infixr `∘` := comp
-  infixl [parsing-only] `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
+  infixr `∘` := precategory.comp
+  -- input ⟶ using \--> (this is a different arrow than \-> (→))
+  infixl [parsing-only] `⟶`:25 := precategory.hom
  namespace hom
-    infixl `⟶` := hom -- if you open this namespace, hom a b is printed as a ⟶ b
+    infixl `⟶` := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
  end hom

-  variables {h : hom c d} {g : hom b c} {f f' : hom a b} {i : hom a a}
+  abbreviation hom      := @precategory.hom
+  abbreviation homH     := @precategory.homH
+  abbreviation comp     := @precategory.comp
+  abbreviation ID       := @precategory.ID
+  abbreviation assoc    := @precategory.assoc
+  abbreviation id_left  := @precategory.id_left
+  abbreviation id_right := @precategory.id_right

-  theorem id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left
+  section basic_lemmas
+  variables {ob : Type} [C : precategory ob]
+  variables {a b c d : ob} {h : c ⟶ d} {g : hom b c} {f f' : hom a b} {i : a ⟶ a}
+  include C

-  theorem left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
+  definition id [reducible] := ID a
+
+  definition id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left
+
+  definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
  calc i = i ∘ id : id_right
     ... = id     : H

-  theorem right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id :=
+  definition right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id :=
  calc i = id ∘ i : id_left
     ... = id     : H

@ -49,26 +60,29 @@ namespace precategory

  definition is_hprop_eq_hom [instance] : is_hprop (f = f') :=
  !is_trunc_eq
+  end basic_lemmas

-end precategory
+  structure Precategory : Type :=
+    (carrier : Type)
+    (struct : precategory carrier)

-structure Precategory : Type :=
-  (objects : Type)
-  (category_instance : precategory objects)
+  definition precategory.Mk [reducible] {ob} (C) : Precategory := Precategory.mk ob C
+  definition precategory.MK [reducible] (a b c d e f g h) : Precategory :=
+  Precategory.mk a (precategory.mk b c d e f g h)

-namespace precategory
-  definition Mk {ob} (C) : Precategory := Precategory.mk ob C
-  definition MK (a b c d e f g h) : Precategory := Precategory.mk a (precategory.mk b c d e f g h)
+  abbreviation carrier := @Precategory.carrier

-  definition objects [coercion] [reducible] := Precategory.objects
-  definition category_instance [instance] [coercion] [reducible] := Precategory.category_instance
-  notation g `∘⁅` C `⁆` f := @compose (objects C) (category_instance C) _ _ _ g f
+  attribute Precategory.carrier [coercion]
+  attribute Precategory.struct [instance] [priority 10000] [coercion]
+  -- definition precategory.carrier [coercion] [reducible] := Precategory.carrier
+  -- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct
+  notation g `∘⁅` C `⁆` f := @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
  -- TODO: make this left associative
  -- TODO: change this notation?

-end precategory
+  definition Precategory.eta (C : Precategory) : Precategory.mk C C = C :=
+  Precategory.rec (λob c, idp) C

-open precategory
+end category

-protected definition Precategory.eta (C : Precategory) : Precategory.mk C C = C :=
-Precategory.rec (λob c, idp) C
+open category
--- a/hott/algebra/precategory/constructions.hlean
+++ b/hott/algebra/precategory/constructions.hlean
@ -13,27 +13,27 @@ import types.prod types.sigma types.pi

 open eq prod eq eq.ops equiv is_trunc

-namespace precategory
+namespace category
  namespace opposite

  definition opposite [reducible] {ob : Type} (C : precategory ob) : precategory ob :=
-  mk (λ a b, hom b a)
-     (λ b a, !homH)
+  precategory.mk (λ a b, hom b a)
+                 (λ a b, !homH)
                 (λ a b c f g, g ∘ f)
                 (λ a, id)
                 (λ a b c d f g h, !assoc⁻¹)
                 (λ a b f, !id_right)
                 (λ a b f, !id_left)

-  definition Opposite [reducible] (C : Precategory) : Precategory := Mk (opposite C)
+  definition Opposite [reducible] (C : Precategory) : Precategory := precategory.Mk (opposite C)

-  infixr `∘op`:60 := @compose _ (opposite _) _ _ _
+  infixr `∘op`:60 := @comp _ (opposite _) _ _ _

  variables {C : Precategory} {a b c : C}

  set_option apply.class_instance false -- disable class instance resolution in the apply tactic

-  theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp
+  definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp

  -- TODO: Decide whether just to use funext for this theorem or
  --       take the trick they use in Coq-HoTT, and introduce a further
@ -91,9 +91,9 @@ namespace precategory
  section
  open prod is_trunc

-  definition prod_precategory [reducible] [instance] {obC obD : Type} (C : precategory obC) (D : precategory obD)
+  definition prod_precategory [reducible] {obC obD : Type} (C : precategory obC) (D : precategory obD)
      : precategory (obC × obD) :=
-  mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
+  precategory.mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
                 (λ a b, !is_trunc_prod)
                 (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
                 (λ a, (id, id))
@ -101,7 +101,8 @@ namespace precategory
                 (λ a b f,         prod_eq  !id_left  !id_left )
                 (λ a b f,         prod_eq  !id_right !id_right)

-  definition Prod_precategory [reducible] (C D : Precategory) : Precategory := Mk (prod_precategory C D)
+  definition Prod_precategory [reducible] (C D : Precategory) : Precategory :=
+  precategory.Mk (prod_precategory C D)

  end
  end product
@ -113,8 +114,6 @@ namespace precategory
    infixr `×c`:30 := product.Prod_precategory
    --instance [persistent] type_category category_one
    --                      category_two product.prod_category
-    attribute product.prod_precategory [instance]
-
  end ops

  open ops
@ -156,7 +155,7 @@ namespace precategory
    open morphism functor nat_trans
    definition precategory_functor [instance] [reducible] (C D : Precategory)
      : precategory (functor C D) :=
-    mk (λa b, nat_trans a b)
+    precategory.mk (λa b, nat_trans a b)
                   (λ a b, @nat_trans.to_hset C D a b)
                   (λ a b c g f, nat_trans.compose g f)
                   (λ a, nat_trans.id)
@ -165,7 +164,7 @@ namespace precategory
                   (λ a b f, !nat_trans.id_right)

    definition Precategory_functor [reducible] (C D : Precategory) : Precategory :=
-    Mk (precategory_functor C D)
+    precategory.Mk (precategory_functor C D)

    definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory :=
    Precategory_functor D C
@ -206,11 +205,10 @@ namespace precategory
  end precategory_functor

  namespace ops
-  abbreviation set := Precategory_hset
  infixr `^c`:35 := Precategory_functor_rev
  infixr `×f`:30 := product.prod_functor
  infixr `ᵒᵖᶠ`:(max+1) := opposite.opposite_functor
  end ops


-end precategory
+end category
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@ -1,10 +1,14 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Floris van Doorn, Jakob von Raumer
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.precategory.functor
+Authors: Floris van Doorn, Jakob von Raumer
+-/

 import .basic types.pi

-open function precategory eq prod equiv is_equiv sigma sigma.ops is_trunc funext
+open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext
 open pi

 structure functor (C D : Precategory) : Type :=
@ -134,7 +138,7 @@ namespace functor
  end

  protected definition strict_cat_has_functor_hset
-    [HD : is_hset (objects D)] : is_hset (functor C D) :=
+    [HD : is_hset D] : is_hset (functor C D) :=
  begin
    apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv,
      apply sigma_char,
@ -151,10 +155,12 @@ namespace functor

 end functor

-namespace precategory
+
+namespace category
  open functor

-  definition precat_of_strict_precats : precategory (Σ (C : Precategory), is_hset (objects C)) :=
+  --TODO: make this a structure
+  definition precat_of_strict_precats : precategory (Σ (C : Precategory), is_hset C) :=
  precategory.mk (λ a b, functor a.1 b.1)
     (λ a b, @functor.strict_cat_has_functor_hset a.1 b.1 b.2)
     (λ a b c g f, functor.compose g f)
@ -163,13 +169,13 @@ namespace precategory
     (λ a b f, !functor.id_left)
     (λ a b f, !functor.id_right)

-  definition Precat_of_strict_cats := Mk precat_of_strict_precats
+  definition Precat_of_strict_cats := precategory.Mk precat_of_strict_precats

  namespace ops

    abbreviation PreCat := Precat_of_strict_cats
-    attribute precat_of_strict_precats [instance]
+    --attribute precat_of_strict_precats [instance]

  end ops

-end precategory
+end category
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@ -1,10 +1,14 @@
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Floris van Doorn, Jakob von Raumer
+/-
+Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.precategory.iso
+Authors: Floris van Doorn, Jakob von Raumer
+-/

 import .basic .morphism types.sigma

-open eq precategory sigma sigma.ops equiv is_equiv function is_trunc
+open eq category sigma sigma.ops equiv is_equiv function is_trunc
 open prod

 namespace morphism
@ -62,7 +66,7 @@ namespace morphism
  end

  -- In a precategory, equal objects are isomorphic
-  definition iso_of_path (p : a = b) : isomorphic a b :=
+  definition iso_of_path (p : a = b) : a ≅ b :=
  eq.rec_on p (isomorphic.mk id)

 end morphism
--- a/hott/algebra/precategory/morphism.hlean
+++ b/hott/algebra/precategory/morphism.hlean
@ -1,14 +1,20 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Floris van Doorn, Jakob von Raumer
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.precategory.morphism
+Authors: Floris van Doorn, Jakob von Raumer
+-/

 import .basic

-open eq precategory sigma sigma.ops equiv is_equiv function is_trunc
+open eq category sigma sigma.ops equiv is_equiv function is_trunc

 namespace morphism
-  variables {ob : Type} [C : precategory ob] include C
+  variables {ob : Type} [C : precategory ob]
  variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
+  include C
+
  inductive is_section    [class] (f : a ⟶ b) : Type
  := mk : ∀{g}, g ∘ f = id → is_section f
  inductive is_retraction [class] (f : a ⟶ b) : Type
@ -80,7 +86,7 @@ namespace morphism
  theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
  inverse_eq_intro_left !inverse_compose

-  theorem inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f :=
+  theorem inverse_involutive (f : a ⟶ b) [H1 : is_iso f] [H2 : is_iso (f⁻¹)] : (f⁻¹)⁻¹ = f :=
  inverse_eq_intro_right !inverse_compose

  theorem retraction_of_id : retraction_of (ID a) = id :=
--- a/hott/algebra/precategory/nat_trans.hlean
+++ b/hott/algebra/precategory/nat_trans.hlean
@ -1,25 +1,24 @@
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn, Jakob von Raumer
+/-
+Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.precategory.nat_trans
+Author: Floris van Doorn, Jakob von Raumer
+-/

 import .functor .morphism
-open eq precategory functor is_trunc equiv sigma.ops sigma is_equiv function pi funext
+open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext

-inductive nat_trans {C D : Precategory} (F G : C ⇒ D) : Type :=
-mk : Π (η : Π (a : C), hom (F a) (G a))
-  (nat : Π {a b : C} (f : hom a b), G f ∘ η a = η b ∘ F f),
-  nat_trans F G
+structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
+ (natural_map : Π (a : C), hom (F a) (G a))
+ (naturality : Π {a b : C} (f : hom a b), G f ∘ natural_map a = natural_map b ∘ F f)

 namespace nat_trans

  infixl `⟹`:25 := nat_trans -- \==>
  variables {C D : Precategory} {F G H I : C ⇒ D}

-  definition natural_map [coercion] (η : F ⟹ G) : Π (a : C), F a ⟶ G a :=
-  nat_trans.rec (λ x y, x) η
-
-  theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a = η b ∘ F f :=
-  nat_trans.rec (λ x y, y) η
+  attribute natural_map [coercion]

  protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
  nat_trans.mk
@ -84,10 +83,10 @@ namespace nat_trans
  begin
    apply is_trunc_is_equiv_closed, apply (equiv.to_is_equiv !sigma_char),
    apply is_trunc_sigma,
-      apply is_trunc_pi, intro a, exact (@homH (objects D) _ (F a) (G a)),
+      apply is_trunc_pi, intro a, exact (@homH (Precategory.carrier D) _ (F a) (G a)),
    intro η, apply is_trunc_pi, intro a,
    apply is_trunc_pi, intro b, apply is_trunc_pi, intro f,
-    apply is_trunc_eq, apply is_trunc_succ, exact (@homH (objects D) _ (F a) (G b)),
+    apply is_trunc_eq, apply is_trunc_succ, exact (@homH (Precategory.carrier D) _ (F a) (G b)),
  end

 end nat_trans
--- a/hott/algebra/precategory/yoneda.hlean
+++ b/hott/algebra/precategory/yoneda.hlean
@ -7,22 +7,23 @@ Author: Floris van Doorn
 -/

 --note: modify definition in category.set
-import .constructions .morphism
+import algebra.category.constructions .morphism

-open eq precategory functor is_trunc equiv is_equiv pi
-open is_trunc.trunctype funext precategory.ops prod.ops
+open category eq category.ops functor prod.ops is_trunc

 set_option pp.beta true
-
 namespace yoneda
  set_option class.conservative false

-  definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C} (f1 : a5 ⟶ a6) (f2 : a4 ⟶ a5) (f3 : a3 ⟶ a4) (f4 : a2 ⟶ a3) (f5 : a1 ⟶ a2) : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 :=
+  --TODO: why does this take so much steps? (giving more information than "assoc" hardly helps)
+  definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C}
+    (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2)
+      : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 :=
  calc
-    (f1 ∘ f2) ∘ f3 ∘ f4 ∘ f5 = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : assoc
+        _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : assoc
      ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5 : assoc
      ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : assoc
-    ... = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 : assoc
+      ... = _ : assoc

  --disturbing behaviour: giving the type of f "(x ⟶ y)" explicitly makes the unifier loop
  definition representable_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
@ -37,7 +38,7 @@ namespace yoneda
 end yoneda


-
+open is_equiv equiv

 namespace functor
  open prod nat_trans
--- a/hott/equiv_precomp.hlean
+++ b/hott/equiv_precomp.hlean
@ -7,7 +7,8 @@ Author: Jakob von Raumer

 Ported from Coq HoTT
 -/
-exit
+
+-- This file is nowhere used. Do we want to keep it?
 open eq function funext

 namespace is_equiv
--- a/hott/init/axioms/funext.hlean
+++ b/hott/init/axioms/funext.hlean
@ -1,31 +0,0 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad, Jakob von Raumer
-- Ported from Coq HoTT
-prelude
-import ..path ..equiv
-open eq
-
-- Funext
-- ------
-
-- Define function extensionality as a type class
-- structure funext [class] : Type  :=
-- (elim : Π (A : Type) (P : A → Type ) (f g : Π x, P x), is_equiv (@apD10 A P f g))
-- set_option pp.universes true
-- check @funext.mk
-- check @funext.elim
-exit
-
-namespace funext
-
-  attribute elim [instance]
-
-  definition eq_of_homotopy [F : funext] {A : Type} {P : A → Type} {f g : Π x, P x} : f ∼ g → f = g :=
-  is_equiv.inv (@apD10 A P f g)
-
-  definition eq_of_homotopy2 [F : funext] {A B : Type} {P : A → B → Type}
-      (f g : Πx y, P x y) : (Πx y, f x y = g x y) → f = g :=
-    λ E, eq_of_homotopy (λx, eq_of_homotopy (E x))
-
-end funext
--- a/hott/init/axioms/funext_of_ua.hlean
+++ b/hott/init/axioms/funext_of_ua.hlean
@ -1,10 +1,16 @@
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
+/-
+Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: init.axioms.funext_of_ua
+Author: Jakob von Raumer
+
+Ported from Coq HoTT
+-/
+
 prelude
 import ..equiv ..datatypes ..types.prod
-import .funext_varieties .ua .funext
+import .funext_varieties .ua

 open eq function prod is_trunc sigma equiv is_equiv unit

--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@ -1,9 +1,15 @@
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Jakob von Raumer
-- Ported from Coq HoTT
+/-
+Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: init.axioms.funext_varieties
+Authors: Jakob von Raumer
+
+Ported from Coq HoTT
+-/
+
 prelude
-import ..path ..trunc ..equiv .funext
+import ..path ..trunc ..equiv

 open eq is_trunc sigma function

@ -46,7 +52,7 @@ definition weak_funext_of_naive_funext : naive_funext → weak_funext :=

 context
  universes l k
-  parameters (wf : weak_funext.{l k}) {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
+  parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)

  definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
    is_contr.mk (sigma.mk f (homotopy.refl f))
--- a/hott/init/axioms/ua.hlean
+++ b/hott/init/axioms/ua.hlean
@ -1,7 +1,13 @@
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
+/-
+Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: init.axioms.ua
+Author: Jakob von Raumer
+
+Ported from Coq HoTT
+-/
+
 prelude
 import ..path ..equiv
 open eq equiv is_equiv
--- a/hott/init/bool.hlean
+++ b/hott/init/bool.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.bool
 Author: Leonardo de Moura
 -/
+
 prelude
 import init.datatypes init.reserved_notation

--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@ -7,6 +7,7 @@ Authors: Leonardo de Moura, Jakob von Raumer

 Basic datatypes
 -/
+
 prelude
 notation [parsing-only] `Type'` := Type.{_+1}
 notation [parsing-only] `Type₊` := Type.{_+1}
--- a/hott/init/default.hlean
+++ b/hott/init/default.hlean
@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.default
 Authors: Leonardo de Moura, Jakob von Raumer
 -/
+
 prelude
 import init.datatypes init.reserved_notation init.tactic init.logic
 import init.bool init.num init.priority init.relation init.wf
 import init.types.sigma init.types.prod init.types.empty
 import init.trunc init.path init.equiv init.util
-import init.axioms.ua init.axioms.funext init.axioms.funext_of_ua
+import init.axioms.ua init.axioms.funext_of_ua
 import init.hedberg init.nat
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@ -218,33 +218,41 @@ end is_equiv

 open is_equiv
 namespace equiv
-
+  namespace ops
+    attribute to_fun [coercion]
+  end ops
+  open equiv.ops
  attribute to_is_equiv [instance]

  infix `≃`:25 := equiv

-  context
-  parameters {A B C : Type} (eqf : A ≃ B)
+  variables {A B C : Type}

-  private definition f : A → B := to_fun eqf
-  private definition Hf [instance] : is_equiv f := to_is_equiv eqf
+  protected definition MK (f : A → B) (g : B → A) (retr : f ∘ g ∼ id) (sect : g ∘ f ∼ id) : A ≃ B :=
+  equiv.mk f (adjointify f g retr sect)
+  definition to_inv (f : A ≃ B) : B → A :=
+  f⁻¹

-  protected definition refl : A ≃ A := equiv.mk id is_equiv.is_equiv_id
+  protected definition refl : A ≃ A :=
+  equiv.mk id !is_equiv_id

-  definition trans (eqg: B ≃ C) : A ≃ C :=
-    equiv.mk ((to_fun eqg) ∘ f)
-             (is_equiv_compose f (to_fun eqg))
+  protected definition symm (f : A ≃ B) : B ≃ A :=
+  equiv.mk (f⁻¹) !is_equiv_inv

-  definition equiv_of_eq_of_equiv (f' : A → B) (Heq : to_fun eqf = f') : A ≃ B :=
-    equiv.mk f' (is_equiv.is_equiv_eq_closed f Heq)
+  protected definition trans (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
+  equiv.mk (g ∘ f) !is_equiv_compose

-  definition symm : B ≃ A :=
-    equiv.mk (is_equiv.inv f) !is_equiv.is_equiv_inv
+  definition equiv_of_eq_of_equiv (f : A ≃ B) (f' : A → B) (Heq : f = f') : A ≃ B :=
+  equiv.mk f' (is_equiv_eq_closed f Heq)

-  definition equiv_ap (P : A → Type) {x y : A} {p : x = y} : (P x) ≃ (P y) :=
-    equiv.mk (eq.transport P p) (is_equiv_tr P p)
+  definition eq_equiv_fn_eq (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
+  equiv.mk (ap f) !is_equiv_ap

-  end
+  definition eq_equiv_fn_eq_of_equiv (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) :=
+  equiv.mk (ap f) !is_equiv_ap
+
+  definition equiv_ap (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) :=
+  equiv.mk (transport P p) !is_equiv_tr

  --we need this theorem for the funext_of_ua proof
  theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ :=
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@ -7,6 +7,7 @@ Author: Leonardo de Moura

 General operations on functions.
 -/
+
 prelude
 import init.reserved_notation

--- a/hott/init/hedberg.hlean
+++ b/hott/init/hedberg.hlean
@ -6,6 +6,7 @@ Author: Leonardo de Moura

 Hedberg's Theorem: every type with decidable equality is a hset
 -/
+
 prelude
 import init.trunc
 open eq eq.ops nat is_trunc sigma
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.logic
 Authors: Leonardo de Moura
 -/
+
 prelude
 import init.datatypes init.reserved_notation

--- a/hott/init/num.hlean
+++ b/hott/init/num.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module init.num
 Authors: Leonardo de Moura
 -/
+
 prelude
 import init.logic init.bool
 open bool
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@ -3,7 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

 Module: init.path
-Author: Jeremy Avigad, Jakob von Raumer
+Author: Jeremy Avigad, Jakob von Raumer, Floris van Doorn

 Ported from Coq HoTT
 -/
@ -549,10 +549,10 @@ namespace eq
  -- Unwhiskering, a.k.a. cancelling

  definition cancel_left {x y z : A} (p : x = y) (q r : y = z) : (p ⬝ q = p ⬝ r) → (q = r) :=
-  eq.rec_on p (take r, eq.rec_on r (take q a, (idp_con q)⁻¹ ⬝ a)) r q
+  eq.rec_on p (λq r s, !idp_con⁻¹ ⬝ s ⬝ !idp_con) q r

  definition cancel_right {x y z : A} (p q : x = y) (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) :=
-  eq.rec_on r (eq.rec_on p (take q a, a ⬝ con_idp q)) q
+  eq.rec_on r (λs, !con_idp⁻¹ ⬝ s ⬝ !con_idp)

  -- Whiskering and identity paths.

@ -580,7 +580,6 @@ namespace eq
    idp ◾ h = whisker_left idp h :> (idp ⬝ p = idp ⬝ q) :=
  eq.rec_on h idp

-  -- TODO: note, 4 inductions
  -- The interchange law for concatenation.
  definition con2_con_con2 {p p' p'' : x = y} {q q' q'' : y = z}
      (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') :
--- a/hott/init/priority.hlean
+++ b/hott/init/priority.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.priority
 Authors: Leonardo de Moura
 -/
+
 prelude
 import init.datatypes
 definition std.priority.default : num := 1000
--- a/hott/init/relation.hlean
+++ b/hott/init/relation.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.relation
 Authors: Leonardo de Moura
 -/
+
 prelude
 import init.logic

--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@ -7,6 +7,7 @@ Authors: Leonardo de Moura

 Basic datatypes
 -/
+
 prelude
 import init.datatypes

--- a/hott/init/tactic.hlean
+++ b/hott/init/tactic.hlean
@ -10,6 +10,7 @@ expression. We should view 'tactic' as automation that when execute
 produces a term.  tactic.builtin is just a "dummy" for creating the
 definitions that are actually implemented in C++
 -/
+
 prelude
 import init.datatypes init.reserved_notation

--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@ -196,7 +196,7 @@ namespace is_trunc

  notation n `-Type` := trunctype n
  abbreviation hprop := -1-Type
-  abbreviation hset := (-1.+1)-Type
+  abbreviation hset := 0-Type

  protected definition hprop.mk := @trunctype.mk -1
  protected definition hset.mk := @trunctype.mk (-1.+1)
--- a/hott/init/types/prod.hlean
+++ b/hott/init/types/prod.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.types.prod
 Author: Leonardo de Moura, Jeremy Avigad
 -/
+
 prelude
 import ..wf ..num

--- a/hott/init/types/sigma.hlean
+++ b/hott/init/types/sigma.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.types.sigma
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
+
 prelude
 import init.num

--- a/hott/init/types/sum.hlean
+++ b/hott/init/types/sum.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.types.sum
 Author: Leonardo de Moura, Jeremy Avigad
 -/
+
 prelude
 import init.datatypes init.reserved_notation

--- a/hott/init/util.hlean
+++ b/hott/init/util.hlean
@ -7,6 +7,7 @@ Author: Leonardo de Moura

 Auxiliary definitions used by automation
 -/
+
 prelude
 import init.trunc

--- a/hott/init/wf.hlean
+++ b/hott/init/wf.hlean
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: init.wf
 Author: Leonardo de Moura
 -/
+
 prelude
 import init.relation init.tactic

--- a/hott/logic.hlean
+++ b/hott/logic.hlean
@ -1,11 +0,0 @@
-exit
--javra:        Maybe this should go somewhere else
-
-open eq
-
-inductive tdecidable [class] (A : Type) : Type :=
-inl :  A → tdecidable A,
-inr : ¬A → tdecidable A
-
-structure decidable_paths [class] (A : Type) :=
-(elim : ∀(x y : A), tdecidable (x = y))
--- a/hott/truncation.hlean
+++ b/hott/truncation.hlean
@ -1,6 +1,10 @@
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Jakob von Raumer
+/-
+Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: truncation
+Authors: Jakob von Raumer
+-/

 open is_trunc

--- a/hott/types/W.hlean
+++ b/hott/types/W.hlean
@ -1,6 +1,8 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: types.W
 Author: Floris van Doorn

 Theorems about W-types (well-founded trees)
--- a/hott/types/path.hlean
+++ b/hott/types/path.hlean
@ -1,9 +1,11 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Floris van Doorn
-Ported from Coq HoTT

+Module: types.path
+Author: Floris van Doorn
+
+Ported from Coq HoTT
 Theorems about path types (identity types)
 -/

@ -133,11 +135,18 @@ namespace path
  equiv.trans (equiv_concat_l p a3) (equiv_concat_r q a2)

 /- BELOW STILL NEEDS TO BE PORTED FROM COQ HOTT -/
-
-  -- definition isequiv_whiskerL [instance] (p : a1 = a2) (q r : a2 = a3)
-  -- : is_equiv (@whisker_left A a1 a2 a3 p q r) :=
-  -- begin
-
+--   set_option pp.beta true
+--   check @cancel_left
+--   set_option pp.full_names true
+--   definition isequiv_whiskerL [instance] (p : a1 = a2) (q r : a2 = a3)
+--   : is_equiv (@whisker_left A a1 a2 a3 p q r) :=
+--   begin
+--   fapply adjointify,
+--   intro H, apply (!cancel_left H),
+--   intro s, esimp {function.compose, function.id}, unfold eq.cancel_left,
+-- --  reverts (q,r,a),  apply (eq.rec_on p), esimp {whisker_left,concat2, idp, cancel_left, eq.rec_on}, intros, esimp,
+--   end
+--  check @whisker_right_con_whisker_left
  -- end
  -- /-begin
  --   refine (isequiv_adjointify _ _ _ _).
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@ -1,11 +1,14 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Floris van Doorn
-Ported from Coq HoTT

+Module: types.pi
+Author: Floris van Doorn
+
+Ported from Coq HoTT
 Theorems about pi-types (dependent function spaces)
 -/
+
 import types.sigma

 open eq equiv is_equiv funext
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@ -1,9 +1,11 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Floris van Doorn
-Ported from Coq HoTT

+Module: types.prod
+Author: Floris van Doorn
+
+Ported from Coq HoTT
 Theorems about products
 -/

--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@ -1,11 +1,14 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Floris van Doorn
-Ported from Coq HoTT

+Module: types.sigma
+Author: Floris van Doorn
+
+Ported from Coq HoTT
 Theorems about sigma-types (dependent sums)
 -/
+
 import types.prod

 open eq sigma sigma.ops equiv is_equiv
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@ -29,17 +29,16 @@ namespace is_trunc
  definition is_trunc.pi_char (n : trunc_index) (A : Type) :
    (Π (x y : A), is_trunc n (x = y)) ≃ (is_trunc (n .+1) A) :=
  begin
-    fapply equiv.mk,
+    fapply equiv.MK,
      {intro H, apply is_trunc_succ_intro},
-      {fapply is_equiv.adjointify,
      {intros (H, x, y), apply is_trunc_eq},
      {intro H, apply (is_trunc.rec_on H), intro Hint, apply idp},
-        {intro P,
-         unfold compose, apply eq_of_homotopy,
-         exact sorry}},
+      {intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b,
+    esimp {function.id,compose,is_trunc_succ_intro,is_trunc_eq},
+    generalize (P a b), intro H, apply (is_trunc.rec_on H), intro H', apply idp},
  end

-  definition is_hprop_is_trunc {n : trunc_index} :
+  definition is_hprop_is_trunc [instance] (n : trunc_index) :
    Π (A : Type), is_hprop (is_trunc n A) :=
  begin
    apply (trunc_index.rec_on n),
@ -84,7 +83,7 @@ namespace is_trunc
      have H2 : transport (λx, R a x → a = x) p (@imp a a) = @imp a a, from !apD,
      have H3 : Π(r : R a a), transport (λx, a = x) p (imp r)
                              = imp (transport (λx, R a x) p r), from
-        to_fun (symm !heq_pi) H2,
+        to_fun (equiv.symm !heq_pi) H2,
      have H4 : imp (refl a) ⬝ p = imp (refl a), from
        calc
          imp (refl a) ⬝ p = transport (λx, a = x) p (imp (refl a)) : transport_paths_r
@ -117,4 +116,25 @@ namespace is_trunc
    (K : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A :=
  @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_leq H (λp, eq.rec_on p !K))

+  open trunctype equiv equiv.ops
+
+  protected definition trunctype.sigma_char.{l} (n : trunc_index) :
+    (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
+  begin
+    fapply equiv.MK,
+    /--/  intro A, exact (⟨trunctype_type A, is_trunc_trunctype_type A⟩),
+    /--/  intro S, exact (trunctype.mk S.1 S.2),
+    /--/  intro S, apply (sigma.rec_on S), intros (S1, S2), apply idp,
+    intro A, apply (trunctype.rec_on A), intros (A1, A2), apply idp,
+  end
+
+--  set_option pp.notation false
+  protected definition trunctype.eq (n : trunc_index) (A B : n-Type) :
+    (A = B) ≃ (trunctype_type A = trunctype_type B) :=
+  calc
+    (A = B) ≃ (trunctype.sigma_char n A = trunctype.sigma_char n B) : eq_equiv_fn_eq_of_equiv
+      ... ≃ ((trunctype.sigma_char n A).1 = (trunctype.sigma_char n B).1) : equiv.symm (!equiv_subtype)
+      ... ≃ (trunctype_type A = trunctype_type B) : equiv.refl
+
+
 end is_trunc