IanRay11

Corollary 2.4.4. (use of naturality and whiskering)

9

First I will provide a snippet of the text for easy reference.  The first thing I wish to address is the use of 'naturality' in the first line of...

Lemma 2.1.2. Concatenation of paths

4

In the 'first proof' of this lemma the following is stated >  Here it is said, "We will instead define a function with the equivalent type...". What exactly is...

Equivalence of path induction and based path induction

7

In Section 1.12.2 a proof of the equivalence of path induction and based path induction is provided. I am confused about two things in the latter direction (i.e. path induction...

Czf ind def

8

This is still a work in progress but I would like to share what I have.

Formalizing Christensen's result on small types and connectedness

5

I am starting a draft for the Dan Christensen paper.

I was having a github issue so I am just pushing my current progress

Join of maps is defined. Soon I will investigate the join construction paper and see the extent to which the flattening lemma is required.