Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/gist:81c432ac5a5282a4baf3ce789e358519

Created April 30, 2020 17:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kbuzzard/81c432ac5a5282a4baf3ce789e358519 to your computer and use it in GitHub Desktop.
Save kbuzzard/81c432ac5a5282a4baf3ce789e358519 to your computer and use it in GitHub Desktop.
Download ZIP
goal
Raw
gistfile1.txt
@eq.{v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C (@category_theory.category.to_category_struct.{v u} C π’ž))
B
(@category_theory.exp.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
(@coe_fn.{(max 1 (v+1)) v+1}
(equiv.{v+1 v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
(@category_theory.limits.prod.{v u} C π’ž A B
(@category_theory.limits.has_limit_of_has_limits_of_shape.{v u} C π’ž
(category_theory.discrete.{v} category_theory.limits.walking_pair.{v})
(category_theory.discrete_category.{v} category_theory.limits.walking_pair.{v})
(@category_theory.limits.has_binary_products.has_limits_of_shape.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
(@category_theory.limits.pair.{v u v} C π’ž A B)))
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s))
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
B
(@category_theory.exp.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A))))
(@equiv.has_coe_to_fun.{v+1 v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
(@category_theory.limits.prod.{v u} C π’ž A B
(@category_theory.limits.has_limit_of_has_limits_of_shape.{v u} C π’ž
(category_theory.discrete.{v} category_theory.limits.walking_pair.{v})
(category_theory.discrete_category.{v} category_theory.limits.walking_pair.{v})
(@category_theory.limits.has_binary_products.has_limits_of_shape.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
(@category_theory.limits.pair.{v u v} C π’ž A B)))
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s))
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
B
(@category_theory.exp.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A))))
(@category_theory.adjunction.hom_equiv.{v v u u} C π’ž C π’ž
(@category_theory.functor.obj.{v (max u v) u (max v u)} C π’ž
(@category_theory.functor.{v v u u} C π’ž C π’ž)
(@category_theory.functor.category.{v v u u} C π’ž C π’ž)
(@category_theory.limits.prod_functor.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
A)
(@category_theory.is_left_adjoint.right.{v v u u} C π’ž C π’ž
(@category_theory.functor.obj.{v (max u v) u (max v u)} C π’ž
(@category_theory.functor.{v v u u} C π’ž C π’ž)
(@category_theory.functor.category.{v v u u} C π’ž C π’ž)
(@category_theory.limits.prod_functor.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
A)
(@category_theory.exponentiable.is_adj.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
(@category_theory.is_left_adjoint.adj.{v v u u} C π’ž C π’ž
(@category_theory.functor.obj.{v (max u v) u (max v u)} C π’ž
(@category_theory.functor.{v v u u} C π’ž C π’ž)
(@category_theory.functor.category.{v v u u} C π’ž C π’ž)
(@category_theory.limits.prod_functor.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
A)
(@category_theory.exponentiable.is_adj.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
B
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s))
(@coe_fn.{(max 1 (v+1)) v+1}
(equiv.{v+1 v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
B
(@category_theory.exp.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
(@category_theory.limits.prod.{v u} C π’ž A B
(@category_theory.limits.has_limit_of_has_limits_of_shape.{v u} C π’ž
(category_theory.discrete.{v} category_theory.limits.walking_pair.{v})
(category_theory.discrete_category.{v} category_theory.limits.walking_pair.{v})
(@category_theory.limits.has_binary_products.has_limits_of_shape.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
(@category_theory.limits.pair.{v u v} C π’ž A B)))
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)))
(@equiv.has_coe_to_fun.{v+1 v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
B
(@category_theory.exp.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
(@category_theory.limits.prod.{v u} C π’ž A B
(@category_theory.limits.has_limit_of_has_limits_of_shape.{v u} C π’ž
(category_theory.discrete.{v} category_theory.limits.walking_pair.{v})
(category_theory.discrete_category.{v} category_theory.limits.walking_pair.{v})
(@category_theory.limits.has_binary_products.has_limits_of_shape.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
(@category_theory.limits.pair.{v u v} C π’ž A B)))
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)))
(@equiv.symm.{v+1 v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
(@category_theory.limits.prod.{v u} C π’ž A B
(@category_theory.limits.has_limit_of_has_limits_of_shape.{v u} C π’ž
(category_theory.discrete.{v} category_theory.limits.walking_pair.{v})
(category_theory.discrete_category.{v} category_theory.limits.walking_pair.{v})
(@category_theory.limits.has_binary_products.has_limits_of_shape.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
(@category_theory.limits.pair.{v u v} C π’ž A B)))
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s))
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C
(@category_theory.category.to_category_struct.{v u} C π’ž))
B
(@category_theory.exp.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
(@category_theory.adjunction.hom_equiv.{v v u u} C π’ž C π’ž
(@category_theory.functor.obj.{v (max u v) u (max v u)} C π’ž
(@category_theory.functor.{v v u u} C π’ž C π’ž)
(@category_theory.functor.category.{v v u u} C π’ž C π’ž)
(@category_theory.limits.prod_functor.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
A)
(@category_theory.is_left_adjoint.right.{v v u u} C π’ž C π’ž
(@category_theory.functor.obj.{v (max u v) u (max v u)} C π’ž
(@category_theory.functor.{v v u u} C π’ž C π’ž)
(@category_theory.functor.category.{v v u u} C π’ž C π’ž)
(@category_theory.limits.prod_functor.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
A)
(@category_theory.exponentiable.is_adj.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
(@category_theory.is_left_adjoint.adj.{v v u u} C π’ž C π’ž
(@category_theory.functor.obj.{v (max u v) u (max v u)} C π’ž
(@category_theory.functor.{v v u u} C π’ž C π’ž)
(@category_theory.functor.category.{v v u u} C π’ž C π’ž)
(@category_theory.limits.prod_functor.{v u} C π’ž
(@category_theory.limits.category_theory.limits.has_binary_products.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)))
A)
(@category_theory.exponentiable.is_adj.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
A
(@category_theory.is_cartesian_closed.cart_closed.{v u} C π’ž
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C π’ž _inst_1)
(@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
A)))
B
(@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)))
a))
a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment