This is the third post in the Cartesian frames sequence. Read the first post here.

This post will introduce the standard equivalence relations we'll be using for Cartesian frames. Our primary interest will be in homotopy equivalence, which will allow us to classify frames according to their agents' and environments' effect on possible worlds.

 

1. Isomorphism

Before defining homotopy equivalence, I want to define isomorphism between Cartesian frames.

Definition: A morphism  is an isomorphism if both  and  are bijective. If there is an isomorphism between  and , we say .

Claim:  is an equivalence relation.

Proof: Reflexivity is trivial because the identity is an isomorphism. For symmetry, we have that if  is an isomorphism from  to , then  is an isomorphism from  to . Transitivity follows from the fact that bijection is transitive. 

Claim:  if and only if there is a pair of morphisms  and  that compose to the identity morphism in both orders.

Proof: If , we have  with both  and  bijective, and we can take  and .

Conversely, if  is the identity morphism on , then  is the identity on , so  must be injective. Similarly,  is the identity on , so  must be surjective. Surjectivity of  and injectivity of  follow similarly from the fact that  is the identity on 

Isomorphism is pretty intuitive. It is basically saying that it doesn't matter what the possible agents and possible environments are, other than how they interact with the evaluation function.

We will basically always be working up to at least isomorphism. For example, in the last post ("Additive Operations on Cartesian Frames"), we noted that  and  are commutative and associative up to isomorphism.

 

2. Homotopy Equivalence

2.1. Homotopic Morphisms

Our initial definition of homotopy equivalence will be devoid of interpretation, but the meaning will become clear later.

We say that two morphisms from  to  are homotopic if you can take the first function from the first morphism and the second function from the second morphism, and the resulting object is still a morphism.

Definition: Two morphisms