Commits · master · Håkon Gylterud / hott-set-theory · GitLab

Snippets Groups Projects

Jun 21, 2021
- Add a straight forward definition of (homotopic) M-types. · 81b93e98
  Håkon Gylterud authored 3 years ago
  
  81b93e98
Sep 29, 2020
- Delete the empty filed called ":". · 7a6bdc42
  Håkon Gylterud authored 4 years ago
  
  7a6bdc42
Sep 22, 2020
- Fix typo in natural-numbers · a9fcef2a
  Elisabeth.Stenholm authored 4 years ago
  
  a9fcef2a
- Prove model has natural numbers · 81bbe935
  Elisabeth.Stenholm authored 4 years ago
  
  81bbe935
Sep 03, 2020
- Rearrange and begin on natural numbers · 697343e3
  Elisabeth.Stenholm authored 4 years ago
  
  697343e3
Aug 31, 2020
- Change inj-to-emb in Function/Embeddings.agda · 37ac83a3
  Elisabeth.Stenholm authored 4 years ago
  
  37ac83a3
Aug 28, 2020
- Show extensionality · 4f24352a
  Elisabeth.Stenholm authored 4 years ago
  
  4f24352a
Aug 27, 2020
- Clean up code · b5d86a36
  Elisabeth.Stenholm authored 4 years ago
  
  b5d86a36
- Improve code above exponentiation · 72d33a89
  Elisabeth.Stenholm authored 4 years ago
  
  72d33a89
Aug 26, 2020
- Change all but the last two is-equiv.g sup-equiv back to desup · d4eacd7a
  Elisabeth.Stenholm authored 4 years ago
  
  d4eacd7a
- Change desup to is-equiv.g sup-equiv in exponentiation · 16e3b545
  Elisabeth.Stenholm authored 4 years ago
  
  16e3b545
Aug 22, 2020
- Move all equivalences together · bd7c5a29
  Elisabeth.Stenholm authored 4 years ago
  
  bd7c5a29
Aug 21, 2020
- Show exponentiation · 0261342b
  Elisabeth.Stenholm authored 4 years ago
  
  0261342b
- Add is-total-fun-eqv-7 · 1d04b8b4
  Elisabeth.Stenholm authored 4 years ago
  
  1d04b8b4
- Add is-total-fun-eqv-6 · 7b4af23e
  Elisabeth.Stenholm authored 4 years ago
  
  7b4af23e
- Add is-total-fun-eqv-5 · a36b4c98
  Elisabeth.Stenholm authored 4 years ago
  
  a36b4c98
- Add is-total-fun-eqv-4 · a1a0c21c
  Elisabeth.Stenholm authored 4 years ago
  
  a1a0c21c
- Add exists unique equivalence fun · 1ab8e775
  Elisabeth.Stenholm authored 4 years ago
  
  1ab8e775
- Change is-total-fun-eqv-2-b · 847b4998
  Elisabeth.Stenholm authored 4 years ago
  
  847b4998
- Remove is-contr-eqv · 9eba4d53
  Elisabeth.Stenholm authored 4 years ago
  
  9eba4d53
- Change order in is-total-fun · 4738b9ba
  Elisabeth.Stenholm authored 4 years ago
  
  4738b9ba
Aug 20, 2020
- Add more equivalences to exponentiation · fd37a659
  Elisabeth.Stenholm authored 4 years ago
  
  fd37a659
- Add more equivalences in exponentiation · 07e189c8
  Elisabeth.Stenholm authored 4 years ago
  
  07e189c8
Aug 19, 2020
- Add more equivalences in exponentiation · fe9f09ad
  Elisabeth.Stenholm authored 4 years ago
  
  fe9f09ad
Aug 18, 2020
- Prove part of equivalence in extensionality · 2de19f6a
  Elisabeth.Stenholm authored 4 years ago
  
  2de19f6a
- More wip on extensionality · 90b3beb7
  Elisabeth.Stenholm authored 4 years ago
  
  90b3beb7
- Wip on extensionality · bb848bfb
  Elisabeth.Stenholm authored 4 years ago
  
  bb848bfb
- Construct composition of logical equivalences and eqv to iff · 17b845ce
  Elisabeth.Stenholm authored 4 years ago
  
  17b845ce
Aug 13, 2020
- Show equality in V and equivalence w. index type · e8d3da5b
  Elisabeth.Stenholm authored 4 years ago
  
  e8d3da5b
Aug 12, 2020
- Show left to right implication in exponentiation · f22b3b9e
  Elisabeth.Stenholm authored 4 years ago
  
  f22b3b9e
Aug 10, 2020
- Rewrite fun-set-is-emb · f37719a7
  Elisabeth.Stenholm authored 4 years ago
  
  f37719a7
Aug 07, 2020
- Move relationship btw inj and emb to Embeddings.agda · 4b656b00
  Elisabeth.Stenholm authored 4 years ago
  
  4b656b00
- Show function mapping to graph in V is an embedding · 84b0b1bf
  Elisabeth.Stenholm authored 4 years ago
  
  84b0b1bf
Jul 10, 2020
- Prune imports in Embeddings.agda · bec4e20f
  Elisabeth.Stenholm authored 4 years ago
  
  bec4e20f
- Show extensionality for embeddings · b5780334
  Elisabeth.Stenholm authored 4 years ago
  
  b5780334
- Remove unnecessary lemmas about Σ-types and rearrange in Embeddings.agda · 5d33eb3b
  Elisabeth.Stenholm authored 4 years ago
  
  5d33eb3b
- Clean up and explain hfiber-prop-ap≃ · fc84f1bb
  Elisabeth.Stenholm authored 4 years ago
  
  fc84f1bb
- Construct embedding of a function to the set of ordered pairs in the graph · 5ba6d602
  Elisabeth.Stenholm authored 4 years ago
  
  5ba6d602
Jul 09, 2020
- Finish showing that embeddings preserve h-levels · 509518be
  Elisabeth.Stenholm authored 4 years ago
  
  509518be
Jul 08, 2020
- Begin showing that embeddings preserve h-levels · 8d3054fb
  Elisabeth.Stenholm authored 4 years ago
  
  8d3054fb