Library MetaCoq.Translations.param_generous_packed

Reserved Notation "'tsl_ty_param'".


Definition pair (typ1 typ2 t1 t2 : term) : term
  := tApp tPair [ typ1 ; typ2 ; t1 ; t2].
Definition pack (t u : term) : term
  := tApp tSigma [ t ; u ].
Definition sigma_ind := Eval compute in
  match tSigma with tInd i _ ⇒ i | _ ⇒ mkInd "bug: sigma not an inductive" 0 end.
Definition proj1 (t : term) : term
  := tProj (sigma_ind, 2, 0) t.
Definition proj2 (t : term) : term
  := tProj (sigma_ind, 2, S 0) t.
Definition proj (b : bool) (t : term) : term
  := tProj (sigma_ind, 2, if b then 0 else S 0) t.

Fixpoint refresh_universes (t : term) {struct t} :=
  match t with
  | tSort s ⇒ tSort (if Universe.is_level s then s else fresh_universe)
  | tProd na b t ⇒ tProd na b (refresh_universes t)
  | tLetIn na b t' t ⇒ tLetIn na b t' (refresh_universes t)
  | _ ⇒ t
  end.


Fixpoint tsl_rec (fuel : nat) (Σ : global_env_ext) (E : tsl_table) (Γ : context)
         (b : bool) (t : term) {struct fuel} : tsl_result term :=
  match fuel with
  | O ⇒ raise NotEnoughFuel
  | S fuel ⇒
  match t with
  | tRel n ⇒ ret (proj b (tRel n))

  | tSort s ⇒
    if b then ret (tSort s)
    else ret (tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s)))

  | tCast t c A ⇒ if b then
                    t1 <- tsl_rec fuel Σ E Γ true t ;;
                    A1 <- tsl_rec fuel Σ E Γ true A ;;
                    ret (tCast t1 c A1)
                  else
                    t1 <- tsl_rec fuel Σ E Γ true t ;;
                    t2 <- tsl_rec fuel Σ E Γ false t ;;
                    A2 <- tsl_rec fuel Σ E Γ false A ;;
                    ret (tCast t2 c (tApp A2 [t1]))

  | tProd n A B ⇒
    if b then
      A' <- tsl_ty_param fuel Σ E Γ A ;;
         B1 <- tsl_rec fuel Σ E (Γ ,, vass n A) true B ;;
         ret (tProd n A' B1)
    else
      A' <- tsl_ty_param fuel Σ E Γ A ;;
      B1 <- tsl_rec fuel Σ E (Γ ,, vass n A) true B ;;
      B2 <- tsl_rec fuel Σ E (Γ ,, vass n A) false B ;;
      ret (tLambda (nNamed "f") (tProd n A' B1)
                   (tProd n (lift 1 0 A')
                          (tApp (lift 1 1 B2)
                                [tApp (tRel 1) [tRel 0]])))

  | tLambda n A t ⇒ A' <- tsl_ty_param fuel Σ E Γ A ;;
                    t' <- tsl_rec fuel Σ E (Γ ,, vass n A) b t ;;
                    ret (tLambda n A' t')

  | tLetIn n t A u ⇒ t' <- tsl_term fuel Σ E Γ t ;;
                     A' <- tsl_ty_param fuel Σ E Γ A ;;
                     u' <- tsl_rec fuel Σ E (Γ ,, vdef n t A) b u ;;
                     ret (tLetIn n t' A' u')

  | tApp t u ⇒ t' <- tsl_rec fuel Σ E Γ b t ;;
               u' <- monad_map (tsl_term fuel Σ E Γ) u ;;
               ret (tApp t' u')

  | tConst _ _ as t
  | tInd _ _ as t
  | tConstruct _ _ _ as t ⇒ t' <- tsl_term fuel Σ E Γ t ;;
                            ret (proj b t')
  | _ ⇒ raise TranslationNotHandeled
  end
  end

with tsl_term (fuel : nat) (Σ : global_env_ext) (E : tsl_table) (Γ : context)
               (t : term) {struct fuel} : tsl_result term :=
  match fuel with
  | O ⇒ raise NotEnoughFuel
  | S fuel ⇒
  match t with
  | tRel n ⇒ ret (tRel n)

  | tSort s ⇒
    ret (pair (tSort fresh_universe)
              (tLambda (nNamed "A") (tSort fresh_universe) (tProd nAnon (tRel 0) (tSort fresh_universe)))
              (tSort s)
              (tLambda (nNamed "A") (tSort s) (tProd nAnon (tRel 0) (tSort s))))

  | tCast t c A ⇒ t' <- tsl_term fuel Σ E Γ t ;;
                  A' <- tsl_ty_param fuel Σ E Γ A ;;
                  ret (tCast t' c A')

  | tConst s univs ⇒ lookup_tsl_table' E (ConstRef s)
  | tInd i univs ⇒ lookup_tsl_table' E (IndRef i)
  | tConstruct i n univs ⇒ lookup_tsl_table' E (ConstructRef i n)
  | t ⇒ match infer' Σ Γ t with
         | Checked typ ⇒ let typ := refresh_universes typ in
                         t1 <- tsl_rec fuel Σ E Γ true t ;;
                         t2 <- tsl_rec fuel Σ E Γ false t ;;
                         typ1 <- tsl_rec fuel Σ E Γ true typ ;;
                         typ2 <- tsl_rec fuel Σ E Γ false typ ;;
                         ret (pair typ1 typ2 t1 t2)
        | TypeError t ⇒ raise (TypingError t)
        end
  end
  end
where "'tsl_ty_param'" := (fun fuel Σ E Γ t ⇒
                        t1 <- tsl_rec fuel Σ E Γ true t ;;
                        t2 <- tsl_rec fuel Σ E Γ false t ;;
                        ret (pack t1 t2)).

Instance tsl_param : Translation
  := {| tsl_id := tsl_ident ;
        tsl_tm := fun ΣE ⇒ tsl_term fuel (fst ΣE) (snd ΣE) [] ;
        tsl_ty := Some (fun ΣE ⇒ tsl_ty_param fuel (fst ΣE) (snd ΣE) []) ;
        tsl_ind := todo |}.

Notation "'TYPE'" := ({ A : Type & A → Type}).
Notation "'El' A" := (@sigT A.1 A.2) (at level 20).

Definition Ty := Type.
Check Tyᵗ : El Tyᵗ.



Check "yo".




Definition Funext :=
  ∀ A (B : A → Type) (f g : ∀ x, B x), (∀ x, paths (f x) (g x)) → paths f g.


Definition Funext_fullFunext : Funext → ∀ A B f g, IsEquiv (@apD10 A B f g).
Admitted.

Goal Funext → El Funextᵗ.

Definition FALSE := ∀ X, X.

Proposition consistency_preservation : El FALSEᵗ → FALSE.

Definition UIP := ∀ A (x y : A) (p q : paths x y), paths p q.


Proposition uip_preservation : UIP → El UIPᵗ.

Notation " A × B " := (@sigT A (fun _ ⇒ B)) : type_scope.

Definition equiv (A B : Type) : Type :=
  ∃ (f : A → B) (g : B → A),
    (∀ x, paths (g (f x)) x) × (∀ x, paths (f (g x)) x).



Check "go".
Check "proof".