name: "hott";
version: "0.1.0";
description: "add your description here";
functions {
  HLev : HLev';
  I : I';
  hcontr_eq : x -> (HLev'(z', x) == HLev'(z', true));
  hcontr_tr : true -> HLev'(z', true);
  hcontr_unit : true -> (true : true);
  hlev_cong : (n : nat') -> cong'(HLev'(n));
  hlev_contr_to_prop : HLev'(z', x) -> HLev'(s'(z'), x);
  hlev_eq_right : ((n : nat') & (x == y)) -> (HLev'(n, x) == HLev'(n, y));
  hlev_prop : HLev'(s'(z'), x) -> (((a : x) & (b : x)) => ((a ~~ b) : I' => x));
  hlev_prop_eq : true -> (sym(x, ((a : x') & (b : x')) => HLev'(z', (a ~~ b) : I' => x'))(x) == sym(x, ((a : x') & (b : x')) => ((a ~~ b) : I' => x'))(x));
  hlev_prop_from : sym(x, all(((a : x') & (b : x')) => ((a ~~ b) : I' => x')))(x) -> HLev'(s'(z'), x);
  hlev_prop_qu : HLev'(s'(z'), x) -> ((a : x) => (~a : I' => x));
  hlev_set : (HLev'(s'(s'(z')), x) & ((a : x) & (b : x))) -> (((p : (a ~~ b) : I' => x) & (q : (a ~~ b) : I' => x)) => ((p ~~ q) : I' => ((a ~~ b) : I' => x)));
  hlev_sn : (n : nat') -> (HLev'(s'(n), x) == sym(n, sym(x, all(((a : x') & (b : x')) => HLev'(n', (a ~~ b) : I' => x'))))(n, x));
  hlev_sn_from : ((n : nat') & sym(n, sym(x, all(((a : x') & (b : x')) => HLev'(n', (a ~~ b) : I' => x'))))(n, x)) -> HLev'(s'(n), x);
  hlev_sn_to : ((n : nat') & HLev'(s'(n), x)) -> sym(n, sym(x, all(((a : x') & (b : x')) => HLev'(n', (a ~~ b) : I' => x'))))(n, x);
  hlev_sn_to_concrete : ((n : nat') & HLev'(s'(n), x)) -> (((a : x) & (b : x)) => HLev'(n, (a ~~ b) : I' => x));
  hlev_z : true -> (HLev'(z', x) == x);
  hlev_z_from : x -> HLev'(z', x);
  hlev_z_to : HLev'(z', x) -> x;
  hprop_fa : ((a : false) & (b : false)) -> ((a ~~ b) : !I');
  hprop_fa_hlev : true -> HLev'(s'(z'), false);
  hprop_tr : ((a : true) & (b : true)) -> ((a ~~ b) : I' => true);
  hprop_tr_hlev : true -> HLev'(s'(z'), true);
  i0 : i0';
  i0_ty : true -> (i0' : I');
  i1 : i1';
  i1_ty : true -> (i1' : I');
  i_left_ty : (f : I' => a) -> (f(i0') : a);
  i_points : ((a ~~ b) : I' => x) -> ((a : x) & (b : x));
  i_right_ty : (f : I' => a) -> (f(i1') : a);
  i_ty : true -> (I' : type'(z'));
  iq_cong : true -> cong'(a ~~ b);
  iq_left : true -> ((a ~~ b)(i0') == a);
  iq_right : true -> ((a ~~ b)(i1') == b);
  iqu_cong : true -> cong'(~a);
  iqu_left : true -> (~a(i0') == a);
  iqu_right : true -> (~a(i1') == a);
}
dependencies {
}