A set can be considered a 0-category or a sort of degenerate category/groupoid.
Equivalence forms the morphisms and the objects of the set are the members of the set.
A function is a 0-functor between sets.
In pseudocoq
Record function (A B: Set') := {
op: A -> B ;
map {x y}: x == y -> op x == op y
}.
A function is a map between object of the set and a proof the function respects the set's equivalence relation.
But lower categories confuse me.
It seems a functor between propositions is entailment?
But shouldn't this just be a raw function between objects not implication?
And the same should hold for -2-categories as well. A point is a category where all objects are isomorphic. But this is only the added structure of a -2-category to the set of objects.
I think maybe I might just be confused about metatheory vs the internals.
From "inside" you should never be able to see that a proposition has more than one proof.
From "outside" a theorem prover needs to be able to do so or else how will it display results?
I'm still not quite sure how you would prove up to equivalence a functor between points is a point and up to equivalence a functor between propositions is a proposition.
A "raw function" $P \to Q$ is entailment. If you're working in Coq (as it seems you are), this is literally true.
P -> Qis both the type of functions fromPtoQand the type that represents the proposition of "PimpliesQ".In set theory, it's less literal, but it still makes sense if you interpret the proposition $P$ as the set $\{x \in 1 | P\}$, where $1$ is a fixed singleton set (which is a singleton if $P$ is true and empty if $P$ is false). Then $P \Rightarrow Q$ is equivalent to the existence of a function $\{x \in 1 | P\} \to \{x \in 1 | Q\}$.
Not quite: not all categories with all objects isomorphic are $(-2)$-categories. For example, all objects in a group viewed as a one object category are isomorphic (there's only one object!).
To state the definition of (-2)-categories in terms of isomorphisms between objects, you need a couple extra ingredients. First, you need to exclude empty categories. The simplest way to say that is make each object not isomorphic to every other object, but rather isomorphic to one particular object in the category. That ensures that the category at least has that one particular object.
Next, the assignment of an object to its isomorphism to that particular object needs to be "functorial" in some sense. Let $x_0$ be the particular object and $i_x$ the chosen isomorphism $x \cong x_0$. For morphisms $f \colon x \to y$, we need $i_y \circ f = i_x$.
These extra conditions ensure that being a $(-2)$-category is the same as the category being equivalent to the terminal category (one object, one morphism).
It depends a bit on what you mean by "point" and "proposition" here.
If you take "point" to mean the contractible types (the types where
IsContr A := {x0: A & forall x: A, x = x0}is inhabited), then you'll need an additional axiom like functional extensionality to prove this. Using that axiom, it's straightforward to prove that every function between contractible types is equal to the constant function that takes everything to the particular point in the codomain.On the other hand, if you take "point" to mean every element is equivalent to some particular element with respect to some particular equivalence relation, this can be proved without additional axioms. Just take the equivalence relation on the functions to be pointwise equality.
A similar story holds with propositions. You can try "setoid propositions" or use proof-irrelevant types, but if you use proof irrelevant types, you'll need functional extensionality to prove that the type of functions between propositions is itself a proposition.
On the other hand, if you're using Coq's
Propfor propositions, a type being a proposition isn't something you prove. It's either structurally true, or not. In this case, ifPandQare members ofProp, thenP -> Qis also a member ofProp.