Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.opp_precat.

Require Import TypeTheory.Auxiliary.Auxiliary.
Require Import TypeTheory.Auxiliary.UnicodeNotations.
Require Import TypeTheory.Auxiliary.CategoryTheoryImports.

Set Automatic Introduction.

Section category_of_elements_covariant.

Variable C : precategory.
Variable F : functor C HSET.

Definition precategory_of_elements_ob_mor : precategory_ob_mor.
Proof.
  exists (∑ c : C, pr1hSet (F c)).
  intros ca db.
  exact (∑ f : pr1 ca --> pr1 db, #F f (pr2 ca) = (pr2 db)).
Defined.

Definition precategory_of_elements_data : precategory_data.
Proof.
  exists precategory_of_elements_ob_mor.
  split.
  - intro c.
    exists (identity (pr1 c)).
    eapply pathscomp0.
    + rewrite (functor_id F). apply idpath.
    + apply idpath.
  - intros a b c f g.
    exists (pr1 f ;; pr1 g).
    rewrite functor_comp. unfold compose; simpl in *.
    unfold compose. simpl.
    etrans. apply maponpaths. apply (pr2 f).
    apply (pr2 g).
Defined.

Lemma is_precategory_precategory_of_elements : is_precategory precategory_of_elements_data.
Proof.
  repeat split; intros;
  simpl in *.
  - apply subtypeEquality.
    + intro. apply setproperty.
    + apply id_left.
  - apply subtypeEquality.
    + intro; apply setproperty.
    + apply id_right.
  - apply subtypeEquality.
    + intro; apply setproperty.
    + apply assoc.
Qed.

Definition precategory_of_elements : precategory
  := tpair _ _ is_precategory_precategory_of_elements.

Local Notation "∫" := precategory_of_elements.

Definition proj_functor_data : functor_data ∫ C.
Proof.
  exists (@pr1 _ _ ).
  exact (λ a b, @pr1 _ _ ).
Defined.

Lemma is_functor_proj : is_functor proj_functor_data.
Proof.
  split; unfold functor_idax, functor_compax; intros;
  simpl in *; apply idpath.
Qed.

Definition proj_functor : functor _ _ := tpair _ _ is_functor_proj.

Definition Elem_cov_iso_type (ac bd : ∫) : UU
  := ∑ (f : iso (pr1 ac) (pr1 bd)), #F f (pr2 ac) = pr2 bd.

Definition Elem_cov_iso_type_eq {ac bd : ∫} (T T' : Elem_cov_iso_type ac bd)
  : T = T' ≃ (pr1 (pr1 T)) = (pr1 (pr1 T')).
Proof.
  eapply weqcomp.
    apply subtypeInjectivity.     intro. apply setproperty.
  apply subtypeInjectivity.
  intro. apply isaprop_is_iso.
Defined.


Definition Elem_cov_iso_gives_iso (ac bd : ∫) :
  iso ac bd → iso (pr1 ac) (pr1 bd).
Proof.
  intro H.
  set (H':=is_z_iso_from_is_iso H (pr2 H)).
  exists (pr1 (pr1 H)).
  apply is_iso_from_is_z_iso.
  exists (pr1 (pr1 H')).
  split.
  - set (T:= pr1 (pr2 H')).
    apply (maponpaths pr1 T).
  - apply (maponpaths pr1 (pr2 (pr2 H'))).
Defined.

Definition Elem_cov_iso_to_Elem_cov_iso_type (ac bd : ∫) :
  iso ac bd → Elem_cov_iso_type ac bd.
Proof.
  intro H.
  exists (Elem_cov_iso_gives_iso _ _ H).
  simpl.
  exact (pr2 (pr1 H)).
Defined.

Lemma iso_in_HSET (A B : HSET) (f : iso A B) (Y : pr1 B) (X : pr1 A) :
  pr1 f X = Y → inv_from_iso f Y = X.
Proof.
  intro H.
  set (T:= maponpaths (inv_from_iso f) H).
  apply pathsinv0.
  etrans. Focus 2. apply T.
  apply pathsinv0.
  set (HT:= iso_inv_after_iso f).
  set (HT':= toforallpaths _ _ _ HT).
  apply HT'.
Qed.

Lemma foo (ac bd : ∫) (H : Elem_cov_iso_type ac bd) :
  # F (inv_from_iso (pr1 H)) (pr2 bd) = pr2 ac.
Proof.
  destruct H as [t p].
  destruct ac as [a c].
  destruct bd as [b d]; simpl in *.
  set (T:= (@functor_on_inv_from_iso _ HSET F _ _ t)).
  set (T':= toforallpaths _ _ _ T d).
  etrans. apply T'. clear T' T.
  apply iso_in_HSET.
  apply p.
Qed.

Definition Elem_cov_iso_type_to_Elem_cov_iso (ac bd : ∫) :
  Elem_cov_iso_type ac bd → iso ac bd .
Proof.
  intro H.
  unshelve refine (tpair _ _ _ ).
  unshelve refine (tpair _ _ _ ).
  - exact (pr1 H).
  - exact (pr2 H).
  - apply is_iso_from_is_z_iso.
    unshelve refine (tpair _ _ _ ).
    exists (inv_from_iso (pr1 H)).
    apply foo.
    split.
    + apply subtypeEquality.
      intro; apply setproperty.
      simpl. apply iso_inv_after_iso.
    + apply subtypeEquality.
      intro; apply setproperty.
      simpl. apply iso_after_iso_inv.
Defined.

Definition Elem_cov_iso_type_equiv_Elem_cov_iso (ac bd : ∫) :
  iso ac bd ≃ Elem_cov_iso_type ac bd.
Proof.
  exists (Elem_cov_iso_to_Elem_cov_iso_type _ _ ).
  apply (gradth _ (Elem_cov_iso_type_to_Elem_cov_iso _ _ )).
  - intro.
    apply eq_iso. simpl.
    apply subtypeEquality.
    + intro; apply setproperty.
    + apply idpath.
  - intro.
    apply (invmap (Elem_cov_iso_type_eq _ _ )).
    apply idpath.
Defined.

Lemma bla (H : is_univalent C) (ac bd : ∫) :
  ac = bd ≃ ∑ p : iso (pr1 ac) (pr1 bd), #F p (pr2 ac) = pr2 bd.
Proof.
  eapply weqcomp.
  apply total2_paths_equiv.
  unshelve refine (weqbandf (weqpair (@idtoiso _ _ _ ) _ ) _ _ _ ).
  - apply (pr1 H).
  - simpl. intro x.
    destruct ac. destruct bd.
    simpl in *.
    induction x. simpl.
    rewrite (functor_id F).
    apply idweq.
Defined.

Definition foobar (H : is_univalent C) (ac bd : ∫) :
  ac = bd ≃ iso ac bd.
Proof.
  eapply weqcomp.
  apply bla.
  apply H.
  apply invweq.
  apply Elem_cov_iso_type_equiv_Elem_cov_iso.
Defined.


Definition is_univalent_Elem (H : is_univalent C) : is_univalent ∫.
Proof.
  split.
  - intros a b.
    set (T := isweqhomot (foobar H a b)(@idtoiso _ a b) ).
    apply T.
    intro p.
    induction p.
    destruct a; simpl in *.

    simpl.
    apply eq_iso.
    simpl.
    apply subtypeEquality. intro; apply setproperty.
    apply idpath.
    apply pr2.
  - intros a b.
    apply (isofhleveltotal2 2).
    apply (pr2 H).
    intro. apply isasetaprop.
    apply setproperty.
Defined.

End category_of_elements_covariant.