random agda experiments
root
- categorica
- cubical
- halting
- hoas
- induction
- injective
- logic
- lrs
- nbe
- sorting
- universes
- why-not-w
- .boring
- AVL.agda
- AckInd0.agda
- BijectiveIso.agda
- Bindings.agda
- CExp.agda
- CI.agda
- ChurchLaw.agda
- Coexp.agda
- Conat.agda
- ContAdj.agda
- Coprod.agda
- Countable.agda
- DC.agda
- DecEq.agda
- DepCat.agda
- DiaFun.agda
- Diag.agda
- Distinct.agda
- EckmannHilton.agda
- ExistentialCoinduction.agda
- F.agda
- Fib.agda
- FibredImpredicative.agda
- FinLT.agda
- FinalAlgebra.agda
- Float.agda
- Foundation.agda
- Free.agda
- FunView.agda
- HEqExt.agda
- Horse.agda
- IOE.agda
- IRDomain.agda
- IRHurkens.agda
- IRSetTheory.agda
- IndexedMonad.agda
- Infinitary.agda
- Infinite.agda
- InfiniteDescent.agda
- InjTCSplit.agda
- Interp.agda
- K.agda
- Kripke.agda
- LICENCE
- Lenses.agda
- MFin.agda
- MuNu.agda
- Negative.agda
- Nest.agda
- NestPoly.agda
- Newtype.agda
- Ordinal.agda
- PHOASNorm.agda
- PW.agda
- ParamFunc.agda
- ParamInduction.agda
- ParamProj.agda
- ParametricTerminal.agda
- Pent.agda
- Pigeon.agda
- Prime.agda
- PropRewrite.agda
- PushoutQuotients.agda
- QuickSort.agda
- Rat.agda
- Refinement.agda
- Regular.agda
- Russell.agda
- SKI.agda
- SetoidFacts.agda
- SetoidPushout.agda
- StateAlgebra.agda
- TrivMLTT.agda
- Two.agda
- WISC.agda
- WeirdSetoid.agda
- WhyNotW.agda
- ZigZag.agda
- Zip.agda
- agda-share.agda-lib