Zulip Chat Archive

Stream: general

Topic: timeout with structure command


Yuma Mizuno (Feb 23 2022 at 05:44):

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

Last updated: Dec 20 2023 at 11:08 UTC