Xiaohu Wang XiaohuWang0921

XiaohuWang0921 / Circle.ard

Created November 13, 2022 18:21

A proof that the fundamental group of the pointed circle is isomorphic to the integers in cubical type theory, using Arend.

	\import Function
	\import Paths
	\import Arith.Int

	\open Nat (-)
	\open IntRing (negative)

	-- # Raising a loop to an natural power

	-- \| Concatenate a certain loop to itself ``n`` times.

XiaohuWang0921 / RussellsParadox.idr

Created August 4, 2019 13:27

Russell's paradox implemented in Idris, translated from https://gist.github.com/scott-fleischman/8ace399d19b30f0875daa443629d6176

	module RussellsParadox

	data Set : Type where
	MkSet : (a -> Set) -> Set

	elem : Set -> Set -> Type
	elem e (MkSet supp) = Exists (\ x => e = supp x)

	notElem : Set -> Set -> Type
	notElem e s = elem e s -> Void