Skip to content
Latest commit 7ec73d2 @dlicata335 substructural
..
Failed to load latest commit information.
cubical stuff
loopspace fix termination things
scraps mostly done with KG1
spaces torus paper
AdjointEquiv.agda substructural
BasicTypes.agda
Bool.agda new hit hacks
Char.agda mark postulates so I can see what is left
DecidablePath.agda rename new-without-K back to without-K
FIXME.txt
First.agda stuff
Functions.agda beta reduction
Group.agda new hit hacks
Groupoid.agda
HFiber.agda do some beta reduction
HigherHomotopyAbelian.agda rename new-without-K back to without-K
Int.agda fix termination things
List.agda rename new-without-K back to without-K
LoopSpace.agda rename new-without-K back to without-K
Maybe.agda rename new-without-K back to without-K
Monoid.agda rename new-without-K back to without-K
NConnected.agda first cut at endgame
NType.agda stuff
Nat.agda stuff
Paths.agda first cut at endgame
PointedTypes.agda rename new-without-K back to without-K
Prelude.agda
PrimTrustMe.agda update S1 and Torus to new hit hacks
Prods.agda enc-dec observation
Pushout.agda
PushoutFat.agda mark postulates so I can see what is left
PushoutFatFib.agda more beta reduction
PushoutFib.agda stuff
REquiv.agda need to generalize elim rule
Spectra.agda
Stream.agda stuff
String.agda rename new-without-K back to without-K
Sums.agda rename new-without-K back to without-K
Suspension.agda stuff
TOFIX
Truncations.agda torus paper
Universe.agda rename new-without-K back to without-K
WEq.agda stuff
WrappedPath.agda rename new-without-K back to without-K
loops.txt
Something went wrong with that request. Please try again.