amelia
/
cubical


-- We begin by adding some primitive bindings using the PRIMITIVE pragma.

--

-- It goes like this: PRIMITIVE primName varName.

--

-- If the varName is dropped, then it's taken to be the same as primName.

--

-- If there is a previous declaration for the varName, then the type

-- is checked against the internally-known "proper" type for the primitive.


-- Universe of fibrant types

{-# PRIMITIVE Type #-}


-- Universe of non-fibrant types

{-# PRIMITIVE Pretype #-}


-- Fibrant is a fancy word for "has a composition structure". Most types

-- we inherit from MLTT are fibrant:

--

-- Stuff like products Π, sums Σ, naturals, booleans, lists, etc., all

-- have composition structures.

--

-- The non-fibrant types are part of the structure of cubical

-- categories: The interval, partial elements, cubical subtypes, ...


-- The interval

---------------


-- The interval has two endpoints i0 and i1.

-- These form a de Morgan algebra.

I : Pretype

{-# PRIMITIVE Interval I #-}


i0, i1 : I

{-# PRIMITIVE i0 #-}

{-# PRIMITIVE i1 #-}


-- "minimum" on the interval

iand : I -> I -> I

{-# PRIMITIVE iand #-}


-- "maximum" on the interval.

ior : I -> I -> I

{-# PRIMITIVE ior #-}


-- The interpretation of iand as min and ior as max justifies the fact that

-- ior i (inot i) != i1, since that equality only holds for the endpoints.


-- inot i = 1 - i is a de Morgan involution.

inot : I -> I

{-# PRIMITIVE inot #-}


-- Paths

--------


-- Since every function in type theory is internally continuous,

-- and the two endpoints i0 and i1 are equal, we can take the type of

-- equalities to be continuous functions out of the interval.

-- That is, x ≡ y iff. ∃ f : I -> A, f i0 = x, f i1 = y.


-- The type PathP generalises this to dependent products (i : I) -> A i.


PathP : (A : I -> Type) -> A i0 -> A i1 -> Type

{-# PRIMITIVE PathP #-}


-- By taking the first argument to be constant we get the equality type

-- Path.


Path : {A : Type} -> A -> A -> Type

Path {A} = PathP (\i -> A)


-- reflexivity is given by constant paths


refl : {A : Type} {x : A} -> Path x x

refl {A} {x} i = x


-- Symmetry (for dpeendent paths) is given by inverting the argument to the path, such that

-- sym p i0 = p (inot i0) = p i1

-- sym p i1 = p (inot i1) = p i0

-- This has the correct endpoints.


sym : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x

sym p i = p (inot i)


id : {A : Type} -> A -> A

id x = x


the : (A : Type) -> A -> A

the A x = x


-- The eliminator for the interval says that if you have x : A i0 and y : A i1,

-- and x ≡ y, then you can get a proof A i for every element of the interval.

iElim : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i

iElim p i = p i


-- This corresponds to the elimination principle for the HIT

-- data I : Pretype where

-- i0 i1 : I

-- seg : i0 ≡ i1


-- The singleton subtype of A at x is the type of elements of y which

-- are equal to x.

Singl : (A : Type) -> A -> Type

Singl A x = (y : A) * Path x y


-- Contractible types are those for which there exists an element to which

-- all others are equal.

isContr : Type -> Type

isContr A = (x : A) * ((y : A) -> Path x y)


-- Using the connection \i j -> y.2 (iand i j), we can prove that

-- singletons are contracible. Together with transport later on,

-- we get the J elimination principle of paths.

singContr : {A : Type} {a : A} -> isContr (Singl A a)

singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))


-- Some more operations on paths. By rearranging parentheses we get a

-- proof that the images of equal elements are themselves equal.

cong : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)

cong f p i = f (p i)


-- These satisfy definitional equalities, like congComp and congId, which are

-- propositional in vanilla MLTT.

congComp : {A : Type} {B : Type} {C : Type}

 {f : A -> B} {g : B -> C} {x : A} {y : A}

 (p : Path x y)

 -> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)

congComp p = refl


congId : {A : Type} {x : A} {y : A}

 (p : Path x y)

 -> Path (cong (id {A}) p) p

congId p = refl


-- Just like rearranging parentheses gives us cong, swapping the value

-- and interval binders gives us function extensionality.

funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}

 (h : (x : A) -> Path (f x) (g x))

 -> Path f g

funext h i x = h x i


happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}

 -> (p : Path f g) -> (x : A) -> Path (f x) (g x)

happly p x i = p i x


-- The proposition associated with an element of the interval

-------------------------------------------------------------


-- Associated with every element i : I of the interval, we have the type

-- IsOne i which is inhabited only when i = i1. In the model, this

-- corresponds to the map [φ] from the interval cubical set to the

-- subobject classifier.


IsOne : I -> Pretype

{-# PRIMITIVE IsOne #-}


-- The value itIs1 witnesses the fact that i1 = i1.

itIs1 : IsOne i1


-- Furthermore, if either of i or j are one, then so is (i or j).

isOneL : {i : I} {j : I} -> IsOne i -> IsOne (ior i j)

isOneR : {i : I} {j : I} -> IsOne j -> IsOne (ior i j)


{-# PRIMITIVE itIs1 #-}

{-# PRIMITIVE isOneL #-}

{-# PRIMITIVE isOneR #-}


-- Partial elements

-------------------

--

-- Since a function I -> A has two endpoints, and a function I -> I -> A

-- has four endpoints + four functions I -> A as "sides" (obtained by

-- varying argument while holding the other as a bound variable), we

-- refer to elements of I^n -> A as "cubes".


-- This justifies the existence of partial elements, which are, as the

-- name implies, partial cubes. Namely, a Partial φ A is an element of A

-- which depends on a proof that IsOne φ.


Partial : I -> Type -> Pretype

{-# PRIMITIVE Partial #-}


-- There is also a dependent version where the type A is itself a

-- partial element.


PartialP : (phi : I) -> Partial phi Type -> Pretype

{-# PRIMITIVE PartialP #-}


-- Why is Partial φ A not just defined as φ -> A? The difference is that

-- Partial φ A has an internal representation which definitionally relates

-- any two partial elements which "agree everywhere", that is, have

-- equivalent values for every possible assignment of variables which

-- makes IsOne φ hold.


-- Cubical Subtypes

--------------------


-- Given A : Type, phi : I, and a partial element u : A defined on φ,

-- we have the type Sub A phi u, notated A[phi -> u] in the output of

-- the type checker, whose elements are "extensions" of u.


-- That is, element of A[phi -> u] is an element of A defined everywhere

-- (a total element), which, when IsOne φ, agrees with u.


Sub : (A : Type) (phi : I) -> Partial phi A -> Pretype

{-# PRIMITIVE Sub #-}


-- Every total element u : A can be made partial on φ by ignoring the

-- constraint. Furthermore, this "totally partial" element agrees with

-- the original total element on φ.

inS : {A : Type} {phi : I} (u : A) -> Sub A phi (\x -> u)

{-# PRIMITIVE inS #-}


-- When IsOne φ, outS {A} {φ} {u} x reduces to u itIs1.

-- This implements the fact that x agrees with u on φ.

outS : {A : Type} {phi : I} {u : Partial phi A} -> Sub A phi u -> A

{-# PRIMITIVE outS #-}


-- The composition operation

----------------------------


-- Now that we have syntax for specifying partial cubes,

-- and specifying that an element agrees with a partial cube,

-- we can describe the composition operation.


comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1

{-# PRIMITIVE comp #-}


-- In particular, when φ is a disjunction of the form

-- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a

-- "tube", an open square with no floor or roof:

--

-- Given u = \j [ (i = i0) -> x, (i = i1) -> q j] on the extent i || ~i,

-- we draw:

--

-- x q i1

-- | |

-- \j -> x | | \j -> q j

-- | |

-- x q i0

--

-- The composition operation says that, as long as we can provide a

-- "floor" connecting x -- q i0, as a total element of A which, on

-- phi, extends u i0, then we get the "roof" connecting x and q i1

-- for free.

--

-- If we have a path p : x ≡ y, and q : y ≡ z, then we do get the

-- "floor", and composition gets us the dotted line:

--

-- x..........z

-- | |

-- x | | q j

-- | |

-- x----------y

-- p i


trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z

trans {A} {x} p q i =

 comp (\i -> A)

 {ior i (inot i)}

 (\j [ (i = i0) -> x, (i = i1) -> q j ])

 (inS (p i))


-- In particular when the formula φ = i0 we get the "opposite face" to a

-- single point, which corresponds to transport.


transp : (A : I -> Type) (x : A i0) -> A i1

transp A x = comp A (\i [ ]) (inS x)


-- Since we have the iand operator, we can also derive the *filler* of a cube,

-- which connects the given face and the output of composition.


fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> (i : I) -> A i

fill A {phi} u a0 i =

 comp (\j -> A (iand i j))

 {ior phi (inot i)}

 (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])

 (inS (outS a0))


hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> I -> A

hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i


hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A

hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0


-- For instance, the filler of the previous composition square

-- tells us that trans p refl = p:


transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p

transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)


-- Reduction of composition

---------------------------

--

-- Composition reduces on the structure of the family A : I -> Type to create

-- the element a1 : (A i1)[phi -> u i1].

--

-- For instance, when filling a cube of functions, the behaviour is to

-- first transport backwards along the domain, apply the function, then

-- forwards along the codomain.


transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path C D)

 -> (f : A -> C) -> Path (transp (\i -> p i -> q i) f)

 (\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x)))

transpFun p q f = refl


-- When considering the more general case of a composition respecing sides,

-- the outer transport becomes a composition.


-- Glueing and Univalence

-------------------------


-- First, let's get some definitions out of the way.

--

-- The *fiber* of a function f : A -> B at a point y : B is the type of

-- inputs x : A which f takes to y, that is, for which there exists a

-- path f(x) = y.


fiber : {A : Type} {B : Type} -> (A -> B) -> B -> Type

fiber f y = (x : A) * Path (f x) y


-- An *equivalence* is a function where every fiber is contractible.

-- That is, for every point in the codomain y : B, there is exactly one

-- point in the input which f maps to y.


isEquiv : {A : Type} {B : Type} -> (A -> B) -> Type

isEquiv {A} {B} f = (y : B) -> isContr (fiber f y)


-- By extracting this point, which must exist because the fiber is contractible,

-- we can get an inverse of f:


inverse : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A

inverse eqv y = (eqv y) .1 .1


-- We can prove that «inverse eqv» is a section of f:


section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id

section f eqv i y = (eqv y) .1 .2 i


-- Proving that it's also a retraction is left as an exercise to the

-- reader. We can package together a function and a proof that it's an

-- equivalence to get a capital-E Equivalence.


Equiv : (A : Type) (B : Type) -> Type

Equiv A B = (f : A -> B) * isEquiv f


-- The identity function is an equivalence between any type A and

-- itself.

idEquiv : {A : Type} -> isEquiv (id {A})

idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j)))


-- The glue operation expresses that "extensibility is invariant under

-- equivalence". Less concisely, the Glue type and its constructor,

-- glue, let us extend a partial element of a partial type to a total

-- element of a total type, by "gluing" the partial type T using a

-- partial equivalence e onto a total type A.


-- In particular, we have that when φ = i1, Glue A [i1 -> (T, f)] = T.


primGlue : (A : Type) {phi : I}

 (T : Partial phi Type)

 (e : PartialP phi (\o -> Equiv (T o) A))

 -> Type

{-# PRIMITIVE Glue primGlue #-}


-- The glue constructor extends the partial element t : T to a total

-- element of Glue A [φ -> (T, e)] as long as we have a total im : A

-- which is the image of f(t).

--

-- Agreeing with the condition that Glue A [i1 -> (T, e)] = T,

-- we have that glue {A} {i1} t im => t.

prim'glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}

 -> (t : PartialP phi T)

 -> (im : Sub A phi (\o -> (e o).1 (t o)))

 -> primGlue A T e


{-# PRIMITIVE glue prim'glue #-}


-- The unglue operation undoes a glueing. Since when φ = i1,

-- Glue A [φ -> (T, f)] = T, the argument to primUnglue {A} {i1} ...

-- will have type T, and so to get back an A we need to apply the

-- partial equivalence f (defined everywhere).


primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}

 -> primGlue A {phi} T e -> A


{-# PRIMITIVE unglue primUnglue #-}


-- Diagramatically, i : I |- Glue A [(i \/ ~i) -> (T, e)] can be drawn

-- as giving us the dotted line in:

--

-- T i0 ......... T i1

-- | |

-- | |

-- e i0 |~ ~| e i1

-- | |

-- | |

-- A i0 --------- A i1

-- A

--

-- Where the the two "e" sides are equivalences, and the bottom side is

-- the line i : I |- A.

--

-- Thus, by choosing a base type, a set of partial types and partial

-- equivalences, we can make a line between two types (T i0) and (T i1).


Glue : (A : Type) {phi : I} -> Partial phi ((X : Type) * Equiv X A) -> Type

Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)


-- For example, we can glue together the type A and the type B as long

-- as there exists an Equiv A B.

--

-- A ............ B

-- | |

-- | |

-- equiv |~ ua equiv ~| idEquiv {B}

-- | |

-- | |

-- B ------------ B

-- \i → B

--

univalence : {A : Type} {B : Type} -> Equiv A B -> Path A B

univalence {A} {B} equiv i =

 Glue B (\[ (i = i0) -> (A, equiv),

 (i = i1) -> (B, the B, idEquiv {B}) ])


-- The fact that this diagram has 2 filled-in B sides explains the

-- complication in the proof below.

--

-- In particular, the actual behaviour of transp (\i -> univalence f i)

-- (x : A) is not just to apply f x to get a B (the left side), it also

-- needs to:

--

-- * For the bottom side, compose along (\i -> B) (the bottom side)

-- * For the right side, apply the inverse of the identity, which

-- is just identity, to get *some* b : B

--

-- But that b : B might not agree with the sides of the composition

-- operation in a more general case, so it composes along (\i -> B)

-- *again*!

--

-- Thus the proof: a simple cubical argument suffices, since

-- for any composition, its filler connects either endpoints. So

-- we need to come up with a filler for the bottom and right faces.


univalenceBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1

univalenceBeta {A} {B} f i a =

 let

 -- The bottom left corner

 botLeft : B

 botLeft = transp (\i -> B) (f.1 a)


 -- The "bottom face" filler connects the bottom-left corner, f.1 a,

 -- and the bottom-right corner, which is the transport of f.1 a

 -- along \i -> B.

 botFace : Path (f.1 a) botLeft

 botFace i = fill (\i -> B) (\j []) (inS (f.1 a)) i


 -- The "right face" filler connects the bottom-right corner and the

 -- upper-right corner, which is again a simple transport along

 -- \i -> B.

 rightFace : Path (transp (\i -> B) botLeft) botLeft

 rightFace i = fill (\i -> B) (\j []) (inS botLeft) (inot i)


 -- The goal is a path between the bottom-left and top-right corners,

 -- which we can get by composing (in the path sense) the bottom and

 -- right faces.

 goal : Path (transp (\i -> B) botLeft) (f.1 a)

 goal = trans rightFace (\i -> botFace (inot i))

 in goal i


-- The terms univalence + univalenceBeta suffice to prove the "full"

-- univalence axiom of Voevodsky, as can be seen in the paper

--

-- Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom.

--

-- Available freely here: https://arxiv.org/abs/1712.04890v3


J : {A : Type} {x : A}

 (P : (y : A) -> Path x y -> Type)

 (d : P x (\i -> x))

 {y : A} (p : Path x y)

 -> P y p

J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d


-- Isomorphisms

---------------

--

-- Since isomorphisms are a much more convenient notion of equivalence

-- than contractible fibers, it's natural to ask why the CCHM paper, and

-- this implementation following that, decided on the latter for our

-- definition of equivalence.


isIso : {A : Type} -> {B : Type} -> (A -> B) -> Type

isIso {A} {B} f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x)


-- The reason is that the family of types IsIso is not a proposition!

-- This means that there can be more than one way for a function to be

-- an equivalence. This is Lemma 4.1.1 of the HoTT book.


Iso : Type -> Type -> Type

Iso A B = (f : A -> B) * isIso f


-- Nevertheless, we can prove that any function with an isomorphism

-- structure has contractible fibers, using a cubical argument adapted

-- from CCHM's implementation of cubical type theory:

--

-- https://github.com/mortberg/cubicaltt/blob/master/experiments/isoToEquiv.ctt#L7-L55


IsoToEquiv : {A : Type} {B : Type} -> Iso A B -> Equiv A B

IsoToEquiv {A} {B} iso =

 let

 f = iso.1

 g = iso.2.1

 s = iso.2.2.1

 t = iso.2.2.2


 lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path (f x0) y) (p1 : Path (f x1) y)

 -> PathP (\i -> fiber f y) (x0, p0) (x1, p1)

 lemIso y x0 x1 p0 p1 =

 let

 rem0 : Path x0 (g y)

 rem0 i = hcomp {A} (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i)))


 rem1 : Path x1 (g y)

 rem1 i = hcomp {A} (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i)))


 p : Path x0 x1

 p i = hcomp {A} (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))


 fill0 : I -> I -> A

 fill0 i j = hcomp {A} (\k [ (i = i0) -> t x0 (iand j k)

 , (i = i1) -> g y

 , (j = i0) -> g (p0 i)

 ])

 (inS (g (p0 i)))


 fill1 : I -> I -> A

 fill1 i j = hcomp {A} (\k [ (i = i0) -> t x1 (iand j k)

 , (i = i1) -> g y

 , (j = i0) -> g (p1 i) ])

 (inS (g (p1 i)))


 fill2 : I -> I -> A

 fill2 i j = hcomp {A} (\k [ (i = i0) -> rem0 (ior j (inot k))

 , (i = i1) -> rem1 (ior j (inot k))

 , (j = i1) -> g y ])

 (inS (g y))


 sq : I -> I -> A

 sq i j = hcomp {A} (\k [ (i = i0) -> fill0 j (inot k)

 , (i = i1) -> fill1 j (inot k)

 , (j = i1) -> g y

 , (j = i0) -> t (p i) (inot k) ])

 (inS (fill2 i j))


 sq1 : I -> I -> B

 sq1 i j = hcomp {B} (\k [ (i = i0) -> s (p0 j) k

 , (i = i1) -> s (p1 j) k

 , (j = i0) -> s (f (p i)) k

 , (j = i1) -> s y k

 ])

 (inS (f (sq i j)))

 in \i -> (p i, \j -> sq1 i j)


 fCenter : (y : B) -> fiber f y

 fCenter y = (g y, s y)


 fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w

 fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2

 in (f, \y -> (fCenter y, fIsCenter y))


-- We can prove that any involutive function is an isomorphism, since

-- such a function is its own inverse.


involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f

involToIso {A} f inv = (f, inv, inv)


-- An example of univalence

---------------------------

--

-- The classic example of univalence is the equivalence

-- not : Bool \simeq Bool.

--

-- We define it here.


Bool : Type

{-# PRIMITIVE Bool #-}


true, false : Bool

{-# PRIMITIVE true #-}

{-# PRIMITIVE false #-}


-- Pattern matching for booleans: If a proposition holds for true and

-- for false, then it holds for every bool.

elimBool : (P : Bool -> Type) -> P true -> P false -> (b : Bool) -> P b

{-# PRIMITIVE if elimBool #-}


-- Non-dependent elimination of booleans

if : {A : Type} -> A -> A -> Bool -> A

if {A} = elimBool (\b -> A)


not : Bool -> Bool

not = if false true


-- By pattern matching it suffices to prove (not (not true)) ≡ true and

-- not (not false) ≡ false. Since not (not true) computes to true (resp.

-- false), both proofs go through by refl.

notInvol : (x : Bool) -> Path (not (not x)) x

notInvol = elimBool (\b -> Path (not (not b)) b) refl refl


notp : Path Bool Bool

notp = univalence (IsoToEquiv (not, involToIso not notInvol))


-- This path actually serves to prove a simple lemma about the universes

-- of HoTT, namely, that any univalent universe is not a 0-type. If we

-- had HITs, we could prove that this fact holds for any n, but for now,

-- proving it's not an h-set is the furthest we can go.


-- First we define what it means for something to be false. In type theory,

-- we take ¬P = P → ⊥, where the bottom type is the only type satisfying

-- the elimination principle

--

-- elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b

--

-- This follows from setting bottom := ∀ A, A.


bottom : Type

bottom = {A : Type} -> A


elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b

elimBottom P x = x


-- We prove that true != false by transporting along the path

--

-- \i -> if (Bool -> Bool) A (p i)

-- (Bool -> Bool) ------------------------------------ A

--

-- To verify that this has the correct endpoints, check out the endpoints

-- for p:

--

-- true ------------------------------------ false

--

-- and evaluate the if at either end.


trueNotFalse : Path true false -> bottom

trueNotFalse p {A} = transp (\i -> if (Bool -> Bool) A (p i)) id


-- To be an h-Set is to have no "higher path information". Alternatively,

--

-- isHSet A = (x : A) (y : A) -> isHProp (Path x y)

--

isHSet : Type -> Type

isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q


-- We can prove *a* contradiction (note: this is a direct proof!) by adversarially

-- choosing two paths p, q that we know are not equal. Since "equal" paths have

-- equal behaviour when transporting, we can choose two paths p, q and a point x

-- such that transporting x along p gives a different result from x along q.

--

-- Since transp notp = not but transp refl = id, that's what we go with. The choice

-- of false as the point x is just from the endpoints of trueNotFalse.


universeNotSet : isHSet Type -> bottom

universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false)