diff --git a/library/algebra/category.lean b/library/algebra/category.lean
index 00e95e314..e72c19be6 100644
--- a/library/algebra/category.lean
+++ b/library/algebra/category.lean
@@ -6,20 +6,23 @@
 import logic.core.eq logic.core.connectives
 import data.unit data.sigma data.prod
 import algebra.function
+import logic.axioms.funext
 
 open eq
 
 inductive category [class] (ob : Type) : Type :=
-mk : Π (mor : ob → ob → Type) (comp : Π{A B C : ob}, mor B C → mor A B → mor A C)
+mk : Π (mor : ob → ob → Type) (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
            (id : Π {A : ob}, mor A A),
-            (Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
+            (Π ⦃A B C D : ob⦄ {h : mor C D} {g : mor B C} {f : mor A B},
             comp h (comp g f) = comp (comp h g) f) →
-           (Π {A B : ob} {f : mor A B}, comp f id = f) →
-           (Π {A B : ob} {f : mor A B}, comp id f = f) →
+           (Π ⦃A B : ob⦄ {f : mor A B}, comp id f = f) →
+           (Π ⦃A B : ob⦄ {f : mor A B}, comp f id = f) →
             category ob
 
+inductive Category : Type :=
+mk : Π (A : Type), category A → Category
+
 namespace category
-  precedence `∘` : 60
 
   section
   parameters {ob : Type} {Cat : category ob} {A B C D : ob}
@@ -32,16 +35,17 @@ namespace category
   rec (λ mor compose id assoc idr idl, id) Cat
   definition ID (A : ob) : mor A A := @id A
 
+  precedence `∘` : 60
   infixr `∘` := compose
 
-  theorem assoc : Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
+  theorem assoc : Π {A B C D : ob} {h : mor C D} {g : mor B C} {f : mor A B},
                 h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
   rec (λ mor comp id assoc idr idl, assoc) Cat
 
-  theorem id_right : Π {A B : ob} {f : mor A B}, f ∘ id = f :=
-  rec (λ mor comp id assoc idr idl, idr) Cat
   theorem id_left  : Π {A B : ob} {f : mor A B}, id ∘ f = f :=
-  rec (λ mor comp id assoc idr idl, idl) Cat
+  rec (λ mor comp id assoc idl idr, idl) Cat
+  theorem id_right : Π {A B : ob} {f : mor A B}, f ∘ id = f :=
+  rec (λ mor comp id assoc idl idr, idr) Cat
 
   theorem id_compose {A : ob} : (ID A) ∘ id = id :=
   id_left
@@ -178,8 +182,16 @@ namespace category
   ... = h : id_right
 
   end
-  infixr `∘` := compose
-  postfix `⁻¹` := inverse
+
+  section
+
+  definition objects [coercion] (C : Category) : Type
+  := Category.rec (fun c s, c) C
+
+  definition category_instance [instance] (C : Category) : category (objects C)
+  := Category.rec (fun c s, s) C
+
+  end
 
   section
   open unit
@@ -192,19 +204,24 @@ namespace category
   parameter {ob : Type}
   definition opposite (C : category ob) : category ob :=
   category.mk (λa b, mor b a) (λ a b c f g, g ∘ f) (λ a, id) (λ a b c d f g h, symm assoc)
-    (λ a b f, id_left) (λ a b f, id_right)
+    (λ a b f, id_right) (λ a b f, id_left)
   precedence `∘op` : 60
   infixr `∘op` := @compose _ (opposite _) _ _ _
 
-  parameters {C : category ob} {a b c : ob} {f : @mor ob C a b} {g : @mor ob C b c}
+  parameters {C : category ob} {a b c : ob}
 
-  theorem compose_op : f ∘op g = g ∘ f :=
+  theorem compose_op {f : @mor ob C a b} {g : mor b c} : f ∘op g = g ∘ f :=
   rfl
 
   theorem op_op {C : category ob} : opposite (opposite C) = C :=
-  rec (λ mor comp id assoc idl idr, sorry) C
+  rec (λ mor comp id assoc idl idr, rfl) C
+
   end
 
+  definition Opposite (C : Category) : Category :=
+  Category.mk (objects C) (opposite (category_instance C))
+
+
   section
   --need extensionality
   -- definition type_cat : category Type :=
@@ -217,15 +234,18 @@ end category
 open category
 
 inductive functor {obC obD : Type} (C : category obC) (D : category obD) : Type :=
-mk : Π (obF : obC → obD) (morF : Π{A B : obC}, mor A B → mor (obF A) (obF B)),
-    (Π {A : obC}, morF (ID A) = ID (obF A)) →
-    (Π {A B C : obC} {f : mor A B} {g : mor B C}, morF (g ∘ f) = morF g ∘ morF f) →
-     @functor obC obD C D
+mk : Π (obF : obC → obD) (morF : Π⦃A B : obC⦄, mor A B → mor (obF A) (obF B)),
+    (Π ⦃A : obC⦄, morF (ID A) = ID (obF A)) →
+    (Π ⦃A B C : obC⦄ {f : mor A B} {g : mor B C}, morF (g ∘ f) = morF g ∘ morF f) →
+     functor C D
+
+inductive Functor (C D : Category) : Type :=
+mk : functor (category_instance C) (category_instance D) → Functor C D
 
 infixl `⇒`:25 := functor
 
 namespace functor
-  section
+  section basic_functor
   parameters {obC obD : Type} {C : category obC} {D : category obD}
   definition object [coercion] (F : C ⇒ D) : obC → obD := rec (λ obF morF Hid Hcomp, obF) F
 
@@ -238,10 +258,12 @@ namespace functor
   theorem respect_comp (F : C ⇒ D) : Π {a b c : obC} {f : mor a b} {g : mor b c},
       F (g ∘ f) = F g ∘ F f :=
   rec (λ obF morF Hid Hcomp, Hcomp) F
-  end
+  end basic_functor
+
+  section category_functor
 
   definition compose {obC obD obE : Type} {C : category obC} {D : category obD} {E : category obE}
-      (F : C ⇒ D) (G : D ⇒ E) : C ⇒ E :=
+      (G : D ⇒ E) (F : C ⇒ D) : C ⇒ E :=
   functor.mk C E
     (λx, G (F x))
     (λ a b f, G (F f))
@@ -252,4 +274,178 @@ namespace functor
       G (F (g ∘ f)) = G (F g ∘ F f)     : {respect_comp F}
                 ... = G (F g) ∘ G (F f) : respect_comp G)
 
+  precedence `∘∘` : 60
+  infixr `∘∘` := compose
+
+  -- theorem congr_functor {obC obD : Type} {C : category obC} {D : category obD} {o : obC → obD}
+  --     {m m' : Π⦃A B : obC⦄, mor A B → mor (o A) (o B)} {i i' c c'}
+  --     (Hm : ∀{a b : obC} {f : mor a b}, m f = m' f)
+  --       : functor.mk C D o m i c = functor.mk C D o m' i' c' :=
+  -- sorry
+
+  -- theorem congr_functor_refl {obC obD : Type} {C : category obC} {D : category obD} {o : obC → obD}
+  --     {m : Π⦃A B : obC⦄, mor A B → mor (o A) (o B)} {i i' c c'}
+  --       : functor.mk C D o m i c = functor.mk C D o m i' c' :=
+  -- rfl
+
+  theorem assoc {obA obB obC obD : Type} {A : category obA} {B : category obB}
+      {C : category obC} {D : category obD} (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
+      H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
+  rfl
+
+  -- later check whether we want implicit or explicit arguments here. For the moment, define both
+  definition id {ob : Type} {C : category ob} : functor C C :=
+  mk C C (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
+  definition ID {ob : Type} (C : category ob) : functor C C := id
+  definition Id {C : Category} : Functor C C := Functor.mk id
+  definition iD (C : Category) : Functor C C := Functor.mk id
+
+  theorem id_left {obC obB : Type} {B : category obB} {C : category obC} (F : B ⇒ C)
+      : id ∘∘ F = F :=
+  rec (λ obF morF idF compF, rfl) F
+
+  theorem id_right {obC obB : Type} {B : category obB} {C : category obC} (F : B ⇒ C)
+      : F ∘∘ id = F :=
+  rec (λ obF morF idF compF, rfl) F
+
+  end category_functor
+
+  section Functor
+--  parameters {C D E : Category} (G : Functor D E) (F : Functor C D)
+  definition Functor_functor {C D : Category} (F : Functor C D) : functor (category_instance C) (category_instance D) :=
+  Functor.rec (λ x, x) F
+
+  definition Compose {C D E : Category} (G : Functor D E) (F : Functor C D) : Functor C E :=
+  Functor.mk (compose (Functor_functor G) (Functor_functor F))
+
+--  namespace Functor
+  precedence `∘∘` : 60
+  infixr `∘∘` := Compose
+--  end Functor
+
+  definition Assoc {A B C D : Category} (H : Functor C D) (G : Functor B C) (F : Functor A B)
+    :  H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
+  rfl
+
+  theorem Id_left {B : Category} {C : Category} (F : Functor B C)
+      : Id ∘∘ F = F :=
+  Functor.rec (λ f, subst (id_left f) rfl) F
+
+  theorem Id_right {B : Category} {C : Category} (F : Functor B C)
+      : F ∘∘ Id = F :=
+  Functor.rec (λ f, subst (id_right f) rfl) F
+
+  end Functor
+
 end functor
+
+open functor
+
+inductive natural_transformation {obC obD : Type} {C : category obC} {D : category obD}
+    (F G : functor C D) : Type :=
+mk : Π (η : Π(a : obC), mor (object F a) (object G a)), Π{a b : obC} (f : mor a b), morphism G f ∘ η a = η b ∘ morphism F f
+ → natural_transformation F G
+
+inductive Natural_transformation {C D : Category} (F G : Functor C D) : Type :=
+mk : natural_transformation (Functor_functor F) (Functor_functor G) → Natural_transformation F G
+
+namespace natural_tranformation
+
+  -- todo
+
+end natural_tranformation
+
+open functor
+namespace category
+  section cat_Cat
+
+  definition Cat : category Category :=
+  mk (λ a b, Functor a b) (λ a b c g f, Compose g f) (λ a, Id)
+     (λ a b c d h g f, Assoc h g f) (λ a b f, Id_left f) (λ a b f, Id_right f)
+
+  end cat_Cat
+
+  section slice
+  open sigma
+
+  definition slice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor b c) :=
+  mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a)
+     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
+       (calc
+         dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : assoc
+           ... = dpr2 b ∘ dpr1 f : {dpr2 g}
+           ... = dpr2 a : {dpr2 f}))
+     (λ a, dpair id id_right)
+     (λ a b c d h g f, dpair_eq    assoc    proof_irrel)
+     (λ a b f,         sigma.equal id_left  proof_irrel)
+     (λ a b f,         sigma.equal id_right proof_irrel)
+  --replacing proof_irrel with rfl confuses the unifier
+  end slice
+
+
+  section coslice
+  open sigma
+
+  definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor c b) :=
+  mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b)
+     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
+       (calc
+         (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr1 g ∘ (dpr1 f ∘ dpr2 a): symm assoc
+           ... = dpr1 g ∘ dpr2 b : {dpr2 f}
+           ... = dpr2 c : {dpr2 g}))
+     (λ a, dpair id id_left)
+     (λ a b c d h g f, dpair_eq    assoc    proof_irrel)
+     (λ a b f,         sigma.equal id_left  proof_irrel)
+     (λ a b f,         sigma.equal id_right proof_irrel)
+
+  -- theorem slice_coslice_opp {ob : Type} (C : category ob) (c : ob) :
+  --     coslice C c = opposite (slice (opposite C) c) :=
+  -- sorry
+  end coslice
+
+  section product
+  open prod
+  definition product {obC obD : Type} (C : category obC) (D : category obD)
+      : category (obC × obD) :=
+  mk (λa b, mor (pr1 a) (pr1 b) × mor (pr2 a) (pr2 b))
+     (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
+     (λ a, (id,id))
+     (λ a b c d h g f, pair_eq    assoc    assoc   )
+     (λ a b f,         prod.equal id_left  id_left )
+     (λ a b f,         prod.equal id_right id_right)
+
+  end product
+
+  section arrow
+  open sigma eq_ops
+
+  definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), mor a b) :=
+  mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)) (h : mor (dpr2' a) (dpr2' b)),
+       dpr3 b ∘ g = h ∘ dpr3 a)
+     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (dpair (dpr2' g ∘ dpr2' f)
+       (calc
+         dpr3 c ∘ (dpr1 g ∘ dpr1 f) = (dpr3 c ∘ dpr1 g) ∘ dpr1 f : assoc
+           ... = (dpr2' g ∘ dpr3 b) ∘ dpr1 f : {dpr3 g}
+           ... = dpr2' g ∘ (dpr3 b ∘ dpr1 f) : symm assoc
+           ... = dpr2' g ∘ (dpr2' f ∘ dpr3 a) : {dpr3 f}
+           ... = (dpr2' g ∘ dpr2' f) ∘ dpr3 a : assoc)))
+     (λ a, dpair id (dpair id (id_right ⬝ (symm id_left))))
+     (λ a b c d h g f, dtrip_eq2   assoc    assoc    proof_irrel)
+     (λ a b f,         trip.equal2 id_left  id_left  proof_irrel)
+     (λ a b f,         trip.equal2 id_right id_right proof_irrel)
+     -- (λ a b c d h g f, dpair_eq assoc sorry)
+     -- (λ a b f,         sigma.equal id_left sorry)
+     -- (λ a b f,         sigma.equal id_right sorry)
+  end arrow
+
+
+  -- definition foo {obC obD : Type} (C : category obC) (D : category obD)
+  --     : category (obC × obD) :=
+  -- mk (λa b, sorry)
+  --    (λ a b c g f, sorry)
+  --    (λ a, sorry)
+  --    (λ a b c d h g f, sorry)
+  --    (λ a b f, sorry)
+  --    (λ a b f, sorry)
+
+end category
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index b5707aafa..343087f33 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -27,19 +27,59 @@ section
 
   theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
     dpair a₁ b₁ = dpair a₂ b₂ :=
-  eq.rec_on H₁
-    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂),
-      calc
-        dpair a₁ b₁ = dpair a₁ (eq.rec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
-                ... = dpair a₁ b₂                : {H₂})
-    b₂ H₁ H₂
+  congr_arg2 dpair H₁ H₂
 
   protected theorem equal {p₁ p₂ : Σx : A, B x} :
-    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = (dpr2 p₂)), p₁ = p₂ :=
+    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
   protected theorem is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
     inhabited (sigma B) :=
   inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b)))
 end
+
+section trip_quad
+  parameters {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
+
+  definition dtrip (a : A) (b : B a) (c : C a b) := dpair a (dpair b c)
+  definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := dpair a (dpair b (dpair c d))
+
+  definition dpr1' (x : Σ a, B a) := dpr1 x
+  definition dpr2' (x : Σ a b, C a b) := dpr1 (dpr2 x)
+  definition dpr3  (x : Σ a b, C a b) := dpr2 (dpr2 x)
+  definition dpr3' (x : Σ a b c, D a b c) := dpr1 (dpr2 (dpr2 x))
+  definition dpr4  (x : Σ a b c, D a b c) := dpr2 (dpr2 (dpr2 x))
+
+  -- theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
+  --     (H₁ : a₁ = a₂)  (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
+  --   dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
+  -- eq.rec_on H₁
+  --   (λ (b₂ : B a₁) (c₂ : C a₁ b₂) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂)
+  --       (x : (eq (eq.rec_on (congr_arg2 C H₁ H₂) c₁) c₂)), sorry
+  --     -- have H : dpair b₁ c₁ = dpair b₂ c₂, from
+  --     --   dpair_eq H₂ (eq.subst (eq.rec_on_id H₁ c₁) H₃),
+  --     -- eq.subst H rfl
+  --   )
+  --   b₂ c₂ H₁ H₂ H₃
+end trip_quad
+
+  theorem dtrip_eq2 {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
+      {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂)
+      (H₃ : eq.rec_on H₂ (eq.rec_on H₁ c₁) = c₂) :
+    dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
+  eq.rec_on H₁
+    (λ (b₂ : B) (c₂ : C a₁ b₂) (H₁ : a₁ = a₁) (H₂ : b₁ = b₂)
+        (H₃ : eq.rec_on H₂ (eq.rec_on H₁ c₁) = c₂),
+      have H : dpair b₁ c₁ = dpair b₂ c₂, from
+        dpair_eq H₂ (eq.subst (eq.rec_on_id H₁ c₁) H₃),
+      eq.subst H rfl
+    )
+    b₂ c₂ H₁ H₂ H₃
+
+  theorem trip.equal2 {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
+      ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : dpr2' p₁ = dpr2' p₂)
+      (H₃ : eq.rec_on H₂ (eq.rec_on H₁ (dpr3 p₁)) = dpr3 p₂), p₁ = p₂ :=
+  destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
+    (take b₂ c₂ H₁ H₂ H₃, dtrip_eq2 H₁ H₂ H₃))))
+
 end sigma
diff --git a/library/hott/path.lean b/library/hott/path.lean
index e0e5ea636..b13047192 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -40,9 +40,9 @@ infixl `@`:75 := concat
 postfix `^`:100 := inverse
 
 -- In Coq, these are not needed, because concat and inv are kept transparent
-definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp
+-- definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp
 
-definition concat_11 {A : Type} (x : A) : idpath x @ idpath x ≈ idpath x := idp
+-- definition concat_11 {A : Type} (x : A) : idpath x @ idpath x ≈ idpath x := idp
 
 
 -- The 1-dimensional groupoid structure
diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean
index 799851b78..efc3cbc20 100644
--- a/library/logic/core/eq.lean
+++ b/library/logic/core/eq.lean
@@ -71,6 +71,16 @@ H ▸ rfl
 theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
 H ▸ rfl
 
+theorem congr_arg2 {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
+    {b₁ : B a₁} {b₂ : B a₂} (f : Πa, B a → C) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
+    f a₁ b₁ = f a₂ b₂ :=
+  eq.rec_on H₁
+    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.rec_on H₁ b₁ = b₂),
+      calc
+        f a₁ b₁ = f a₁ (eq.rec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
+            ... = f a₁ b₂                : {H₂})
+    b₂ H₁ H₂
+
 theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
   f a = g b :=
 H1 ▸ H2 ▸ rfl
@@ -99,6 +109,9 @@ assume Ha, H2 ▸ (H1 Ha)
 theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
 assume Ha, H2 (H1 ▸ Ha)
 
+-- proof irrelevance is built in the kernel
+theorem proof_irrel {a : Prop} {H1 H2 : a} : H1 = H2 := rfl
+
 -- ne
 -- --