GitHub - Blaisorblade/Agda-playground: My Agda experiments

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 128 Commits
CaiSeminar		CaiSeminar
LogicalRelationsEquivChecking		LogicalRelationsEquivChecking
PolymorphCalculus		PolymorphCalculus
.gitignore		.gitignore
AgdaBasics.agda		AgdaBasics.agda
AgdaPlusZero.agda		AgdaPlusZero.agda
AltArtemov.agda		AltArtemov.agda
BrutalDepTypes.lagda		BrutalDepTypes.lagda
BugReport.agda		BugReport.agda
CyclicFin.agda		CyclicFin.agda
DeltaGroup.agda		DeltaGroup.agda
DeltaGroupoid.agda		DeltaGroupoid.agda
Demo2.agda		Demo2.agda
DependentTypesAtWork-+.agda		DependentTypesAtWork-+.agda
DependentTypesAtWork-Nat.agda		DependentTypesAtWork-Nat.agda
DependentTypesAtWork-eq.agda		DependentTypesAtWork-eq.agda
DependentTypesAtWork-plus1.agda		DependentTypesAtWork-plus1.agda
DependentTypesAtWork-plus2.agda		DependentTypesAtWork-plus2.agda
DependentTypesAtWork.agda		DependentTypesAtWork.agda
Equality.agda		Equality.agda
False.agda		False.agda
ImpredicativePolymorphism.agda		ImpredicativePolymorphism.agda
Kypling.agda		Kypling.agda
LawfulFunctor.agda		LawfulFunctor.agda
LeibnizEquality.agda		LeibnizEquality.agda
ListExamples.agda		ListExamples.agda
MixfixAmbiguity.agda		MixfixAmbiguity.agda
OrnamentalAlgebras.agda		OrnamentalAlgebras.agda
RawArrow.agda		RawArrow.agda
SoundnessOpenTermsXiRule.agda		SoundnessOpenTermsXiRule.agda
TreeDiff.agda		TreeDiff.agda
TypedSelfRepresentation.agda		TypedSelfRepresentation.agda
UnfoldingAbstractDatatypes.agda		UnfoldingAbstractDatatypes.agda
UnfoldingAbstractDatatypes.hs		UnfoldingAbstractDatatypes.hs
UnfoldingAbstractDatatypesFinite.agda		UnfoldingAbstractDatatypesFinite.agda
UnfoldingAbstractDatatypesUtils.agda		UnfoldingAbstractDatatypesUtils.agda
UsingLibrary.agda		UsingLibrary.agda
VectorEqualityExtras.agda		VectorEqualityExtras.agda
WhyDependentTypesMatter.agda		WhyDependentTypesMatter.agda