<commit_before>//  Copyright © 2015 <NAME>. All rights reserved.

extension Module {
	public static var propositionalEquality: Module {
		let Identical = Declaration("≡",
			type: nil => { A in A --> A --> .Type },
			value: nil => { A in (A, A) => { x, y in .Type => { Motive in (A --> A --> Motive) --> Motive } } })

		let refl = Declaration("refl",
			type: nil => { A in A => { a in Identical.ref[A, a, a] } },
			value: nil)

		return Module("PropositionalEquality", [ Identical, refl ])
	}
}<commit_msg>Flesh out the definition of `refl`.<commit_after>//  Copyright © 2015 <NAME>. All rights reserved.

extension Module {
	public static var propositionalEquality: Module {
		let Identical = Declaration("≡",
			type: nil => { A in A --> A --> .Type },
			value: nil => { A in (A, A) => { x, y in .Type => { Motive in (A --> A --> Motive) --> Motive } } })

		let refl = Declaration("refl",
			type: nil => { A in A => { a in Identical.ref[A, a, a] } },
			value: nil => { A in A => { a in nil => { Motive in (A --> A --> Motive) => { f in f[a, a] } } } })

		return Module("PropositionalEquality", [ Identical, refl ])
	}
}
{'fraction_non_alphanumeric': 0.1929203539823009, 'fraction_numerical': 0.007079646017699115, 'mean_word_length': 2.7450331125827816, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6260383', 'n_tokens_mistral': 428, 'n_tokens_neox': 388, 'n_words': 140}