martinescardo/TypeTopology

Issues

• Update the Agda action to 2.7.0

  #308 opened 3 months ago by ayberkt
  1

• Give a native coinductive definition of ℕ∞

  #309 opened 5 months ago by martinescardo
  0

• Add alternative definition of the notion of distributive lattice isomorphism

  #269 opened 6 months ago by ayberkt
  0

• update line and file count

  #290 opened 7 months ago by martinescardo
  1

• Should order-theoretic notions be separated out from the Dcpo module?

  #42 opened 7 months ago by ayberkt
  15

• Add a proof of Zorn’s Lemma

  #178 opened 7 months ago by ayberkt
  1

• Define the sublocale of a locale

  #183 opened a year ago by ayberkt
  0

• Prove that every spectral frame is isomorphic to the frame of ideals of its lattice of compact opens

  #268 opened 8 months ago by ayberkt
  0

• Define the Lawson topology of a dcpo

  #219 opened a year ago by ayberkt
  1

• Remove completed TODO on the topology of Scott domains

  #263 opened 9 months ago by ayberkt
  3

• Avoid the use of function extensionality in `InternalModCont.lagda`

  #174 opened 10 months ago by ayberkt
  1

• Clarify the terminology of “cofinal”

  #213 opened a year ago by ayberkt
  3

• Prove equivalence to alternative notion of uniform continuity

  #211 opened a year ago by ayberkt
  0

• Prove correctness of the internal modulus of uniform continuity operation

  #212 opened a year ago by ayberkt
  0

• Add an alternative definition of Kuratowski-finiteness using `listed`

  #223 opened a year ago by ayberkt
  0

• A to-do from the `LiftingSetAlgebraic` module

  #222 opened a year ago by ayberkt
  0

• Add comments to the locale theory development

  #190 opened a year ago by ayberkt
  0

• Propositional truncation causes some types to not be strictly positive

  #216 opened a year ago by 9Y0
  2

• Port PathSeq from HoTT-Agda to TypeTopology

  #107 opened a year ago by ettorealdrovandi
  4

• Add proof that the type of small compact bases for large and locally small dcpos has split support

  #189 opened a year ago by ayberkt
  1

• Generalise the powerset module

  #196 opened a year ago by ayberkt
  1

• Add comments to `index.lagda`

  #191 opened a year ago by ayberkt
  0

• Decouple the small basis condition from the definition of spectrality

  #168 opened a year ago by ayberkt
  1

• Define the Hydra game and implement a proof of its termination

  #159 opened a year ago by ayberkt
  2

• Decouple the small basis condition from the definitions of regularity and zero-dimensionality

  #169 opened a year ago by ayberkt
  0

• Use `꞉` (MODIFIER LETTER COLON) instead of `:` (RATIO) in `UF-Subsingleton-Combinators`

  #76 opened 2 years ago by ayberkt
  2

• Refactor `InitialFrame` to avoid using full univalence

  #69 opened 2 years ago by ayberkt
  4

• Modulus of continuity is off by 1

  #129 opened 2 years ago by martinescardo
  1

• Proper compilation to HTML

  #86 opened 3 years ago by ayberkt
  0

• Weird message in typechecking workflow logs

  #56 opened 3 years ago by ayberkt
  1

• Update the typechecking workflow to Agda 2.6.2

  #57 opened 3 years ago by ayberkt
  6

• ∀[ i ∶ I ] e should be ∀ i ∶ I , e

  #53 opened 3 years ago by martinescardo
  4

• Unify two developments of frames (`frame.lagda` and `Frame.lagda`)

  #49 opened 3 years ago by ayberkt
  4

• Typechecking workflow fails for no apparent reason

  #54 opened 4 years ago by ayberkt
  5

• Define combinators for Ω

  #43 opened 4 years ago by ayberkt
  2

• Add CI/CD workflow for typechecking the code

  #45 opened 4 years ago by ayberkt
  1

• Expressing decidability in terms of semidecidability

  #28 opened 5 years ago by ayberkt
  2