eta-counterexample gets accepted by agda-core(?)

Author: diode-lang

test/EtaFunctions.agda

@@ -29,6 +29,8 @@ addTwoAfterAddOne = λ x → (comp Nat Nat Nat addTwo addOne x)
 eta-higher : (A B C : Set) → (f : A → B → C) → (λ x → λ y → f x y) ≡ f
 eta-higher = λ A B C → λ f → refl
 
-
-test : addTwoAfterAddOne ≡ (λ x → (comp Nat Nat Nat addTwo addOne) x)
-test = refl
+-- In this case, the type which Agda infers is addTwoAfterAddOne ≡ comp Nat Nat Nat addTwo addOne
+-- So the agda-core typechecker would expand `addTwoAfterAddOne`, which expands to λ x → (comp Nat Nat Nat addTwo addOne x)
+-- and the remaining equation would need to be solved by either eta-reduction or eta-expansion
+eta-counterexample : addTwoAfterAddOne ≡ (λ x → (comp Nat Nat Nat addTwo addOne) x)
+eta-counterexample = refl

test/EtaFunctionsChurch.agda

@@ -15,18 +15,6 @@ Id = λ A x y → (P : A → Set) → P x → P y
 refl : (A : Set) (x : A) → Id A x x
 refl = λ A x P p → p
 
-id_typ : Set → Set
-id_typ = λ A → A
-
-s : Set → Set
-s = λ typ → id_typ typ
-
-s' : (Set → Set) → Set → Set
-s' = λ f → λ typ → f typ
-
-id : (A : Set) → A → A
-id = λ A x → x
-
 idbool : Bool → Bool
 idbool = λ b → b
 
@@ -43,19 +31,25 @@ addTwo = λ x → (suc (suc x))
 addTwoAfterAddOne : Nat → Nat
 addTwoAfterAddOne = λ x → (comp Nat Nat Nat addTwo addOne x)
 
-
--- eta-functions : {A B : Set} (f : A → B) → (f ≡ (λ x → f x))
--- eta-functions = λ h → refl
-
 eta-functions_expl : (A B : Set) (f : A → B) → (Id (A → B) f (λ x → f x))
 eta-functions_expl = λ A B → λ f → refl (A → B) f
 
 eta-functions_two : (A B C : Set) (f : B → C) → (g : A → B) → (Id (A → C) (comp A B C f g) (λ x → (comp A B C f g) x))
 eta-functions_two = λ A B C → λ f → λ g → refl (A → C) (comp A B C f g)
 
+-- apply : (A B : Set) → (A → B) → A → B
+-- apply = λ A B → λ f → λ x → f x
+
+-- eta-apply : (A B : Set) → (f : A → B) → Id (apply f) f
+
+
+eta-counterexample : Id (Nat → Nat) addTwoAfterAddOne (λ x → (comp Nat Nat Nat addTwo addOne) x)
+eta-counterexample = refl (Nat → Nat) addTwoAfterAddOne
+
+
+eta-counterexample-simple : Id (Nat → Nat) addOne (λ y → (λ x → (suc x)) y)
+eta-counterexample-simple = refl (Nat → Nat) addOne
 
-test : Id addTwoAfterAddOne (λ x → (comp Nat Nat Nat addTwo addOne) x)
-test = refl
 
 -- eta-higher : (A B C : Set) → (f : A → B → C) → Id (λ x → λ y → f x y) f
 -- eta-higher = λ A B C → λ f → refl