Not signed in

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

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: axiom of separation

Bottom of Page

1 to 33 of 33

- CommentRowNumber1.
- CommentAuthorTobyBartels
- CommentTimeSep 5th 2011
- PermaLink
Author: TobyBartels
Format: MarkdownItexThis finally exists: [[axiom of separation]].

This finally exists: axiom of separation.
- CommentRowNumber2.
- CommentAuthorMike Shulman
- CommentTimeSep 6th 2011
- PermaLink
Author: Mike Shulman
Format: MarkdownItexHooray, thanks! I edited the comment about autology to accord with my answer in the [other thread](http://www.math.ntnu.no/~stacey/Mathforge/nForum/comments.php?DiscussionID=3100&page=1#Comment_25739).

Hooray, thanks! I edited the comment about autology to accord with my answer in the other thread.
- CommentRowNumber3.
- CommentAuthorFinnLawler
- CommentTimeJan 20th 2014
- PermaLink
Author: FinnLawler
Format: MarkdownItexNew page at [[comprehension]], describing Lawvere's version of the comprehension schema in a hyperdoctrine, and also Jacobs's variant.

New page at comprehension, describing Lawvere’s version of the comprehension schema in a hyperdoctrine, and also Jacobs’s variant.
- CommentRowNumber4.
- CommentAuthorUrs
- CommentTimeJan 21st 2014
- PermaLink
Author: Urs
Format: MarkdownItexThanks, nice, I had not been aware of this. I have added the tautological example (the hyperdoctrine over $Set$ of posets of subsets) to offer the reader help to see what the abstract definition is trying to achieve. Apart from this I made two trivial formatting edits, please feel free to disagree: * gave Lawvere's and Jacobs' definition separate subsection * changed the notation $E X$ for the fibers to $E_X$ (okay?)
Thanks, nice, I had not been aware of this.

I have added the tautological example (the hyperdoctrine over $Set$ of posets of subsets) to offer the reader help to see what the abstract definition is trying to achieve.

Apart from this I made two trivial formatting edits, please feel free to disagree:
- gave Lawvere’s and Jacobs’ definition separate subsection
- changed the notation $E X$ for the fibers to $E_X$ (okay?)
- CommentRowNumber5.
- CommentAuthorUrs
- CommentTimeJan 21st 2014
- PermaLink
Author: Urs
Format: MarkdownItexI have also made "comprehension scheme" a redirect and added links to old entries mentioning comprehension, such as _[[second-order arithmetic]]_ and _[[Trimble on ETCS III]]_. I notice that looking at _[[axiom of separation]]_ that the relation between the two entries remains a bit vague at the moment.

I have also made “comprehension scheme” a redirect and added links to old entries mentioning comprehension, such as second-order arithmetic and Trimble on ETCS III.

I notice that looking at axiom of separation that the relation between the two entries remains a bit vague at the moment.
- CommentRowNumber6.
- CommentAuthorFinnLawler
- CommentTimeJan 21st 2014
- PermaLink
Author: FinnLawler
Format: MarkdownItexLooks fine. I've done some minor tidying-up, and added the example of the category of elements of a presheaf.

Looks fine. I’ve done some minor tidying-up, and added the example of the category of elements of a presheaf.
- CommentRowNumber7.
- CommentAuthorUrs
- CommentTimeJan 21st 2014
- PermaLink
Author: Urs
Format: MarkdownItexSince you use the word "extension" now, should we add a remark that if the right adjoint exists, then it is called "extension". So that "comprehension means that we have extension." Is that the right way of speaking?

Since you use the word “extension” now, should we add a remark that if the right adjoint exists, then it is called “extension”. So that “comprehension means that we have extension.” Is that the right way of speaking?
- CommentRowNumber8.
- CommentAuthorFinnLawler
- CommentTimeJan 21st 2014
- PermaLink
Author: FinnLawler
Format: MarkdownItexYes, good point. I have rephrased things slightly.

Yes, good point. I have rephrased things slightly.
- CommentRowNumber9.
- CommentAuthorUrs
- CommentTimeJan 21st 2014
- (edited Jan 21st 2014)
- PermaLink
Author: Urs
Format: MarkdownItexWe have an old stub entry _[[extension (semantics)]]_ which used to just point to Wikipedia and otherwise receive a link from _[[extensional type theory]]_. I have added a bare minimum to _[[extension (semantics)]]_ and cross-linked it with _[[comprehension]]_.

We have an old stub entry extension (semantics) which used to just point to Wikipedia and otherwise receive a link from extensional type theory.

I have added a bare minimum to extension (semantics) and cross-linked it with comprehension.
- CommentRowNumber10.
- CommentAuthorTobyBartels
- CommentTimeJan 26th 2014
- PermaLink
Author: TobyBartels
Format: MarkdownItexI'm inclined to say that the contents of [[comprehension]] belong in [[axiom of separation]], in the (so far quite brief) section on structural versions. It is the same axiom. (Note that a few axioms called ‘comprehension’ are defined at [[axiom of separation]]; also, [[axiom of comprehension]] and several variants already redirect there, although the particular phrases that currently redirect to [[comprehension]].)

I’m inclined to say that the contents of comprehension belong in axiom of separation, in the (so far quite brief) section on structural versions. It is the same axiom. (Note that a few axioms called ‘comprehension’ are defined at axiom of separation; also, axiom of comprehension and several variants already redirect there, although the particular phrases that currently redirect to comprehension.)
- CommentRowNumber11.
- CommentAuthorUrs
- CommentTimeJan 26th 2014
- PermaLink
Author: Urs
Format: MarkdownItexThat sounds very reasonable to me. I am in favor of merging the entries. (But I won't do it myself, now.)

That sounds very reasonable to me. I am in favor of merging the entries. (But I won’t do it myself, now.)
- CommentRowNumber12.
- CommentAuthorTodd_Trimble
- CommentTimeJan 26th 2014
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexThere's something else called the "comprehensive factorization", but I can't remember now how it goes. Maybe someone can add something to this effect, if it can be made to fit?

There’s something else called the “comprehensive factorization”, but I can’t remember now how it goes. Maybe someone can add something to this effect, if it can be made to fit?
- CommentRowNumber13.
- CommentAuthorUrs
- CommentTimeJan 26th 2014
- PermaLink
Author: Urs
Format: MarkdownItexthere is _[[michaelshulman:comprehensive factorization]]_. But is "comprehensive" here really related to "comprehension"?

there is comprehensive factorization (michaelshulman).

But is “comprehensive” here really related to “comprehension”?
- CommentRowNumber14.
- CommentAuthorTodd_Trimble
- CommentTimeJan 26th 2014
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexThanks, Urs. I'm going to have to study what Mike wrote to remind myself how this is supposed to go, but if I remember correctly there is supposed to be a connection (it was originally called the comprehensive factorization because of some connection with comprehension). It has something to do with generalizing the fact that an external predicate or relation on a set $A$, given by a monomorphism $S \hookrightarrow A$, is 'reified' by a function $A \to \Omega$ or an element $1 \to P(A)$, only that in Mike's context we are replacing relations by discrete op-fibrations over $A$ and functions $A \to \Omega$ by functors $A \to Set$, or at least so in the motivating examples. So comprehension is supposed to be abstracted: in a hyperdoctrine $S: E^{op} \to Pos$ (with motivating example $Sub: E^{op} \to Pos$, with $E$ a topos), comprehension allows us to 'reflect' a predicate $p \in S(E)$ down into a morphism in the base category $E$. In the generalization we consider instead the pseudofunctor $S: E^{op} \to Cat$ corresponding to a fibration, and then factor through a discrete fibration... Sorry, I realize that I'm making a mess here and am speaking something close to gibberish -- I'll have to think harder, or maybe someone can help out. I thought there was supposed to be a connection (due originally to Lawvere).

Thanks, Urs. I’m going to have to study what Mike wrote to remind myself how this is supposed to go, but if I remember correctly there is supposed to be a connection (it was originally called the comprehensive factorization because of some connection with comprehension).

It has something to do with generalizing the fact that an external predicate or relation on a set $A$ , given by a monomorphism $S \hookrightarrow A$ , is ’reified’ by a function $A \to \Omega$ or an element $1 \to P(A)$ , only that in Mike’s context we are replacing relations by discrete op-fibrations over $A$ and functions $A \to \Omega$ by functors $A \to Set$ , or at least so in the motivating examples. So comprehension is supposed to be abstracted: in a hyperdoctrine $S: E^{op} \to Pos$ (with motivating example $Sub: E^{op} \to Pos$ , with $E$ a topos), comprehension allows us to ’reflect’ a predicate $p \in S(E)$ down into a morphism in the base category $E$ . In the generalization we consider instead the pseudofunctor $S: E^{op} \to Cat$ corresponding to a fibration, and then factor through a discrete fibration…

Sorry, I realize that I’m making a mess here and am speaking something close to gibberish – I’ll have to think harder, or maybe someone can help out. I thought there was supposed to be a connection (due originally to Lawvere).
- CommentRowNumber15.
- CommentAuthorTodd_Trimble
- CommentTimeJan 26th 2014
- (edited Jan 26th 2014)
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexWell, instead of watching me babble here, maybe try this [link](http://sqig.math.ist.utl.pt/pub/HermidaC/comp-fact.ps) where Claudio Hermida explains it. At least my memory wasn't completely fabricated. (Maybe to babble a bit further, though, the factorization of a fibration $F \to A$ through a discrete op-fibration is supposed to remind one of a classifier $A \to \Omega$, where $\Omega$ is now standing for $Set$ and $A \to Set$ classifies the discrete op-fibration.)

Well, instead of watching me babble here, maybe try this link where Claudio Hermida explains it. At least my memory wasn’t completely fabricated. (Maybe to babble a bit further, though, the factorization of a fibration $F \to A$ through a discrete op-fibration is supposed to remind one of a classifier $A \to \Omega$ , where $\Omega$ is now standing for $Set$ and $A \to Set$ classifies the discrete op-fibration.)
- CommentRowNumber16.
- CommentAuthorUrs
- CommentTimeJan 26th 2014
- PermaLink
Author: Urs
Format: MarkdownItexAh, thanks. I'll try to read this when I have a minute.

Ah, thanks. I’ll try to read this when I have a minute.
- CommentRowNumber17.
- CommentAuthorFinnLawler
- CommentTimeJan 26th 2014
- PermaLink
Author: FinnLawler
Format: MarkdownItexI was planning to add something on the comprehensive factorization to [[comprehension]] when I got the chance, so I'll do that this evening, and move the whole lot to [[axiom of separation]] at the same time. There's nothing complicated about the factorization system, really: a fibration with full comprehension gives a subfibration of the codomain fibration, and if the resulting 'subtype inclusions' are closed under composition, then that gives you a factorization system on the base category (this is in Carboni et. al., _On localization and stabilization for factorization systems_). The factorization of a morphism is the commuting triangle given by the unit of the reflection. For the subobject fibration of a regular category this is the usual epi-mono factorization, whereas for the presheaf fibration over Cat it gives the factorization of an arbitrary functor into a final functor followed by a discrete fibration.

I was planning to add something on the comprehensive factorization to comprehension when I got the chance, so I’ll do that this evening, and move the whole lot to axiom of separation at the same time.

There’s nothing complicated about the factorization system, really: a fibration with full comprehension gives a subfibration of the codomain fibration, and if the resulting ’subtype inclusions’ are closed under composition, then that gives you a factorization system on the base category (this is in Carboni et. al., On localization and stabilization for factorization systems). The factorization of a morphism is the commuting triangle given by the unit of the reflection. For the subobject fibration of a regular category this is the usual epi-mono factorization, whereas for the presheaf fibration over Cat it gives the factorization of an arbitrary functor into a final functor followed by a discrete fibration.
- CommentRowNumber18.
- CommentAuthorUrs
- CommentTimeJan 26th 2014
- PermaLink
Author: Urs
Format: MarkdownItexWhen you do these edits, I suppose you could cross-link with _[[reflective factorization system]]_ and _[[stable factorization system]]_.

When you do these edits, I suppose you could cross-link with reflective factorization system and stable factorization system.
- CommentRowNumber19.
- CommentAuthorFinnLawler
- CommentTimeJan 26th 2014
- PermaLink
Author: FinnLawler
Format: MarkdownItexRight, I've moved everything to [[axiom of separation]] and added a section on the comprehensive factorization, as well as a redirect from the page [[comprehension]]. I've blanked the latter, but now I'm not sure whether that's the right thing to do in this situation.

Right, I’ve moved everything to axiom of separation and added a section on the comprehensive factorization, as well as a redirect from the page comprehension. I’ve blanked the latter, but now I’m not sure whether that’s the right thing to do in this situation.
- CommentRowNumber20.
- CommentAuthorUrs
- CommentTimeJan 26th 2014
- (edited Jan 26th 2014)
- PermaLink
Author: Urs
Format: MarkdownItexThanks! I have also renamed the now blank page to something (to "comprehension $\gt$ history" as it were, but it does not matter much) (and made sure to kill the automatically created redirect in the process)

Thanks!

I have also renamed the now blank page to something (to “comprehension $\gt$ history” as it were, but it does not matter much) (and made sure to kill the automatically created redirect in the process)
- CommentRowNumber21.
- CommentAuthorMike Shulman
- CommentTimeJan 27th 2014
- PermaLink
Author: Mike Shulman
Format: MarkdownItexCould also cross-link [[factorization system in a 2-category]]?

Could also cross-link factorization system in a 2-category?
- CommentRowNumber22.
- CommentAuthorFinnLawler
- CommentTimeJan 27th 2014
- PermaLink
Author: FinnLawler
Format: MarkdownItexI've given it a mention, beside the link to your page [[michaelshulman:comprehensive factorization]]. (Note to self: read and understand that page!)

I’ve given it a mention, beside the link to your page comprehensive factorization (michaelshulman). (Note to self: read and understand that page!)
- CommentRowNumber23.
- CommentAuthorUrs
- CommentTimeJan 29th 2014
- (edited Jan 29th 2014)
- PermaLink
Author: Urs
Format: MarkdownItexMike just indirectly reminded me elsewhere of my going off into the blue in the thread on Finn's thesis about dependent linear type theory and comprehension. Thinking about it, let me have another go: Isn't it right that: a linear hyperdoctrine having Lawvere-ian comprehension means equivalently that it has a dependent [!-modality](http://ncatlab.org/nlab/show/dependent+linear+type+theory#TheCanonicalComodality) ? Here I am assuming that in the definition of Lawvere-ian comprehension we say we are pushing the tensor unit instead of pushing the terminal object, which anyway seems to be a more robust way of going about it, I'd think. Then following [Ponto-Shulman 12, (4.3)](http://ncatlab.org/nlab/show/dependent+linear+type+theory#TheCanonicalComodality) (and using that by linear Frobenius reciprocity context extension/pullback preserves tensor units) the [linearization functor](http://ncatlab.org/nlab/show/dependent+linear+type+theory#TheCanonicalComodality) $\Sigma$ is $$ \Sigma \;\colon\; \mathbf{H}_{/X} \longrightarrow Mod(X) $$ given by sending any $(p : Y \to X) \in \mathbf{H}_X$ to $p_! 1_Y \in Mod(X)$ and this having a right adjoint $R$ that induces the dependent linear type theory $!_X$-comonad is precisely Lawvere's comprehension in this case. Right?

Mike just indirectly reminded me elsewhere of my going off into the blue in the thread on Finn’s thesis about dependent linear type theory and comprehension. Thinking about it, let me have another go:

Isn’t it right that: a linear hyperdoctrine having Lawvere-ian comprehension means equivalently that it has a dependent !-modality

?

Here I am assuming that in the definition of Lawvere-ian comprehension we say we are pushing the tensor unit instead of pushing the terminal object, which anyway seems to be a more robust way of going about it, I’d think.

Then following Ponto-Shulman 12, (4.3) (and using that by linear Frobenius reciprocity context extension/pullback preserves tensor units) the linearization functor $\Sigma$ is
$\Sigma \;\colon\; \mathbf{H}_{/X} \longrightarrow Mod(X)$
given by sending any $(p : Y \to X) \in \mathbf{H}_X$ to $p_! 1_Y \in Mod(X)$ and this having a right adjoint $R$ that induces the dependent linear type theory $!_X$ -comonad is precisely Lawvere’s comprehension in this case.

Right?
- CommentRowNumber24.
- CommentAuthorMike Shulman
- CommentTimeJan 29th 2014
- PermaLink
Author: Mike Shulman
Format: MarkdownItexYes, exactly. That's what I was trying to say "elsewhere".

Yes, exactly. That’s what I was trying to say “elsewhere”.
- CommentRowNumber25.
- CommentAuthorUrs
- CommentTimeJan 29th 2014
- PermaLink
Author: Urs
Format: MarkdownItexOkay, thanks. I have now briefly recorded this at _[comprehension -- Examples -- In linear dependent type theory](http://ncatlab.org/nlab/show/axiom+of+separation#ExamplesDependentLinearTypeTheory)_. Also cross-linked with _[[dependent linear type theory]]_. Created a stub for _[[!-modality]]_ in the process.

Okay, thanks.

I have now briefly recorded this at comprehension – Examples – In linear dependent type theory. Also cross-linked with dependent linear type theory.

Created a stub for !-modality in the process.
- CommentRowNumber26.
- CommentAuthorNoam_Zeilberger
- CommentTimeFeb 23rd 2016
- PermaLink
Author: Noam_Zeilberger
Format: MarkdownItexThis is a minor comment, but I did some digging up of references and noticed that what is described in the article as "Jacobs' reformulation" is actually from Thomas Ehrhard's thesis. That is stated clearly in Jacobs' older article, "Comprehension categories and the semantics of type dependency", and see also Ehrhard's [A Categorical Semantics of Constructions](https://www.irif.univ-paris-diderot.fr/~ehrhard/pub/categ-sem-constr.pdf). I don't have time to edit the article now, but will try to do it next week if no one gets around to it earlier.

This is a minor comment, but I did some digging up of references and noticed that what is described in the article as “Jacobs’ reformulation” is actually from Thomas Ehrhard’s thesis. That is stated clearly in Jacobs’ older article, “Comprehension categories and the semantics of type dependency”, and see also Ehrhard’s A Categorical Semantics of Constructions. I don’t have time to edit the article now, but will try to do it next week if no one gets around to it earlier.
- CommentRowNumber27.
- CommentAuthortonyjones
- CommentTimeFeb 27th 2016
- PermaLink
Author: tonyjones
Format: MarkdownItexAny thoughts on Bart Jacobs recent work on Quotient-Comprehension Chains? <http://arxiv.org/abs/1511.01570> ''This paper reveals that quotients and comprehension are related to measurement, not only in quantum logic, but also in probabilistic and classical logic'' Also his work on the notion of effectus? <http://arxiv.org/abs/1512.05813> "Effectus theory is a new branch of categorical logic that aims to capture the essentials of quantum logic, with probabilistic and Boolean logic as special cases. Predicates in effectus theory are not subobjects having a Heyting algebra structure, like in topos theory, but `characteristic' functions, forming effect algebras. Such effect algebras are algebraic models of quantitative logic, in which double negation holds. Effects in quantum theory and fuzzy predicates in probability theory form examples of effect algebras."

Any thoughts on Bart Jacobs recent work on Quotient-Comprehension Chains? http://arxiv.org/abs/1511.01570 ”This paper reveals that quotients and comprehension are related to measurement, not only in quantum logic, but also in probabilistic and classical logic”

Also his work on the notion of effectus? http://arxiv.org/abs/1512.05813 “Effectus theory is a new branch of categorical logic that aims to capture the essentials of quantum logic, with probabilistic and Boolean logic as special cases. Predicates in effectus theory are not subobjects having a Heyting algebra structure, like in topos theory, but ‘characteristic’ functions, forming effect algebras. Such effect algebras are algebraic models of quantitative logic, in which double negation holds. Effects in quantum theory and fuzzy predicates in probability theory form examples of effect algebras.”
- CommentRowNumber28.
- CommentAuthorMike Shulman
- CommentTimeDec 3rd 2018
- PermaLink
Author: Mike Shulman
Format: MarkdownItexAs far as I can tell, Ehrhard's definition of comprehension requires not just that the fibers have terminal objects but that these are preserved by the reindexing functors. This is automatic if the fibration is a bifibration, as in Lawvere's version; it's fairly explicit in Ehrhard's formulation, and somewhat implicit in Jacobs' but I believe still present (his "terminal object functor" must, I think, be a *fibered* terminal object). <a href="https://ncatlab.org/nlab/revision/diff/axiom+of+separation/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/axiom+of+separation/14">v14</a>, <a href="https://ncatlab.org/nlab/show/axiom+of+separation">current</a>

As far as I can tell, Ehrhard’s definition of comprehension requires not just that the fibers have terminal objects but that these are preserved by the reindexing functors. This is automatic if the fibration is a bifibration, as in Lawvere’s version; it’s fairly explicit in Ehrhard’s formulation, and somewhat implicit in Jacobs’ but I believe still present (his “terminal object functor” must, I think, be a fibered terminal object).

diff, v14, current
- CommentRowNumber29.
- CommentAuthorMike Shulman
- CommentTimeDec 3rd 2018
- PermaLink
Author: Mike Shulman
Format: MarkdownItexBTW, this new thread could be merged with [this one](https://nforum.ncatlab.org/discussion/5616/comprehension/) and (more obviously, but less interestingly) [this one](https://nforum.ncatlab.org/discussion/3099/the-axiom-of-separation/).

BTW, this new thread could be merged with this one and (more obviously, but less interestingly) this one.
- CommentRowNumber30.
- CommentAuthorRichard Williamson
- CommentTimeDec 3rd 2018
- PermaLink
Author: Richard Williamson
Format: MarkdownItexRe #29: Done. Comments #1 and #2 are from a Latest Changes thread entitled 'The axiom of separation', the second of the two threads that Mike mentioned. Comments #3- #27 are from a Latest Changes thread entitled 'comprehension', the first of the two threads that Mike mentioned.

Re #29: Done. Comments #1 and #2 are from a Latest Changes thread entitled ’The axiom of separation’, the second of the two threads that Mike mentioned. Comments #3- #27 are from a Latest Changes thread entitled ’comprehension’, the first of the two threads that Mike mentioned.
- CommentRowNumber31.
- CommentAuthornLab edit announcer
- CommentTimeOct 24th 2022
- PermaLink
Author: nLab edit announcer
Format: MarkdownItexAdding disambiguation message to top of page Anonymous <a href="https://ncatlab.org/nlab/revision/diff/axiom+of+separation/19">diff</a>, <a href="https://ncatlab.org/nlab/revision/axiom+of+separation/19">v19</a>, <a href="https://ncatlab.org/nlab/show/axiom+of+separation">current</a>

Adding disambiguation message to top of page

Anonymous

diff, v19, current
- CommentRowNumber32.
- CommentAuthorrisingtides
- CommentTimeOct 29th 2023
- PermaLink
Author: risingtides
Format: MarkdownItexAdd a temporary reference to Shulman's paper (https://arxiv.org/abs/1004.3802) for the definition of autological category. An "autological category" page should be made eventually (or created as a subsection of the "axiom of separation" page). <a href="https://ncatlab.org/nlab/revision/diff/axiom+of+separation/23">diff</a>, <a href="https://ncatlab.org/nlab/revision/axiom+of+separation/23">v23</a>, <a href="https://ncatlab.org/nlab/show/axiom+of+separation">current</a>

Add a temporary reference to Shulman’s paper (https://arxiv.org/abs/1004.3802) for the definition of autological category. An “autological category” page should be made eventually (or created as a subsection of the “axiom of separation” page).

diff, v23, current
- CommentRowNumber33.
- CommentAuthorvarkor
- CommentTimeNov 29th 2023
- PermaLink
Author: varkor
Format: MarkdownItexAdded a reference to [[Clemens Berger]] and [[Ralph M. Kaufmann]]'s *Comprehensive Factorization Systems*. <a href="https://ncatlab.org/nlab/revision/diff/axiom+of+separation/24">diff</a>, <a href="https://ncatlab.org/nlab/revision/axiom+of+separation/24">v24</a>, <a href="https://ncatlab.org/nlab/show/axiom+of+separation">current</a>

Added a reference to Clemens Berger and Ralph M. Kaufmann’s Comprehensive Factorization Systems.

diff, v24, current

1 to 33 of 33

nForum

Discussion Feed

Not signed in

Site Tag Cloud

nLab > Latest Changes: axiom of separation