Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 21st 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexAt [[natural deduction]] it says > natural deduction with computation rules gives a formulation of [[computation]]. See [[computational trinitarianism]] for discussion of this unification of concepts. But I don't see anything at these links to help explain the role of the C in FIEC (formation-introduction-elimination-computation). Philosophers call the satisfaction of computation rules 'harmony', and there's some reflection on why this is desirable, and of course arguments against. There should presumably be perspectives on this from the three corners of the trinity of trinitarianism. What can we say from the perspectives of computing and of category theory?

   At natural deduction it says

   natural deduction with computation rules gives a formulation of computation. See computational trinitarianism for discussion of this unification of concepts.

   But I don’t see anything at these links to help explain the role of the C in FIEC (formation-introduction-elimination-computation). Philosophers call the satisfaction of computation rules ’harmony’, and there’s some reflection on why this is desirable, and of course arguments against.

   There should presumably be perspectives on this from the three corners of the trinity of trinitarianism. What can we say from the perspectives of computing and of category theory?

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 21st 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexE.g., in the case of category theory, one will want to talk about universal properties. In the case of product, we know this is right adjoint to duplication.

   E.g., in the case of category theory, one will want to talk about universal properties. In the case of product, we know this is right adjoint to duplication.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 21st 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see Mike said some useful things [here](https://mathoverflow.net/questions/177830/question-about-higher-inductive-types-and-computational-rules).

   I see Mike said some useful things here.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 21st 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRight. From the perspective of computation, the computation rules are what allow you to compute. And from the perspective of category theory, they implement universal properties. A (left) universal property is in general a representation of a functor, i.e. an isomorphism between a functor $F$ and a representable functor $\hom(X,-)$. The introduction rule is the map $\hom(X,-) \to F$ (or its Yoneda reduct, an element of $F(X)$); the elimination rule is the map $F \to \hom(X,-)$; the computation rule says that the composite $F \to \hom(X,-) \to F$ is the identity; and the uniqueness rule says that the composite $\hom(X,-) \to F \to\hom(X,-)$ is the identity.

   Right. From the perspective of computation, the computation rules are what allow you to compute. And from the perspective of category theory, they implement universal properties. A (left) universal property is in general a representation of a functor, i.e. an isomorphism between a functor $F$ and a representable functor $\hom(X,-)$. The introduction rule is the map $\hom(X,-) \to F$ (or its Yoneda reduct, an element of $F(X)$); the elimination rule is the map $F \to \hom(X,-)$; the computation rule says that the composite $F \to \hom(X,-) \to F$ is the identity; and the uniqueness rule says that the composite $\hom(X,-) \to F \to\hom(X,-)$ is the identity.

5. • CommentRowNumber5.
   • CommentAuthorSam Staton
   • CommentTimeFeb 22nd 2018
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexMy understanding is that the universal properties give you equations, such as beta/eta equations. But it is another thing to build (compute?) a normal form, which typically requires orienting the equations, such as beta reduction and eta expansion. Perhaps this is what Mike meant by "implement". I am not sure whether "computation" refers to the equations or to their oriented forms.

   My understanding is that the universal properties give you equations, such as beta/eta equations. But it is another thing to build (compute?) a normal form, which typically requires orienting the equations, such as beta reduction and eta expansion. Perhaps this is what Mike meant by “implement”. I am not sure whether “computation” refers to the equations or to their oriented forms.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 22nd 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexRe #5, does this point to the reason for looking to bicategories to represent computation, as in the work John Baez and Mike Stay were doing (and no doubt many others).

   Re #5, does this point to the reason for looking to bicategories to represent computation, as in the work John Baez and Mike Stay were doing (and no doubt many others).

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 22nd 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexRe #4, thanks, Mike. So could one do some counterfactual 'trinitarian' history where the computer scientist sees the need for universal properties? And another where the category theorist foresees the need for formation-introduction-elimination-computation? I see at [[representability determines functoriality]] it claims that the lemma there >gives an explanation for why the “dogma” of introduction and elimination rules is so effective in practice.

   Re #4, thanks, Mike. So could one do some counterfactual ’trinitarian’ history where the computer scientist sees the need for universal properties? And another where the category theorist foresees the need for formation-introduction-elimination-computation?

   I see at representability determines functoriality it claims that the lemma there

   gives an explanation for why the “dogma” of introduction and elimination rules is so effective in practice.

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 22nd 2018
   • (edited Feb 22nd 2018)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexAnother thing, the page speaks of "this lemma", but nowhere is anything titled 'Lemma'. Presumably it's the final two sentences of section 3. [edit: this should have been on the other thread, but has been acted on.]

   Another thing, the page speaks of “this lemma”, but nowhere is anything titled ’Lemma’. Presumably it’s the final two sentences of section 3.

   [edit: this should have been on the other thread, but has been acted on.]

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 22nd 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRe #7, I guess so. Re #5, that's true, there is a difference there. Maybe the thing to say is that the "computation rules" (including uniqueness rules) can "often" be oriented to determine an operational notion of computation?

   Re #7, I guess so.

   Re #5, that’s true, there is a difference there. Maybe the thing to say is that the “computation rules” (including uniqueness rules) can “often” be oriented to determine an operational notion of computation?