tmp.v

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/test" "HoTT.Tests" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Top.bug_01") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 231 lines to 38 lines, then from 51 lines to 162 lines, then from 167 lines to 41 lines, then from 54 lines to 475 lines, then from 480 lines to 42 lines, then from 55 lines to 133 lines, then from 138 lines to 42 lines, then from 55 lines to 453 lines, then from 458 lines to 82 lines, then from 95 lines to 780 lines, then from 780 lines to 164 lines, then from 177 lines to 2432 lines, then from 2435 lines to 207 lines, then from 220 lines to 1079 lines, then from 1080 lines to 230 lines, then from 243 lines to 296 lines, then from 301 lines to 232 lines, then from 245 lines to 1327 lines, then from 1332 lines to 252 lines, then from 265 lines to 1073 lines, then from 1068 lines to 266 lines, then from 279 lines to 318 lines, then from 323 lines to 279 lines, then from 292 lines to 622 lines, then from 626 lines to 280 lines, then from 293 lines to 384 lines, then from 389 lines to 284 lines, then from 297 lines to 851 lines, then from 856 lines to 368 lines, then from 381 lines to 519 lines, then from 521 lines to 443 lines, then from 456 lines to 498 lines, then from 503 lines to 454 lines, then from 467 lines to 731 lines, then from 736 lines to 484 lines, then from 497 lines to 735 lines, then from 740 lines to 544 lines, then from 557 lines to 1422 lines, then from 1426 lines to 552 lines, then from 565 lines to 2044 lines, then from 2045 lines to 552 lines, then from 565 lines to 1364 lines, then from 1365 lines to 592 lines, then from 605 lines to 1390 lines, then from 1394 lines to 700 lines, then from 713 lines to 803 lines, then from 808 lines to 705 lines, then from 718 lines to 1026 lines, then from 1028 lines to 730 lines, then from 735 lines to 730 lines, then from 723 lines to 617 lines, then from 622 lines to 618 lines *)
(* coqc version 8.21+alpha compiled with OCaml 4.09.0
   coqtop version runner-t7b1znuaq-project-4504-concurrent-2:/builds/coq/coq/_build/default,(HEAD detached at 01e8890dbcb983) (01e8890dbcb983bb6babb0d95bfd01b1aaf7354e)
   Expected coqc runtime on this file: 0.150 sec *)

Module Export HoTT_DOT_Basics_DOT_Notations_WRAPPED.
Module Export Notations.

Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).

Reserved Notation "x = y  :>  T"
(at level 70, y at next level, no associativity).
Reserved Notation "x * y" (at level 40, left associativity).
Reserved Notation "- x" (at level 35, right associativity).
Reserved Notation "f == g" (at level 70, no associativity).
Reserved Notation "g 'o' f" (at level 40, left associativity).
Declare Scope fibration_scope.
Delimit Scope function_scope with function.
Delimit Scope type_scope with type.
Delimit Scope trunc_scope with trunc.

Global Open Scope trunc_scope.
Global Open Scope fibration_scope.
Global Open Scope type_scope.

End Notations.
Module Export HoTT.
Module Export Basics.
Module Export Notations.
Include HoTT_DOT_Basics_DOT_Notations_WRAPPED.Notations.
End Notations.

End Basics.

Declare ML Module "ltac_plugin".

Declare ML Module "number_string_notation_plugin".

Global Set Default Proof Mode "Classic".

Global Set Universe Polymorphism.

Global Unset Strict Universe Declaration.
Create HintDb typeclass_instances discriminated.

Notation "A -> B" := (forall (_ : A), B) : type_scope.

Inductive option (A : Type) : Type :=
  | Some : A -> option A
  | None : option A.

Arguments Some {A} a.
Arguments None {A}.

Register option as core.option.type.

Record prod (A B : Type) := pair { fst : A ; snd : B }.

Notation "x * y" := (prod x y) : type_scope.

Notation Type0 := Set.

Notation idmap := (fun x => x).

Record sig {A} (P : A -> Type) := exist {
  proj1 : A ;
  proj2 : P proj1 ;
}.

Arguments exist {A}%_type P%_type _ _.
Arguments proj1 {A P} _ / .

Notation "( x ; y )" := (exist _ x y) : fibration_scope.

Notation pr1 := proj1.

Notation "x .1" := (pr1 x) (at level 3) : fibration_scope.

Notation compose := (fun g f x => g (f x)).

Notation "g 'o' f" := (compose g%function f%function) : function_scope.

Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.

Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) (at level 70) : type_scope.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y.
Admitted.

Definition pointwise_paths A (P : A -> Type) (f g : forall x, P x)
  := forall x, f x = g x.

Global Arguments pointwise_paths {A}%_type_scope {P} (f g)%_function_scope.

Notation "f == g" := (pointwise_paths f g) : type_scope.

Class IsEquiv {A B : Type} (f : A -> B) := {
  equiv_inv : B -> A ;
  eisretr : f o equiv_inv == idmap ;
  eissect : equiv_inv o f == idmap ;
  eisadj : forall x : A, eisretr (f x) = ap f (eissect x) ;
}.

Inductive trunc_index : Type0 :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.

Notation "n .+1" := (trunc_S n) (at level 3) : trunc_scope.
Notation "n .+2" := (n.+1.+1)%trunc (at level 3) : trunc_scope.

Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| Build_Contr : forall (center : A) (contr : forall y, center = y), IsTrunc_internal A minus_two
| istrunc_S : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).

Existing Class IsTrunc_internal.

Notation IsTrunc n A := (IsTrunc_internal A n).
Notation IsHProp A := (IsTrunc minus_two.+1 A).

Monomorphic Axiom Funext : Type0.
Existing Class Funext.

Inductive nat : Type0 :=
| O : nat
| S : nat -> nat.
Delimit Scope nat_scope with nat.
Bind Scope nat_scope with nat.

Inductive Empty : Type0 := .

Definition not (A : Type) := A -> Empty.

Inductive Unit : Type0 := tt : Unit.

Tactic Notation "do_with_holes" tactic3(x) uconstr(p) :=
  x uconstr:(p) ||
  x uconstr:(p _) ||
  x uconstr:(p _ _) ||
  x uconstr:(p _ _ _) ||
  x uconstr:(p _ _ _ _) ||
  x uconstr:(p _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
  x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).

Tactic Notation "srefine" uconstr(term) := simple refine term.

Tactic Notation "rapply" uconstr(term)
  := do_with_holes ltac:(fun x => refine x) term.

Tactic Notation "srapply" uconstr(term)
  := do_with_holes ltac:(fun x => srefine x) term.
Module Export Decimal.

Inductive uint : Type0 :=
 | Nil
 | D0 (_:uint)
 | D1 (_:uint)
 | D2 (_:uint)
 | D3 (_:uint)
 | D4 (_:uint)
 | D5 (_:uint)
 | D6 (_:uint)
 | D7 (_:uint)
 | D8 (_:uint)
 | D9 (_:uint).

Notation zero := (D0 Nil).

Variant int : Type0 := Pos (d:uint) | Neg (d:uint).

Variant decimal : Type0 :=
 | Decimal (i:int) (f:uint)
 | DecimalExp (i:int) (f:uint) (e:int).

Register uint as num.uint.type.
Register int as num.int.type.
Register decimal as num.decimal.type.

Fixpoint revapp (d d' : uint) :=
  match d with
  | Nil => d'
  | D0 d => revapp d (D0 d')
  | D1 d => revapp d (D1 d')
  | D2 d => revapp d (D2 d')
  | D3 d => revapp d (D3 d')
  | D4 d => revapp d (D4 d')
  | D5 d => revapp d (D5 d')
  | D6 d => revapp d (D6 d')
  | D7 d => revapp d (D7 d')
  | D8 d => revapp d (D8 d')
  | D9 d => revapp d (D9 d')
  end.

Definition rev d := revapp d Nil.

Module Export Little.

Fixpoint succ d :=
  match d with
  | Nil => D1 Nil
  | D0 d => D1 d
  | D1 d => D2 d
  | D2 d => D3 d
  | D3 d => D4 d
  | D4 d => D5 d
  | D5 d => D6 d
  | D6 d => D7 d
  | D7 d => D8 d
  | D8 d => D9 d
  | D9 d => D0 (succ d)
  end.
Module Export Hexadecimal.

Inductive uint : Type0 :=
 | Nil
 | D0 (_:uint)
 | D1 (_:uint)
 | D2 (_:uint)
 | D3 (_:uint)
 | D4 (_:uint)
 | D5 (_:uint)
 | D6 (_:uint)
 | D7 (_:uint)
 | D8 (_:uint)
 | D9 (_:uint)
 | Da (_:uint)
 | Db (_:uint)
 | Dc (_:uint)
 | Dd (_:uint)
 | De (_:uint)
 | Df (_:uint).

Variant int : Type0 := Pos (d:uint) | Neg (d:uint).

Variant hexadecimal : Type0 :=
 | Hexadecimal (i:int) (f:uint)
 | HexadecimalExp (i:int) (f:uint) (e:Decimal.int).

Register uint as num.hexadecimal_uint.type.
Register int as num.hexadecimal_int.type.
Register hexadecimal as num.hexadecimal.type.
Module Export Numeral.

Variant uint : Type0 := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint).

Variant int : Type0 := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int).

Variant numeral : Type0 := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal).

Register uint as num.num_uint.type.
Register int as num.num_int.type.
Register numeral as num.number.type.
Module Export Nat.

Fixpoint tail_add n m :=
  match n with
    | O => m
    | S n => tail_add n (S m)
  end.

Fixpoint tail_addmul r n m :=
  match n with
    | O => r
    | S n => tail_addmul (tail_add m r) n m
  end.

Definition tail_mul n m := tail_addmul O n m.

Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))).

Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) :=
  match d with
  | Decimal.Nil => acc
  | Decimal.D0 d => of_uint_acc d (tail_mul ten acc)
  | Decimal.D1 d => of_uint_acc d (S (tail_mul ten acc))
  | Decimal.D2 d => of_uint_acc d (S (S (tail_mul ten acc)))
  | Decimal.D3 d => of_uint_acc d (S (S (S (tail_mul ten acc))))
  | Decimal.D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc)))))
  | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc))))))
  | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc)))))))
  | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc))))))))
  | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))
  | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))))
  end.

Definition of_uint (d:Decimal.uint) := of_uint_acc d O.

Local Notation sixteen := (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))).

Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) :=
  match d with
  | Hexadecimal.Nil => acc
  | Hexadecimal.D0 d => of_hex_uint_acc d (tail_mul sixteen acc)
  | Hexadecimal.D1 d => of_hex_uint_acc d (S (tail_mul sixteen acc))
  | Hexadecimal.D2 d => of_hex_uint_acc d (S (S (tail_mul sixteen acc)))
  | Hexadecimal.D3 d => of_hex_uint_acc d (S (S (S (tail_mul sixteen acc))))
  | Hexadecimal.D4 d => of_hex_uint_acc d (S (S (S (S (tail_mul sixteen acc)))))
  | Hexadecimal.D5 d => of_hex_uint_acc d (S (S (S (S (S (tail_mul sixteen acc))))))
  | Hexadecimal.D6 d => of_hex_uint_acc d (S (S (S (S (S (S (tail_mul sixteen acc)))))))
  | Hexadecimal.D7 d => of_hex_uint_acc d (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))
  | Hexadecimal.D8 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))
  | Hexadecimal.D9 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))
  | Hexadecimal.Da d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))
  | Hexadecimal.Db d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))
  | Hexadecimal.Dc d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))
  | Hexadecimal.Dd d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))
  | Hexadecimal.De d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))))
  | Hexadecimal.Df d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))))
  end.

Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.

Definition of_num_uint (d:Numeral.uint) :=
  match d with
  | Numeral.UIntDec d => of_uint d
  | Numeral.UIntHex d => of_hex_uint d
  end.

Fixpoint to_little_uint n acc :=
  match n with
  | O => acc
  | S n => to_little_uint n (Decimal.Little.succ acc)
  end.

Definition to_uint n :=
  Decimal.rev (to_little_uint n Decimal.zero).

Definition to_num_uint n := Numeral.UIntDec (to_uint n).

Number Notation nat of_num_uint to_num_uint (abstract after 5001) : nat_scope.
Generalizable Variables A B m n f.
Definition nat_to_trunc_index@{} (n : nat) : trunc_index.
Admitted.
Definition int_to_trunc_index@{} (v : Decimal.int) : option trunc_index.
exact (match v with
     | Decimal.Pos d => Some (nat_to_trunc_index (Nat.of_uint d))
     | Decimal.Neg d => match Nat.of_uint d with
                        | 2%nat => Some minus_two
                        | 1%nat => Some (minus_two.+1)
                        | 0%nat => Some (minus_two.+2)
                        | _ => None
                        end
     end).
Defined.
Definition num_int_to_trunc_index@{} (v : Numeral.int) : option trunc_index.
exact (match v with
  | Numeral.IntDec v => int_to_trunc_index v
  | Numeral.IntHex _ => None
  end).
Defined.

Fixpoint trunc_index_to_little_uint@{} n acc :=
  match n with
  | minus_two => acc
  | minus_two.+1 => acc
  | minus_two.+2 => acc
  | trunc_S n => trunc_index_to_little_uint n (Decimal.Little.succ acc)
  end.

Definition trunc_index_to_int@{} n :=
  match n with
  | minus_two => Decimal.Neg (Nat.to_uint 2)
  | minus_two.+1 => Decimal.Neg (Nat.to_uint 1)
  | n => Decimal.Pos (Decimal.rev (trunc_index_to_little_uint n Decimal.zero))
  end.

Definition trunc_index_to_num_int@{} n :=
  Numeral.IntDec (trunc_index_to_int n).

Number Notation trunc_index num_int_to_trunc_index trunc_index_to_num_int
  : trunc_scope.

Global Instance istrunc_paths' {n : trunc_index} {A : Type} `{IsTrunc n A}
  : forall x y : A, IsTrunc n (x = y) | 1000.
Admitted.

Definition istrunc_isequiv_istrunc A {B} (f : A -> B)
  `{IsTrunc n A} `{IsEquiv A B f}
  : IsTrunc n B.
Admitted.

Record TruncType (n : trunc_index) := {
  trunctype_type : Type ;
  trunctype_istrunc : IsTrunc n trunctype_type
}.

Arguments Build_TruncType _ _ {_}.

Coercion trunctype_type : TruncType >-> Sortclass.

Notation "n -Type" := (TruncType n) (at level 3) : type_scope.
Notation HProp := (-1)-Type.

Notation Build_HProp := (Build_TruncType (-1)).

Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
  : IsHProp (IsTrunc n A) | 0.
Admitted.

Local Open Scope nat_scope.

  Definition ExtensionAlong@{a b p m} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
             (P : B -> Type@{p}) (d : forall x:A, P (f x))
    :=
       sig@{m m} (fun (s : forall y:B, P y) => forall x:A, s (f x) = d x).

  Fixpoint ExtendableAlong@{i j k l}
           (n : nat) {A : Type@{i}} {B : Type@{j}}
           (f : A -> B) (C : B -> Type@{k}) : Type@{l}
    := match n with
         | 0 => Unit
         | S n => (forall (g : forall a, C (f a)),
                     ExtensionAlong@{i j k l} f C g) *
                  forall (h k : forall b, C b),
                    ExtendableAlong n f (fun b => h b = k b)
       end.
Definition ooExtendableAlong@{i j k l}
             {A : Type@{i}} {B : Type@{j}}
             (f : A -> B) (C : B -> Type@{k}) : Type@{l}.
exact (forall n : nat, ExtendableAlong@{i j k l} n f C).
Defined.
Import HoTT.Basics.

Record Subuniverse@{i} :=
{
  In_internal : Type@{i} -> Type@{i} ;
  hprop_inO_internal : Funext -> forall (T : Type@{i}),
      IsHProp (In_internal T) ;
  inO_equiv_inO_internal : forall (T U : Type@{i}) (T_inO : In_internal T)
                                  (f : T -> U) {feq : IsEquiv f},
      In_internal U ;
}.

Class In (O : Subuniverse) (T : Type) := in_internal : In_internal O T.

Class PreReflects@{i} (O : Subuniverse@{i}) (T : Type@{i}) :=
{
  O_reflector : Type@{i} ;
  O_inO : In O O_reflector ;
  to : T -> O_reflector ;
}.

Arguments O_reflector O T {_}.
Arguments to O T {_}.

Class Reflects@{i} (O : Subuniverse@{i}) (T : Type@{i})
      `{PreReflects@{i} O T} :=
{
  extendable_to_O : forall {Q : Type@{i}} {Q_inO : In O Q},
      ooExtendableAlong (to O T) (fun _ => Q)
}.

Record ReflectiveSubuniverse@{i} :=
{
  rsu_subuniv : Subuniverse@{i} ;
  rsu_prereflects : forall (T : Type@{i}), PreReflects rsu_subuniv T ;
  rsu_reflects : forall (T : Type@{i}), Reflects rsu_subuniv T ;
}.

Coercion rsu_subuniv : ReflectiveSubuniverse >-> Subuniverse.
Global Existing Instance rsu_prereflects.
Definition rsu_reflector (O : ReflectiveSubuniverse) (T : Type) : Type.
exact (O_reflector O T).
Defined.

Coercion rsu_reflector : ReflectiveSubuniverse >-> Funclass.

Class ReflectsD@{i} (O' O : Subuniverse@{i}) (T : Type@{i})
      `{PreReflects@{i} O' T} :=
{
  extendable_to_OO :
    forall (Q : O_reflector O' T -> Type@{i}) {Q_inO : forall x, In O (Q x)},
      ooExtendableAlong (to O' T) Q
}.

Definition reflectsD_from_OO_ind@{i} {O' O : Subuniverse@{i}}
           {A : Type@{i}} `{PreReflects O' A}
           (OO_ind' : forall (B : O_reflector O' A -> Type@{i})
                             (B_inO : forall oa, In O (B oa))
                             (f : forall a, B (to O' A a))
                             oa, B oa)
           (OO_ind_beta' : forall (B : O_reflector O' A -> Type@{i})
                             (B_inO : forall oa, In O (B oa))
                             (f : forall a, B (to O' A a))
                             a, OO_ind' B B_inO f (to O' A a) = f a)
           (inO_paths' : forall (B : Type@{i}) (B_inO : In O B)
                      (z z' : B), In O (z = z'))
  : ReflectsD O' O A.
Admitted.

Record Modality@{i} := Build_Modality'
{
  modality_subuniv : Subuniverse@{i} ;
  modality_prereflects : forall (T : Type@{i}),
      PreReflects modality_subuniv T ;
  modality_reflectsD : forall (T : Type@{i}),
      ReflectsD modality_subuniv modality_subuniv T ;
}.

Global Existing Instance modality_reflectsD.

Definition modality_to_reflective_subuniverse (O : Modality@{i})
  : ReflectiveSubuniverse@{i}.
Proof.
  refine (Build_ReflectiveSubuniverse
            (modality_subuniv O) (modality_prereflects O) _).
  intros T; constructor.
  intros Q Q_inO.
  srapply extendable_to_OO.
Defined.

Coercion modality_to_reflective_subuniverse : Modality >-> ReflectiveSubuniverse.

Definition merely (A : Type@{i}) : HProp@{i}.
Admitted.

Section SwapTypes.

  Context (A B : Type).

  Lemma foo X (p:merely (X = B)) :
    sig (fun p0 : not (merely (X = A)) =>
           merely ((exist (fun a => not (merely (a = A))) X p0).1 = B)).
    refine (fun q => _ ; p).