{-# OPTIONS --without-K #-}

module Ch6HoTT where

-- S¹-ind : (P : S¹ → Set) → (b : P base) → (ℓ : transport loop b ≡ b) → (x : S¹) → P x
-- S¹-ind P b ℓ base = transport ? b











  -- f : A → B
  -- a1 a2 : A
  -- p : a1 ≡ a2
  --
  -- (ap f p) : f a1 ≡ f a2


  -- f : (x : A) → B x
  -- a1 a2 : A
  -- p : a1 ≡ a2
  --
  -- T : B a1 → B a2
  -- T = transport B p
  -- (apd f p) : T (f a1) ≡ f a2
  -- (apd f p) : transport B p (f a1) ≡ f a2

import Relation.Binary.PropositionalEquality as Eq
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type) public

data _≡_ {l : Level} {A : Type l} : A → A → Type l where
 refl : (x : A) → x ≡ x

-- Path induction
path-ind : ∀ {u} → {A : Set} → 
          (C : (x y : A) → x ≡ y → Set u) → 
          (c : (x : A) → C x x (refl x)) → 
          {x y : A} → (p : x ≡ y) → C x y p
path-ind C c {x} (refl x) = c x

Path : {l : Level} (A : Type l) → A → A → Type l
Path A x y = x ≡ y

syntax Path A x y = x ≡ y [ A ]

id : {ℓ : Level} {A : Set ℓ} → A → A
id x = x

-- Transport
transport : {X : Set} (P : X → Set) {x y : X} → x ≡ y → P x → P y
transport P (refl x) = id

ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f p = path-ind (λ x y p → f x ≡ f y) (λ x → ?) p

postulate
  S¹ : Set

  base : S¹

  loop : base ≡ base [ S¹ ]

  -- (apd f p) : transport B p (f a1) ≡ f a2
  -- apd _ loop
  -- f : (x : A) → C x
  -- loop : base ≡ base, base : S¹
  --
  -- apd f loop : transport C loop (f base) ≡ f base
  --
  -- S¹-ind : (C : S¹ → Set)
  --   → (c-base : C base)
  --   → (c-loop : ?)
  --   → (s : S¹) → C s
  --
  -- N-ind : () → (c-zero : C 0) → ... → (n : N) → C n
  --
  -- N-ind 0 : C 0
  --
  -- f : (x : S¹) → C x
  -- f = S¹-ind C _ _
  --
  -- f base : C base
  --
  -- apd (f) loop : (transport C loop (f base)) ≡ f base
  -- (c-loop : (transport C loop (f base)) ≡ f base)
  --
  -- ap f (p₁ ∙ p₂) = (ap f p₁) ∙ (ap f p₂)

-- (λ _ → A)

lemma625 : {A : Set} → (a : A) → (p : a ≡ a) → (S¹ → A)
lemma625 a p s1 = ?

lemma625prop1 : {A : Set} {a : A} {p : a ≡ a} → (lemma625 a p base ≡ a)
-- lemma625prop1 = refl

lemma625prop2 : {A : Set} (a : A) → (p : a ≡ a) → ap (lemma625 a p) loop ≡ p
-- lemma625prop2 a p = refl

-- f : S¹ → A
-- f = lemma625 a p
--
-- f-loop : f base ≡ f base
-- f-loop : ap f loop
--
-- f-loop ≡ p