<commit_before>* The handling of ATP stuff inside where clauses
*** The problems
*** This facilitate the writes of ATP axioms. e.g.
LTC.Examples.GCD.Extra.S≤0-elim : {A : Set}{d : D} → succ d ≤ zero → A

* The difference between predicates' definitions and functions' definitions
From Agda internal representation of clauses, both definitions are
equal, the only difference is in the type of the symbol.

* The problem with eta and the existential
postulate
  D   : Set
  _≡_ : D → D → Set
  P   : (D → Set) → Set
  foo : (x : D) → P (λ y → y ≡ x)
  bar : (x : D) → P (λ y → x ≡ y)

foo and bar have different internal type because in bar Agda uses eta,
i.e. (_≡_ x) is the same as (λ y → x ≡ y).


* Martin-Löf cite
From Peter:
Just a note. In one of <NAME>'s first papers on
type theory he explicitly writes down translations of a number of well
known theories into type theory, including a translation of first
order intuitionistic predicate logic using Curry-Howard.  This might
actually be useful to look at, and to cite.<commit_msg>Only white space.<commit_after>* The handling of ATP stuff inside where clauses
*** The problems
*** This facilitate the writes of ATP axioms. e.g.
LTC.Examples.GCD.Extra.S≤0-elim : {A : Set}{d : D} → succ d ≤ zero → A

* The difference between predicates' definitions and functions' definitions
From Agda internal representation of clauses, both definitions are
equal, the only difference is in the type of the symbol.

* The problem with eta and the existential
postulate
  D   : Set
  _≡_ : D → D → Set
  P   : (D → Set) → Set
  foo : (x : D) → P (λ y → y ≡ x)
  bar : (x : D) → P (λ y → x ≡ y)

foo and bar have different internal type because in bar Agda uses eta,
i.e. (_≡_ x) is the same as (λ y → x ≡ y).

* Martin-Löf cite
From Peter:
Just a note. In one of Per Martin-Löf's first papers on
type theory he explicitly writes down translations of a number of well
known theories into type theory, including a translation of first
order intuitionistic predicate logic using Curry-Howard.  This might
actually be useful to look at, and to cite.
{'fraction_non_alphanumeric': 0.08337326305701964, 'fraction_numerical': 0.0009583133684714902, 'mean_word_length': 3.4520255863539444, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 4, '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': '4113282', 'n_tokens_mistral': 665, 'n_tokens_neox': 636, 'n_words': 364}