Repositories list

• cat

  Public
  Mini Category Theory for F-Algebras

  Coq

  •0•0•0•0•Updated Oct 22, 2017Oct 22, 2017

• hit

  Public
  Three HITs Theorem

  Coq

  •0•0•0•0•Updated Apr 4, 2017Apr 4, 2017

• hit-samples

  Public
  HoTT Examples

  Coq

  •

  MIT License

  •0•0•0•0•Updated Apr 4, 2017Apr 4, 2017

• ftarith

  Public
  Fundamental Theorem of Arithmetic

  Coq

  •0•0•0•0•Updated Mar 30, 2017Mar 30, 2017

• ftc

  Public
  Fundamental Theorem of Calculus

  calculusnewtonleibniz-formula+ 1integral-equations

  Coq

  •0•1•0•0•Updated Mar 29, 2017Mar 29, 2017

• topology

  Public
  Zorn's Lemma and General Topology

  topology

  Coq

  •

  Other

  •1•3•0•0•Updated Mar 29, 2017Mar 29, 2017

• lambda

  Public
  Untyped Lambda Calculus as Initial Object in Cat of Exponential Monads

  monadslambda-calculusexponential

  Coq

  •0•1•0•0•Updated Mar 28, 2017Mar 28, 2017

• termination

  Public
  CoInduction Termination and Category Theory

  streamscategory-theorycoinduction

  Coq

  •0•0•0•0•Updated Mar 28, 2017Mar 28, 2017

• real

  Public
  Real Numbers as CoInductive Streams of Digits

  modelingnumberscoinduction

  Coq

  •

  Other

  •0•2•0•0•Updated Mar 28, 2017Mar 28, 2017

• set

  Public
  Tarski-Grothendieck Set Theory

  set-theoryparadox

  Coq

  •0•1•0•0•Updated Mar 14, 2017Mar 14, 2017

• interpreter

  Public
  Dependent Theory Interpreter

  dependent-typesinterpreterlambda-calculus

  Coq

  •0•0•0•0•Updated Feb 16, 2017Feb 16, 2017