https://github.com/dlicata335/hott-agda
Tip revision: dccc6507ccd337103e738a113831422f18dd64eb authored by emblack on 07 September 2017, 12:30:12 UTC
updated thesis source file
updated thesis source file
Tip revision: dccc650
| File | Mode | Size |
|---|---|---|
| cubical | ||
| loopspace | ||
| scraps | ||
| spaces | ||
| AdjointEquiv.agda | -rw-r--r-- | 11.4 KB |
| BasicTypes.agda | -rw-r--r-- | 1.1 KB |
| Bool.agda | -rw-r--r-- | 6.2 KB |
| Char.agda | -rw-r--r-- | 992 bytes |
| DecidablePath.agda | -rw-r--r-- | 3.6 KB |
| FIXME.txt | -rw-r--r-- | 23 bytes |
| First.agda | -rw-r--r-- | 15.9 KB |
| Functions.agda | -rw-r--r-- | 12.9 KB |
| Group.agda | -rw-r--r-- | 1.5 KB |
| Groupoid.agda | -rw-r--r-- | 1.4 KB |
| HFiber.agda | -rw-r--r-- | 10.3 KB |
| HigherHomotopyAbelian.agda | -rw-r--r-- | 6.1 KB |
| Int.agda | -rw-r--r-- | 9.9 KB |
| List.agda | -rw-r--r-- | 8.3 KB |
| LoopSpace.agda | -rw-r--r-- | 657 bytes |
| Maybe.agda | -rw-r--r-- | 1.2 KB |
| Monoid.agda | -rw-r--r-- | 6.7 KB |
| NConnected.agda | -rw-r--r-- | 41.7 KB |
| NType.agda | -rw-r--r-- | 6.3 KB |
| Nat.agda | -rw-r--r-- | 1.1 KB |
| Paths.agda | -rw-r--r-- | 21.8 KB |
| PointedTypes.agda | -rw-r--r-- | 3.3 KB |
| Prelude.agda | -rw-r--r-- | 102 bytes |
| PrimTrustMe.agda | -rw-r--r-- | 906 bytes |
| Prods.agda | -rw-r--r-- | 17.5 KB |
| Pushout.agda | -rw-r--r-- | 8.2 KB |
| PushoutFat.agda | -rw-r--r-- | 6.3 KB |
| PushoutFatFib.agda | -rw-r--r-- | 4.0 KB |
| PushoutFib.agda | -rw-r--r-- | 2.7 KB |
| REquiv.agda | -rw-r--r-- | 3.2 KB |
| Spectra.agda | -rw-r--r-- | 2.3 KB |
| Stream.agda | -rw-r--r-- | 5.5 KB |
| String.agda | -rw-r--r-- | 701 bytes |
| Sums.agda | -rw-r--r-- | 3.8 KB |
| Suspension.agda | -rw-r--r-- | 4.8 KB |
| TOFIX | -rw-r--r-- | 775 bytes |
| Truncations.agda | -rw-r--r-- | 14.6 KB |
| Universe.agda | -rw-r--r-- | 4.9 KB |
| WEq.agda | -rw-r--r-- | 3.4 KB |
| WrappedPath.agda | -rw-r--r-- | 5.5 KB |
| loops.txt | -rw-r--r-- | 3.2 KB |
