import types.fiber hit.trunc homotopy.circle

open eq eq.ops sigma sigma.ops equiv trunc trunc_index is_trunc
open function unit

namespace cegar_hott

definition Residual {X A : Type} (p : X -> A) (a : A) : Type :=
  fiber p a

definition Support {X A : Type} (p : X -> A) (a : A) : Type :=
  trunc -1 (Residual p a)

definition lift_support {X A : Type} {p : X -> A} {a : A} :
  Residual p a -> Support p a :=
  tr

definition refute_support {X A : Type} {p : X -> A} {a : A}
  (h : Residual p a -> empty) : Support p a -> empty :=
  @trunc.elim -1 (Residual p a) empty is_prop_empty h

definition refute_residual {X A : Type} {p : X -> A} {a : A}
  (h : Support p a -> empty) : Residual p a -> empty :=
  fun  r, h (lift_support r)

definition reindex {A U : Type} (b : U -> A) (P : A -> Type) (u : U) : Type :=
  P (b u)

definition pullback_total {A U : Type} (b : U -> A) (P : A -> Type) : Type :=
  Sigma  u : U, reindex b P u

definition projection {A U : Type} {b : U -> A} {P : A -> Type} :
  pullback_total b P -> U := pr1

definition reindex_fiber {A U : Type} (b : U -> A) (P : A -> Type) (u : U) :
  fiber (@projection A U b P) u ~= P (b u) :=
  fiber.fiber_pr1 (reindex b P) u

definition reindex_support {X A U : Type} (p : X -> A) (b : U -> A) (u : U) :
  trunc -1 (fiber (@projection A U b (Residual p)) u) ~= Support p (b u) :=
  trunc_equiv_trunc (-1) (reindex_fiber b (Residual p) u)

definition residual_compose {X A B : Type} (p : X -> A) (r : A -> B) (b : B) :
  Residual (r  o  p) b ~= (Sigma  a : Residual r b, Residual p (fiber.point a)) :=
  fiber.fiber_compose_equiv r p b

definition compose_point {X A B : Type} {p : X -> A} {r : A -> B} {b : B}
  (a : Residual r b) (x : Residual p (fiber.point a)) : Residual (r  o  p) b :=
  fiber.mk (fiber.point x) (ap r (fiber.point_eq x)  @  fiber.point_eq a)

definition transport_reindex {A U : Type} (b : U -> A) (P : A -> Type)
  {u v : U} (e : u = v) (x : P (b u)) :
  transport (reindex b P) e x = transport P (ap b e) x :=
  by induction e; reflexivity

definition residual_identity {X A : Type} {p : X -> A} {a : A}
  (x y : Residual p a) :
  (x = y) ~=
  (Sigma  e : fiber.point x = fiber.point y,
    fiber.point_eq x = ap p e  @  fiber.point_eq y) :=
  fiber.fiber_eq_equiv x y

open circle

definition constant_circle : unit -> S1 := fun  x, base
definition reflexive_lift : Residual constant_circle base := fiber.mk star idp
definition winding_lift : Residual constant_circle base := fiber.mk star loop

definition lifts_are_distinct : winding_lift != reflexive_lift :=
  fun  h, loop_neq_idp (ap (@fiber.point_eq unit S1 constant_circle base) h)

definition circle_support : Support constant_circle base :=
  lift_support winding_lift

end cegar_hott
