<commit_before>-- Copyright (c) 2014 <NAME>. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: <NAME>
-- Ported from Coq HoTT
import hott.path hott.trunc data.sigma data.prod

open path prod

inductive is_pointed [class] (A : Type) :=
  pointed_mk : Π(a : A), is_pointed A

namespace is_pointed
  variables {A B : Type} (f : A → B)

  definition point (A : Type) [H : is_pointed A] : A :=
    is_pointed.rec (λinv, inv) H

  -- Any contractible type is pointed
  protected definition contr [instance] (H : Contr A) : is_pointed A :=
    pointed_mk (center H)

  -- A pi type with a pointed target is pointed
  protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)]
      : is_pointed (Πx, P x) :=
    pointed_mk (λx, point (P x))

  -- A sigma type of pointed components is pointed
  protected definition sigma [instance] {P : A → Type} [G : is_pointed A]
      [H : is_pointed (P (point A))] : is_pointed (Σx, P x) :=
    pointed_mk (sigma.dpair (point A) (point (P (point A))))

  protected definition prod [H1 : is_pointed A] [H2 : is_pointed B]
      : is_pointed (A × B) :=
    pointed_mk (prod.mk (point A) (point B))
<commit_msg>fix(library/hott) changed pointed.lean to use trunc.lean correctly<commit_after>-- Copyright (c) 2014 <NAME>. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: <NAME>
-- Ported from Coq HoTT
import hott.path hott.trunc data.sigma data.prod

open path prod truncation

inductive is_pointed [class] (A : Type) :=
  pointed_mk : Π(a : A), is_pointed A

namespace is_pointed
  variables {A B : Type.{1}} (f : A → B)

  definition point (A : Type) [H : is_pointed A] : A :=
    is_pointed.rec (λinv, inv) H

  -- Any contractible type is pointed
  protected definition contr [instance] [H : is_contr A] : is_pointed A :=
    pointed_mk (center A)

  -- A pi type with a pointed target is pointed
  protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)]
      : is_pointed (Πx, P x) :=
    pointed_mk (λx, point (P x))

  -- A sigma type of pointed components is pointed
  protected definition sigma [instance] {P : A → Type} [G : is_pointed A]
      [H : is_pointed (P (point A))] : is_pointed (Σx, P x) :=
    pointed_mk (sigma.dpair (point A) (point (P (point A))))

  protected definition prod [H1 : is_pointed A] [H2 : is_pointed B]
      : is_pointed (A × B) :=
    pointed_mk (prod.mk (point A) (point B))

{'fraction_non_alphanumeric': 0.12274368231046931, 'fraction_numerical': 0.00681909346169274, 'mean_word_length': 3.1986531986531985, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, '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': '2727948', 'n_tokens_mistral': 895, 'n_tokens_neox': 875, 'n_words': 343}