Maths - HoTT in Idris

I don't even know if anyone has worked out a model for homotopy type theory so this is not a serous attempt to implement HoTT in Idris. I am just trying to work through a simple example to try to get a feel for what the issues might be.

To get the simplest interesting type, start with a boolean type.
data MyBool = T | F
homotopy invarience There are two ways for terms of this type to be 'equal'. We could match T to T and F to F or T to F and F to T.
So here I have implemented these two 'equalities' as Id1 and Id2:
data Id1 : MyBool -> MyBool -> Type where
   Refl11 : Id1 T T
   Refl12 : Id1 F F
 
 data Id2 : MyBool -> MyBool -> Type where
   Refl21 : Id2 T F
   Refl22 : Id2 F T

These two equalities are not homotopically equivalent to each other because one cannot be continuously deformed into the other.

So we can now think about possible higher order equivalences between the equivalences.
data IdId : a -> b -> Type where
   Refl1' : IdId Id1 Id1
   Refl2' : IdId Id2 Id1
   Refl3' : IdId Id1 Id2
   Refl4' : IdId Id2 Id2

metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.