timeout with structure command

Stream: general

[Yuma Mizuno]

When I tried to define a pseudofunctor between bicategories, I got a timeout at structure line below. The timeout vanished if I removed all . obviously in the definition, but I want to keep them. Why is this so slow? Is there any way to avoid the timeout?

import category_theory.bicategory.basic

namespace category_theory

open_locale bicategory

universes w₁ w₂ v₁ v₂ u₁ u₂

structure pseudofunctor (B : Type u₁) [bicategory.{w₁ v₁} B] (C : Type u₂) [bicategory.{w₂ v₂} C] :=
/- (deterministic) timeout -/
(obj : B → C)
(map {a b : B} : (a ⟶ b) → (obj a ⟶ obj b))
(map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (map f ⟶ map g))
(map_id (a : B) : map (𝟙 a) ⟶ 𝟙 (obj a))
(map_id_inv (a : B) : 𝟙 (obj a) ⟶ map (𝟙 a))
(map_id_self_inv' : ∀ (a : B), map_id a ≫ map_id_inv a = 𝟙 (map (𝟙 a)) . obviously)
(map_id_inv_self' : ∀ (a : B), map_id_inv a ≫ map_id a = 𝟙 (𝟙 (obj a)) . obviously)
(map_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : map (f ≫ g) ⟶ map f ≫ map g)
(map_comp_inv {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : map f ≫ map g ⟶ map (f ≫ g))
(map_comp_self_inv' : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  map_comp f g ≫ map_comp_inv f g = 𝟙 (map (f ≫ g)) . obviously)
(map_comp_inv_self' : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  map_comp_inv f g ≫ map_comp f g = 𝟙 (map f ≫ map g) . obviously)
(map₂_id' : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f) . obviously)
(map₂_comp' : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  map₂ (η ≫ θ) = map₂ η ≫ map₂ θ . obviously)
(map₂_whisker_left' : ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
  map₂ (f ◁ η) = map_comp f g ≫ (map f ◁ map₂ η) ≫ map_comp_inv f h . obviously)
(map₂_whisker_right' : ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  map₂ (η ▷ h) = map_comp f h ≫ (map₂ η ▷ map h) ≫ map_comp_inv g h . obviously)
(map₂_associator' : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  map₂ (α_ f g h).hom = map_comp (f ≫ g) h ≫ (map_comp f g ▷ map h) ≫
    (α_ (map f) (map g) (map h)).hom ≫ (map f ◁ map_comp_inv g h) ≫ map_comp_inv f (g ≫ h) . obviously)
(map₂_left_unitor' : ∀ {a b : B} (f : a ⟶ b),
  map₂ (λ_ f).hom = map_comp (𝟙 a) f ≫ (map_id a ▷ map f) ≫ (λ_ (map f)).hom . obviously)
(map₂_right_unitor' : ∀ {a b : B} (f : a ⟶ b),
  map₂ (ρ_ f).hom = map_comp f (𝟙 b) ≫ (map f ◁ map_id b) ≫ (ρ_ (map f)).hom . obviously)

end category_theory