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

import data.unit data.bool data.nat
import data.prod data.sum data.sigma

open unit bool nat prod sum sigma

inductive fibrant [class] (T : Type) : Type :=
fibrant_mk : fibrant T

namespace fibrant

axiom unit_fibrant : fibrant unit
axiom nat_fibrant : fibrant nat
axiom bool_fibrant : fibrant bool
axiom sum_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A ⊎ B)
axiom prod_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A × B)
axiom sigma_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) :
  fibrant (Σx : A, B x)
axiom pi_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) :
  fibrant (Πx : A, B x)

instance [persistent] unit_fibrant
instance [persistent] nat_fibrant
instance [persistent] bool_fibrant
instance [persistent] sum_fibrant
instance [persistent] prod_fibrant
instance [persistent] sigma_fibrant
instance [persistent] pi_fibrant

end fibrant<commit_msg>fix(library/hott/fibrant): set arguments for type class resolution<commit_after>-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: <NAME>

import data.unit data.bool data.nat
import data.prod data.sum data.sigma

open unit bool nat prod sum sigma

inductive fibrant [class] (T : Type) : Type :=
fibrant_mk : fibrant T

namespace fibrant

axiom unit_fibrant : fibrant unit
axiom nat_fibrant : fibrant nat
axiom bool_fibrant : fibrant bool
axiom sum_fibrant {A B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A ⊎ B)
axiom prod_fibrant {A B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A × B)
axiom sigma_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
  fibrant (Σx : A, B x)
axiom pi_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
  fibrant (Πx : A, B x)

instance [persistent] unit_fibrant
instance [persistent] nat_fibrant
instance [persistent] bool_fibrant
instance [persistent] sum_fibrant
instance [persistent] prod_fibrant
instance [persistent] sigma_fibrant
instance [persistent] pi_fibrant

end fibrant
{'fraction_non_alphanumeric': 0.10528577567683713, 'fraction_numerical': 0.012032660077352814, 'mean_word_length': 4.327231121281464, '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': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2941277', 'n_tokens_mistral': 921, 'n_tokens_neox': 868, 'n_words': 319}