Hypatia du Bois-Marie #RemoveCCP #中共下台 #FormalSciencesForHumanRight #形式科學為人權 analytic-bias

## main.agda

-- This file contains the code from the paper "Formalising
-- type-logical grammars in Agda", and was directly extracted from the
-- paper's source.
--
-- Note: because the symbol customarily used for the "left difference"
-- is unavailable in the Unicode character set, and the backslash used
-- for implication is often a reserved symbol, the source file uses a
-- different notation for the connectives: the left and right
-- implications are represented by the double arrows "⇐" and "⇒", and

	-- This file contains the code from the paper "Formalising
	-- type-logical grammars in Agda", and was directly extracted from the
	-- paper's source.
	--
	-- Note: because the symbol customarily used for the "left difference"
	-- is unavailable in the Unicode character set, and the backslash used
	-- for implication is often a reserved symbol, the source file uses a
	-- different notation for the connectives: the left and right
	-- implications are represented by the double arrows "⇐" and "⇒", and