siddhartha-gadgil

transport : {A : Set} → {B : Set} → {x y : A} → (f : A → B) → x == y → f(x) == f(y)
transport f (refl a) = refl (f a)

symm : {A : Set} → {x y : A} → x == y → y == x
symm (refl a) = refl a


_transEq_ : {A : Set} → {x y z : A} → x == y → y == z → x == z
(refl a) transEq (refl .a) = refl a

siddhartha-gadgil

open import Nat

-- If f(m+1) = f(m) for all m, then f(n) = f(0) for all n  
constthm : (f : ℕ → ℕ) → ((m : ℕ) → (f (succ m)) == (f m)) → (n : ℕ) → (f n) == (f 0)
constthm f _ 0 = refl (f 0)
constthm f adjEq (succ n) = (adjEq n) transEq (constthm f adjEq n)

siddhartha-gadgil

data _×_ (A B : Set) : Set where
  [_,_] : A → B → A × B

siddhartha-gadgil

data _⊕_ (A B : Set) : Set where
  i₁ : A → A ⊕ B
  i₂ : B → A ⊕ B

siddhartha-gadgil

data Σ(A : Set) (B : A → Set) : Set where
  ι : (a : A) → B a → Σ A B

siddhartha-gadgil

postulate 
  extensionality : {A B : Set} → (f g : A → B) → ((x : A) → (f x) == (g x)) → f == g

siddhartha-gadgil

---
title: Faculty Members
---

<div class="col-md-12">
<h2>Faculty members</h2>

<h4>Alphabetically by last name</h4>

  <p><b>To send email: <font face="Courier New" size="3">UserID[at]iisc.ac.in</font></b></p>

siddhartha-gadgil

- name: Arvind Ayyer
  user-id: arvind
  research-areas: Probability, combinatorics, statistical mechanics, mathematical physics, experimental mathematics
  phd: Rutgers
  phone-ext: 3215
  office: X15

- name: Abhishek Banerjee
  user-id: abhishek
  research-areas: Algebraic geometry, noncommutative geometry

siddhartha-gadgil

---

title: Algebraic Number Theory code: MA 313 books:

• author: Artin, E. title: Galois Theory publ: University of Notre Dame Press, 1944
• author: Borevich, Z. and Shafarevich, I. title: Number Theory publ: Academic Press, New York, 1966

siddhartha-gadgil

---
title: Course Catalogue
---

<h2>Course Catalogue</h2>
    {% assign sorted = (site.all-courses | sort: 'code')  %}

{% for course in sorted  %}