|
|
|
@ -399,7 +399,7 @@ primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o - |
|
|
|
-- A i0 --------- A i1 |
|
|
|
-- A |
|
|
|
-- |
|
|
|
-- Where the the two "e" sides are equivalences, and the bottom side is |
|
|
|
-- 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 |
|
|
|
@ -433,7 +433,7 @@ univalence {A} {B} equiv 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 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 |
|
|
|
-- |
|
|
|
@ -443,29 +443,29 @@ univalence {A} {B} equiv i = |
|
|
|
-- |
|
|
|
-- 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. |
|
|
|
-- 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 |
|
|
|
-- 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 |
|
|
|
-- 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 |
|
|
|
-- 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 |
|
|
|
-- 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)) |
|
|
|
@ -619,19 +619,19 @@ notp = univalence (IsoToEquiv (not, involToIso not notInvol)) |
|
|
|
-- 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 |
|
|
|
-- we take ¬P = P → ⊥, where the Bottom type is the only type satisfying |
|
|
|
-- the elimination principle |
|
|
|
-- |
|
|
|
-- elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b |
|
|
|
-- elimBottom : (P : Bottom -> Type) -> (b : Bottom) -> P b |
|
|
|
-- |
|
|
|
-- This follows from setting bottom := ∀ A, A. |
|
|
|
-- This follows from setting Bottom := ∀ A, A. |
|
|
|
|
|
|
|
data bottom : Type where {} |
|
|
|
data Bottom : Type where {} |
|
|
|
|
|
|
|
elimBottom : (P : bottom -> Pretype) -> (b : bottom) -> P b |
|
|
|
elimBottom : (P : Bottom -> Pretype) -> (b : Bottom) -> P b |
|
|
|
elimBottom P = \case {} |
|
|
|
|
|
|
|
absurd : {P : Pretype} -> bottom -> P |
|
|
|
absurd : {P : Pretype} -> Bottom -> P |
|
|
|
absurd = \case {} |
|
|
|
|
|
|
|
-- We prove that true != false by transporting along the path |
|
|
|
@ -646,8 +646,8 @@ absurd = \case {} |
|
|
|
-- |
|
|
|
-- and evaluate the if at either end. |
|
|
|
|
|
|
|
trueNotFalse : Path true false -> bottom |
|
|
|
trueNotFalse p = transp (\i -> if (Bool -> Bool) bottom (p i)) id |
|
|
|
trueNotFalse : Path true false -> Bottom |
|
|
|
trueNotFalse p = transp (\i -> if (Bool -> Bool) Bottom (p i)) id |
|
|
|
|
|
|
|
-- To be an h-Set is to have no "higher path information". Alternatively, |
|
|
|
-- |
|
|
|
@ -664,7 +664,7 @@ isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p 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 : isHSet Type -> Bottom |
|
|
|
universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false) |
|
|
|
|
|
|
|
-- Funext is an inverse of happly |
|
|
|
@ -715,12 +715,12 @@ Nat_elim P pz ps = \case |
|
|
|
zero -> pz |
|
|
|
succ x -> ps x (Nat_elim P pz ps x) |
|
|
|
|
|
|
|
zeroNotSucc : {x : Nat} -> Path zero (succ x) -> bottom |
|
|
|
zeroNotSucc : {x : Nat} -> Path zero (succ x) -> Bottom |
|
|
|
zeroNotSucc p = transp (\i -> fun (p i)) (p i0) where |
|
|
|
fun : Nat -> Type |
|
|
|
fun = \case |
|
|
|
zero -> Nat |
|
|
|
succ x -> bottom |
|
|
|
succ x -> Bottom |
|
|
|
|
|
|
|
succInj : {x : Nat} {y : Nat} -> Path (succ x) (succ y) -> Path x y |
|
|
|
succInj p i = pred (p i) where |
|
|
|
@ -1051,6 +1051,9 @@ sixteen = multInt four four |
|
|
|
isProp : Type -> Type |
|
|
|
isProp A = (x : A) (y : A) -> Path x y |
|
|
|
|
|
|
|
Prop : Type |
|
|
|
Prop = (A : Type) * isProp A |
|
|
|
|
|
|
|
data Sq (A : Type) : Type where |
|
|
|
inc : A -> Sq A |
|
|
|
sq i : (x : Sq A) (y : Sq A) -> Sq A [ (i = i0) -> x, (i = i1) -> y ] |
|
|
|
@ -1065,6 +1068,9 @@ isProp_isSet h {a} {b} p q j i = |
|
|
|
]) |
|
|
|
(inS a) |
|
|
|
|
|
|
|
isProp_isProp : {A : Type} -> isProp (isProp A) |
|
|
|
isProp_isProp f g i a b = isProp_isSet f {a} {b} (f a b) (g a b) i |
|
|
|
|
|
|
|
Sq_rec : {A : Type} {B : Type} |
|
|
|
-> isProp B |
|
|
|
-> (f : A -> B) |
|
|
|
|
