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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI can understand the operation of unfolding an entity in terms of coalgebra. E.g., for the endofunctor on Set, F(X) = 1 + X, I can unfold a potentially infinite stream of 1s, writing 'stop' and ending, or '1' and taking the predecessor. Can I think of unfolding a connected topological space into its [[Postnikov system]] in a similar way?

   I can understand the operation of unfolding an entity in terms of coalgebra. E.g., for the endofunctor on Set, F(X) = 1 + X, I can unfold a potentially infinite stream of 1s, writing ’stop’ and ending, or ’1’ and taking the predecessor.

   Can I think of unfolding a connected topological space into its Postnikov system in a similar way?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeMar 26th 2012
   • (edited Mar 26th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI am not sure if we can get this from a single endofunctor. But the Postnikov tower of an object $X$ $$ \cdots \to \tau_3 X \to \tau_2 X \to \tau_1 X \to \tau_0 X $$ comes from a tower of endofunctors $$ \cdots \mathbf{H} \stackrel{\tau_3}{\to} \mathbf{H} \stackrel{\tau_2}{\to} \mathbf{H} \stackrel{\tau_1}{\to} \mathbf{H} \stackrel{\tau_0}{\to} \mathbf{H} \,, $$ where $\mathbf{H}$ is the ambient $\infty$-topos and where $\tau_n$ is the [[n-truncated|n-truncation]] $\infty$-functors.

   I am not sure if we can get this from a single endofunctor. But the Postnikov tower of an object $X$

   $$\cdots \to \tau_3 X \to \tau_2 X \to \tau_1 X \to \tau_0 X$$

   comes from a tower of endofunctors

   $$\cdots \mathbf{H} \stackrel{\tau_3}{\to} \mathbf{H} \stackrel{\tau_2}{\to} \mathbf{H} \stackrel{\tau_1}{\to} \mathbf{H} \stackrel{\tau_0}{\to} \mathbf{H} \,,$$

   where $\mathbf{H}$ is the ambient $\infty$-topos and where $\tau_n$ is the n-truncation $\infty$-functors.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think a closer analogy would be to the coinductive definition of an $\infty$-category: a set together with hom-$\infty$-categories and composition. Each unfolding peels off one layer of structure "at the bottom" (first the objects, then the 1-morphisms, then the 2-morphisms, etc.).

   I think a closer analogy would be to the coinductive definition of an $\infty$-category: a set together with hom-$\infty$-categories and composition. Each unfolding peels off one layer of structure “at the bottom” (first the objects, then the 1-morphisms, then the 2-morphisms, etc.).

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexThat seems to give the skeletal filtration instead of the coskeletal/Postnikov tower.

   That seems to give the skeletal filtration instead of the coskeletal/Postnikov tower.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat's true! But it still seems to me to be closer to what David was asking, because the functor F in F(X)=1+X is not the "operation of unfolding", but rather that which *defines* the structure under consideration (here, $\infty$-groupoids) as a coinductive object.

   That’s true! But it still seems to me to be closer to what David was asking, because the functor F in F(X)=1+X is not the “operation of unfolding”, but rather that which defines the structure under consideration (here, $\infty$-groupoids) as a coinductive object.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexThat reminds me of something related (or maybe not so related, I am not sure) that I wanted to ask you: I seem to remember that a while back you said something like: it's unclear how to define internal categories in HTT in, notably, the complete Segal space style, because it requires coding an infinite amount of data. Right? Is that really so? Even outside HTT, in practice we never "code" an infinite amount of data, because we never can. While there is a countable number of objects/types involved in an internal Segal-style category, we never define one by listing these explicitly one-by-one. Instead, we always fall back to some finite algorithm that would produce one. But even before coding examples, could you remind me what the problem is, if any, of coding the _definition_ ? I would imagine we start with an $\mathbb{N}$-dependent type (of morphisms), then have some $\mathbb{N} \times \mathbb{N}$-dependent type of maps (simplicial structure) maps, and so forth. Where does one run into problems?

   That reminds me of something related (or maybe not so related, I am not sure) that I wanted to ask you:

   I seem to remember that a while back you said something like: it’s unclear how to define internal categories in HTT in, notably, the complete Segal space style, because it requires coding an infinite amount of data. Right?

   Is that really so? Even outside HTT, in practice we never “code” an infinite amount of data, because we never can. While there is a countable number of objects/types involved in an internal Segal-style category, we never define one by listing these explicitly one-by-one. Instead, we always fall back to some finite algorithm that would produce one.

   But even before coding examples, could you remind me what the problem is, if any, of coding the definition ? I would imagine we start with an $\mathbb{N}$-dependent type (of morphisms), then have some $\mathbb{N} \times \mathbb{N}$-dependent type of maps (simplicial structure) maps, and so forth.

   Where does one run into problems?

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeMar 26th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe problem is that the "and so forth" stands for an infinite list of things (higher homotopy coherence of the simplicial structure maps).

   The problem is that the “and so forth” stands for an infinite list of things (higher homotopy coherence of the simplicial structure maps).

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeMar 27th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItex> stands for an infinite list of things But it just says: for all $n \in \mathbb{N}$, a certain morphism is weak equivalence. A can't see why this could not be coded. It's just some condition parametrized over the type $\mathbb{N}$.

   stands for an infinite list of things

   But it just says: for all $n \in \mathbb{N}$, a certain morphism is weak equivalence. A can’t see why this could not be coded. It’s just some condition parametrized over the type $\mathbb{N}$.

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 27th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThanks, Urs and Mike. I had the suspicion that the closest analogy would be to the coinductive Trimble $\omega$-category construction, but wondered if we could peel things off the other way. So there's no hope of defining truncation in terms of a single endofunctor.

   Thanks, Urs and Mike. I had the suspicion that the closest analogy would be to the coinductive Trimble $\omega$-category construction, but wondered if we could peel things off the other way. So there’s no hope of defining truncation in terms of a single endofunctor.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex@Urs, I must not understand what you meant by > I would imagine we start with an $\mathbb{N}$-dependent type (of morphisms), then have some $\mathbb{N}\times\mathbb{N}$-dependent type of maps (simplicial structure) maps Actually, what is it you are trying to define? I thought you were describing a simplicial object (so I assumed that by "morphisms" you meant "objects"). @David, I probably wouldn't put it so strongly as "no hope", but it seems that right now, we don't know how to do it. (-:

    @Urs, I must not understand what you meant by

    I would imagine we start with an $\mathbb{N}$-dependent type (of morphisms), then have some $\mathbb{N}\times\mathbb{N}$-dependent type of maps (simplicial structure) maps

    Actually, what is it you are trying to define? I thought you were describing a simplicial object (so I assumed that by “morphisms” you meant “objects”).

    @David, I probably wouldn’t put it so strongly as “no hope”, but it seems that right now, we don’t know how to do it. (-:

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexMike, yes, a simplicial object satisfiying the Segal condition. Why can't this be coded in Coq?

    Mike,

    yes, a simplicial object satisfiying the Segal condition. Why can’t this be coded in Coq?

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe problem is not the Segal condition, the problem is the "simplicial object". The Segal condition says "for all n, a certain morphism is an equivalence" — probably no problem with that. But please tell me how you plan to encode a simplicial object?

    The problem is not the Segal condition, the problem is the “simplicial object”. The Segal condition says “for all n, a certain morphism is an equivalence” — probably no problem with that. But please tell me how you plan to encode a simplicial object?

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012
    • (edited Mar 27th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> But please tell me how you plan to encode a simplicial object? "Plan" is a good word. Here is one plan: first I imagine I'd encode the easy bit: the notion of simplicial _0-truncated_ objects (all whose components are 0-truncated). I hear this has been done already, with the aim of building models for HoTT inside HoTT. (Maybe I should assume for this that there is a subcategory of discrete objects? Of course I'd be happy with making that assumption.) Similarly I'd define globular 0-truncated objects and, using Street's combinatorics, the globular nerve operation, all on these degreewise 0-truncated structures. Then I imagine that I can get hold of the simplicial 0-truncated object which is the nerve of $\Delta$, as well as of its globularization $N_G(\Delta)$. Then I'd imaging that I can say that a simplicial object is * For every term $ v \in N_G(\Delta)_0$ a type $X_v$. * For all $n \in \mathbb{N}$ and every term $\sigma \in N_G(\Delta)_{n+1}$, a term in $Id^{n} (source_0(\sigma) \to target_0(\sigma))$ (the $n$-fold identity type on the function type between the 0-source type of $\sigma$ and the 0-target type of $\sigma$). * Together with a choice of the relevant equivalences. So, in summary: I first say "simplicial 0-truncated object", which should be straightforward since we may indeed speak of simplicial _identities_ in this case. Then I'd define a specific simplicial 0-truncated object and use that now as a blueprint from which to read off, degree by degree, the "infinite amount of coherence data".

    But please tell me how you plan to encode a simplicial object?

    "Plan" is a good word. Here is one plan:

    first I imagine I’d encode the easy bit: the notion of simplicial 0-truncated objects (all whose components are 0-truncated). I hear this has been done already, with the aim of building models for HoTT inside HoTT. (Maybe I should assume for this that there is a subcategory of discrete objects? Of course I’d be happy with making that assumption.) Similarly I’d define globular 0-truncated objects and, using Street’s combinatorics, the globular nerve operation, all on these degreewise 0-truncated structures.

    Then I imagine that I can get hold of the simplicial 0-truncated object which is the nerve of $\Delta$, as well as of its globularization $N_G(\Delta)$.

    Then I’d imaging that I can say that a simplicial object is

    • For every term $v \in N_G(\Delta)_0$ a type $X_v$.

    • For all $n \in \mathbb{N}$ and every term $\sigma \in N_G(\Delta)_{n+1}$, a term in $Id^{n} (source_0(\sigma) \to target_0(\sigma))$ (the $n$-fold identity type on the function type between the 0-source type of $\sigma$ and the 0-target type of $\sigma$).

    • Together with a choice of the relevant equivalences.

    So, in summary: I first say "simplicial 0-truncated object", which should be straightforward since we may indeed speak of simplicial identities in this case. Then I’d define a specific simplicial 0-truncated object and use that now as a blueprint from which to read off, degree by degree, the "infinite amount of coherence data".

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhere did you hear that simplicial 0-truncated objects have been done? I agree that it should not be as hard (in fact, I've been working on something similar). I think the problem then with your plan is saying what you mean precisely by "$n$-fold identity type" and/or "relevant equivalences" (depending on how you partition up the important information between those two things). I don't know how to convince you that this is hard other than by saying "try to do it!"

    Where did you hear that simplicial 0-truncated objects have been done? I agree that it should not be as hard (in fact, I’ve been working on something similar).

    I think the problem then with your plan is saying what you mean precisely by “$n$-fold identity type” and/or “relevant equivalences” (depending on how you partition up the important information between those two things). I don’t know how to convince you that this is hard other than by saying “try to do it!”

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Where did you hear that simplicial 0-truncated objects have been done? Over coffee, from a colleague who is in contact with the person who supposedly did it. I'll get back to you tomorrow with details.

    Where did you hear that simplicial 0-truncated objects have been done?

    Over coffee, from a colleague who is in contact with the person who supposedly did it. I’ll get back to you tomorrow with details.

16. • CommentRowNumber16.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 28th 2012
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexMike and I had a little discussion on the cafe about trying to construct simplicial objects, but I can't find it. I suggested using the decalage, I think, but it didn't go anywhere (or I didn't think about it long enough, most likely the former).

    Mike and I had a little discussion on the cafe about trying to construct simplicial objects, but I can’t find it. I suggested using the decalage, I think, but it didn’t go anywhere (or I didn’t think about it long enough, most likely the former).

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMar 28th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItex> I suggested using the decalage, To accoumplish what?

    I suggested using the decalage,

    To accoumplish what?

18. • CommentRowNumber18.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 28th 2012
    • (edited Mar 28th 2012)
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexTo define simplicial objects in Coq. I should say, use the decalage, _truncated_ simplicial objects and maps of truncated simplicial objects so we define simplicial objects and the map from the decalage jointly. Unfortunately my google-foo and n-category-cafe-searching-foo have let me down.

    To define simplicial objects in Coq. I should say, use the decalage, truncated simplicial objects and maps of truncated simplicial objects so we define simplicial objects and the map from the decalage jointly. Unfortunately my google-foo and n-category-cafe-searching-foo have let me down.

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMar 28th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex[fu](http://golem.ph.utexas.edu/category/2011/10/prequantum_physics_in_a_cohesi.html#c039941)?

    fu?

20. • CommentRowNumber20.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 29th 2012
    • (edited Mar 29th 2012)
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex...if you like.... And here's me thinking you'd found the discussion.

    …if you like….

    And here’s me thinking you’d found the discussion.

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWas that not the discussion you were thinking of?

    Was that not the discussion you were thinking of?

22. • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 29th 2012
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexSorry, I didn't see the link because I was using my phone on the bus. I thought it was a linguistic comment on my post. That is exactly the one, thanks! @Urs - I hope you can make something of my idea, or perhaps a completely different approach is needed, say along the lines you mentioned (0-truncated objects etc).

    Sorry, I didn’t see the link because I was using my phone on the bus. I thought it was a linguistic comment on my post. That is exactly the one, thanks!

    @Urs - I hope you can make something of my idea, or perhaps a completely different approach is needed, say along the lines you mentioned (0-truncated objects etc).

23. • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeMar 29th 2012
    • (edited Mar 29th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> I hope you can make something of my idea, A coinductive definition as Mike and maybe you (not sure if I understood yet!) allude to would probably be way more elegant than what I was sketching. I am not so much interested in picking an implementation, since I won't do it any time soon anyway! I was more interested in understanding if in principle there is any obstacle to formulating categories internal to Coq, an obstacle due to the definition involving "an infinite amount" of information. It would seem to me that also outside of Coq we can never make a definition that genuinely involves an infinite amount of data. If it looks as if we do, then always because some finite algorithms for producing that data are secretly understood in the background, maybe so secretly that we don't notice it anymore.

    I hope you can make something of my idea,

    A coinductive definition as Mike and maybe you (not sure if I understood yet!) allude to would probably be way more elegant than what I was sketching. I am not so much interested in picking an implementation, since I won’t do it any time soon anyway!

    I was more interested in understanding if in principle there is any obstacle to formulating categories internal to Coq, an obstacle due to the definition involving “an infinite amount” of information. It would seem to me that also outside of Coq we can never make a definition that genuinely involves an infinite amount of data. If it looks as if we do, then always because some finite algorithms for producing that data are secretly understood in the background, maybe so secretly that we don’t notice it anymore.

24. • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexUrs, I agree that we never actually write down an infinite amount of data (obviously, we only have finite paper...). I see that I should have been more specific about the problem. The problem is that in formalizing an infinite amount of coherence data in a "homotopically coherent diagram" (or any homotopically coherent structure), it seems as though we need to use some notion of strict identity. E.g. the source of the associator constraint has to *be* $f \circ (g\circ h)$. We could ask it to only be isomorphic/equivalent, but then that isomorphism/equivalence has to have an exactly specified source and target, etc. We had a discussion about this sort of thing a while ago at [[evil]], with the point being made that we can make do with *type dependency* as a replacement for a notion of strict identity. That is, rather than saying that "the source of the associator is $f\circ (g\circ h)$ and its target is $(f\circ g)\circ h$", which regarded as a statement involves strict equality, we give the associator the dependent type $Hom(f\circ (g\circ h), (f\circ g)\circ h)$. In principle, and in informal mathematics, this works great. However, when formalizing in type theory, we don't have fully general *language* to talk *internally* about type dependency. For instance, type theory cannot formalize the statement "the map $f$ is a fibration (i.e. display map, dependent type)". We can say "let $f\colon A\to B$ be a fibration" by way of introducing the variable $f$ and the type $A$ (by translating it into "let $F\colon B\to Type$ be a dependent type") but not assert that some already-known map is a fibration. A natural numbers type allows us to talk about "an infinite family of objects" $\{X_n\}_{n\in N}$ as an $N$-indexed type $X\colon N\to Type$, and a family of morphisms $f_{n}\colon X_{n+1} \to X_{n}$ as a dependent function $f\colon \forall n\colon N, X(n+1) \to X(n)$. But there is no obvious way to talk about an infinite tower of *fibrations* $$ \dots \twoheadrightarrow X_{n+1}\twoheadrightarrow X_n \twoheadrightarrow \dots \twoheadrightarrow X_0 $$ This is where the drive to coinduction comes from, because there is a way to formalize such a thing coinductively: CoInductive tower : Type := | lift : forall X0 : Type, (X0 -> tower) -> tower. But for more complicated infinite structures involving fibrations, there's no general formula for how to coinductivify them that I know of. Does that help at all? I wouldn't say that there is an "in principle obstacle" in the sense of an argument that it *can't* be done, but I think this is an "in principle" reason why it is *difficult*, and why no one has done it yet. (-:

    Urs, I agree that we never actually write down an infinite amount of data (obviously, we only have finite paper…). I see that I should have been more specific about the problem. The problem is that in formalizing an infinite amount of coherence data in a “homotopically coherent diagram” (or any homotopically coherent structure), it seems as though we need to use some notion of strict identity. E.g. the source of the associator constraint has to be $f \circ (g\circ h)$. We could ask it to only be isomorphic/equivalent, but then that isomorphism/equivalence has to have an exactly specified source and target, etc.

    We had a discussion about this sort of thing a while ago at evil, with the point being made that we can make do with type dependency as a replacement for a notion of strict identity. That is, rather than saying that “the source of the associator is $f\circ (g\circ h)$ and its target is $(f\circ g)\circ h$”, which regarded as a statement involves strict equality, we give the associator the dependent type $Hom(f\circ (g\circ h), (f\circ g)\circ h)$. In principle, and in informal mathematics, this works great. However, when formalizing in type theory, we don’t have fully general language to talk internally about type dependency.

    For instance, type theory cannot formalize the statement “the map $f$ is a fibration (i.e. display map, dependent type)”. We can say “let $f\colon A\to B$ be a fibration” by way of introducing the variable $f$ and the type $A$ (by translating it into “let $F\colon B\to Type$ be a dependent type”) but not assert that some already-known map is a fibration. A natural numbers type allows us to talk about “an infinite family of objects” $\{X_n\}_{n\in N}$ as an $N$-indexed type $X\colon N\to Type$, and a family of morphisms $f_{n}\colon X_{n+1} \to X_{n}$ as a dependent function $f\colon \forall n\colon N, X(n+1) \to X(n)$. But there is no obvious way to talk about an infinite tower of fibrations

    $$\dots \twoheadrightarrow X_{n+1}\twoheadrightarrow X_n \twoheadrightarrow \dots \twoheadrightarrow X_0$$

    This is where the drive to coinduction comes from, because there is a way to formalize such a thing coinductively:

    CoInductive tower : Type :=
    | lift : forall X0 : Type, (X0 -> tower) -> tower.
    

    But for more complicated infinite structures involving fibrations, there’s no general formula for how to coinductivify them that I know of.

    Does that help at all? I wouldn’t say that there is an “in principle obstacle” in the sense of an argument that it can’t be done, but I think this is an “in principle” reason why it is difficult, and why no one has done it yet. (-: