Skip to content

Instantly share code, notes, and snippets.

@kbuzzard

kbuzzard/gist:8cd788951b49a3ff536c3dce71e085e0

Created April 30, 2020 17:56
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/8cd788951b49a3ff536c3dce71e085e0 to your computer and use it in GitHub Desktop.
Save kbuzzard/8cd788951b49a3ff536c3dce71e085e0 to your computer and use it in GitHub Desktop.
Download ZIP
diff
Raw
gistfile1.txt
5,6c5,9
< (@category_theory.functor.obj.{v v u u} C π’ž C π’ž
< (@category_theory.exp.functor.{v u} C π’ž
---
> (@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 π’ž
8,13c11,12
< 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))
< (@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)))
---
> (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
> A)))
32,33c31,35
< (@category_theory.functor.obj.{v v u u} C π’ž C π’ž
< (@category_theory.exp.functor.{v u} C π’ž
---
> (@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 π’ž
35,40c37,38
< 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))
< (@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s))))
---
> (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
> A))))
58,59c56,60
< (@category_theory.functor.obj.{v v u u} C π’ž C π’ž
< (@category_theory.exp.functor.{v u} C π’ž
---
> (@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 π’ž
61,66c62,63
< 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))
< (@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s))))
---
> (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
> A))))
75,78c72,80
< (@category_theory.exp.functor.{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.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 π’ž
80,81c82,86
< (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
< A))
---
> 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)))
105,106c110,114
< (@category_theory.functor.obj.{v v u u} C π’ž C π’ž
< (@category_theory.exp.functor.{v u} C π’ž
---
> (@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 π’ž
108,113c116,117
< 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))
< (@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)))
---
> (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
> A)))
131,132c135,139
< (@category_theory.functor.obj.{v v u u} C π’ž C π’ž
< (@category_theory.exp.functor.{v u} C π’ž
---
> (@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 π’ž
134,139c141,142
< 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))
< (@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)))
---
> (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
> A)))
169,170c172,176
< (@category_theory.functor.obj.{v v u u} C π’ž C π’ž
< (@category_theory.exp.functor.{v u} C π’ž
---
> (@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 π’ž
172,177c178,179
< 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))
< (@sheaf'.A.{v u} C π’ž _inst_1 _inst_2 j _inst_3 s)))
---
> (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
> A)))
186,189c188,196
< (@category_theory.exp.functor.{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.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 π’ž
191,192c198,202
< (@category_theory.cc_of_lcc.{v u} C π’ž _inst_1 (@lcc_of_pow.{v u} C π’ž _inst_1 _inst_2))
< A))
---
> 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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment