<commit_before>/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: init.funext
Author: <NAME>

Function extensionality follows from quotients.
-/
prelude
import init.quot init.logic

section
  open quot
  variables {A : Type} {B : A → Type}

  private definition fun_eqv (f₁ f₂ : Πx : A, B x) : Prop := ∀x, f₁ x = f₂ x

  infix `~` := fun_eqv

  private theorem fun_eqv.refl (f : Πx : A, B x) : f ~ f := take x, rfl

  private theorem fun_eqv.symm {f₁ f₂ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₁ :=
  λH x, eq.symm (H x)

  private theorem fun_eqv.trans {f₁ f₂ f₃ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
  λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)

  private theorem fun_eqv.is_equivalence (A : Type) (B : A → Type) : equivalence (@fun_eqv A B) :=
  mk_equivalence (@fun_eqv A B) (@fun_eqv.refl A B) (@fun_eqv.symm A B) (@fun_eqv.trans A B)

  definition fun_setoid [instance] (A : Type) (B : A → Type) : setoid (Πx : A, B x) :=
  setoid.mk (@fun_eqv A B) (fun_eqv.is_equivalence A B)

  definition extfun (A : Type) (B : A → Type) : Type :=
  quot (fun_setoid A B)

  definition fun_to_extfun (f : Πx : A, B x) : extfun A B :=
  ⟦f⟧

  definition extfun_app (f : extfun A B) : Πx : A, B x :=
  take x,
  quot.lift_on f
    (λf : Πx : A, B x, f x)
    (λf₁ f₂ H, H x)

  theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
  assume H, calc
     f₁ = extfun_app ⟦f₁⟧      : rfl
    ... = extfun_app ⟦f₂⟧      : {sound H}
    ... = f₂                   : rfl
end

definition subsingleton_pi [instance] {A : Type} {B : A → Type} (H : ∀ a, subsingleton (B a)) : subsingleton (Π a, B a) :=
subsingleton.intro (take f₁ f₂,<commit_msg>refactor(library/init/funext.lean): break out definition of equivalence, and hide auxiliary theorems<commit_after>/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: init.funext
Author: <NAME>

Extensional equality for functions, and a proof of function extensionality from quotients.
-/
prelude
import init.quot init.logic

namespace function
  variables {A : Type} {B : A → Type}

  protected definition equiv (f₁ f₂ : Πx : A, B x) : Prop := ∀x, f₁ x = f₂ x

  namespace equiv_notation
    infix `~` := function.equiv
  end equiv_notation
  open equiv_notation

  protected theorem equiv.refl (f : Πx : A, B x) : f ~ f := take x, rfl

  protected theorem equiv.symm {f₁ f₂ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₁ :=
  λH x, eq.symm (H x)

  protected theorem equiv.trans {f₁ f₂ f₃ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
  λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)

  protected theorem equiv.is_equivalence (A : Type) (B : A → Type) : equivalence (@equiv A B) :=
  mk_equivalence (@equiv A B) (@equiv.refl A B) (@equiv.symm A B) (@equiv.trans A B)
end function

context
  open quot
  variables {A : Type} {B : A → Type}

  private definition fun_setoid [instance] (A : Type) (B : A → Type) : setoid (Πx : A, B x) :=
  setoid.mk (@function.equiv A B) (function.equiv.is_equivalence A B)

  private definition extfun (A : Type) (B : A → Type) : Type :=
  quot (fun_setoid A B)

  private definition fun_to_extfun (f : Πx : A, B x) : extfun A B :=
  ⟦f⟧

  private definition extfun_app (f : extfun A B) : Πx : A, B x :=
  take x,
  quot.lift_on f
    (λf : Πx : A, B x, f x)
    (λf₁ f₂ H, H x)

  theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
  assume H, calc
     f₁ = extfun_app ⟦f₁⟧ : rfl
    ... = extfun_app ⟦f₂⟧ : {sound H}
    ... = f₂             : rfl
end

open function.equiv_notation

definition subsingleton_pi [instance] {A : Type} {B : A → Type} (H : ∀ a, subsingleton (B a)) :
  subsingleton (Π a, B a) :=
subsingleton.intro (take f₁ f₂,
{'fraction_non_alphanumeric': 0.1333157338965153, 'fraction_numerical': 0.0031678986272439284, 'mean_word_length': 2.8004012036108326, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2098621', 'n_tokens_mistral': 1617, 'n_tokens_neox': 1606, 'n_words': 576}